Theorem: Ideal.kerLiftAlg_eq_val_comp_Equiv (DividedPowers/PolynomialMap/Basic.lean)

State before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
⊢ kerLiftAlg φ = φ.range.val.comp ↑(quotientKerEquivRange φ)
Tactic:
apply Ideal.Quotient.algHom_ext
State after:
case h
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
⊢ (kerLiftAlg φ).comp (Quotient.mkₐ R (RingHom.ker φ)) =
    (φ.range.val.comp ↑(quotientKerEquivRange φ)).comp (Quotient.mkₐ R (RingHom.ker φ))

State before:
case h
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
⊢ (kerLiftAlg φ).comp (Quotient.mkₐ R (RingHom.ker φ)) =
    (φ.range.val.comp ↑(quotientKerEquivRange φ)).comp (Quotient.mkₐ R (RingHom.ker φ))
Tactic:
ext s
State after:
case h.H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ ((kerLiftAlg φ).comp (Quotient.mkₐ R (RingHom.ker φ))) s =
    ((φ.range.val.comp ↑(quotientKerEquivRange φ)).comp (Quotient.mkₐ R (RingHom.ker φ))) s

State before:
case h.H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ ((kerLiftAlg φ).comp (Quotient.mkₐ R (RingHom.ker φ))) s =
    ((φ.range.val.comp ↑(quotientKerEquivRange φ)).comp (Quotient.mkₐ R (RingHom.ker φ))) s
Tactic:
simp only [AlgHom.coe_comp, Quotient.mkₐ_eq_mk, Function.comp_apply, kerLiftAlg_mk,
  AlgEquiv.toAlgHom_eq_coe, Subalgebra.coe_val, AlgHom.coe_coe]
State after:
case h.H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ φ s = ↑((quotientKerEquivRange φ) ((Quotient.mk (RingHom.ker φ)) s))

State before:
case h.H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
s : S
⊢ φ s = ↑((quotientKerEquivRange φ) ((Quotient.mk (RingHom.ker φ)) s))
Tactic:
rfl
State after:
no goals