English
Let I be an ideal of a local ring R, then there exists a surjective map from the residue field of R to S with properties etc. (lift construction).
Русский
Пусть I — идеал локального кольца R. Существуют отображения, связанные с полем остатка и локальным гомоморфизмом, включая конструкцию подъема (lift).
LaTeX
$$$\\exists f : \\operatorname{IsLocalRing.ResidueField}(R) \\to+* (S) \\,\\ \\, \\text{(lift construction)}$$$
Lean4
theorem basisQuotient_repr {ι} [Fintype ι] (b : Basis ι R S) (x) (i) :
(basisQuotient b).repr (Ideal.Quotient.mk pS x) i = Ideal.Quotient.mk p (b.repr x i) :=
by
refine congr_fun (g := Ideal.Quotient.mk p ∘ b.repr x) ?_ i
apply (Finsupp.linearEquivFunOnFinite (R ⧸ p) _ _).symm.injective
apply (basisQuotient b).repr.symm.injective
simp only [Finsupp.linearEquivFunOnFinite_symm_coe, LinearEquiv.symm_apply_apply, Basis.repr_symm_apply]
rw [Finsupp.linearCombination_eq_fintype_linearCombination_apply (R ⧸ p), Fintype.linearCombination_apply]
simp only [Function.comp_apply, basisQuotient_apply, Ideal.Quotient.mk_smul_mk_quotient_map_quotient,
← Algebra.smul_def]
rw [← map_sum, Basis.sum_repr b x]
