English
For a given lift, applying g to the lifted element yields the original value.
Русский
При применении g к первому элементу подъема получается исходное значение.
LaTeX
$$g (liftOfSurjective f g hg hg' x) = f x for all x in A.$$
Lean4
@[simp]
theorem liftOfSurjective_apply [FormallySmooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : Function.Surjective g)
(hg' : IsNilpotent <| RingHom.ker g) (x : A) : g (FormallySmooth.liftOfSurjective f g hg hg' x) = f x :=
by
apply (Ideal.quotientKerAlgEquivOfSurjective hg).symm.injective
conv_rhs => rw [← AlgHom.coe_coe, ← AlgHom.comp_apply, ← FormallySmooth.mk_lift (A := A) _ hg']
apply (Ideal.quotientKerAlgEquivOfSurjective hg).injective
rw [AlgEquiv.apply_symm_apply, Ideal.quotientKerAlgEquivOfSurjective_apply]
simp only [liftOfSurjective, ← RingHom.ker_coe_toRingHom g, RingHom.kerLift_mk, AlgEquiv.toAlgHom_eq_coe,
RingHom.coe_coe]
