English
Given a basis b of S as an R-module, the images of the basis elements in S/pS form a basis of S/pS as a module over R/p.
Русский
Дано базис b множества S как модуля над R; изображения элементов базиса в S/pS образуют базис S/pS как модуль над R/p.
LaTeX
$$$\\text{basisQuotient}\\;[\\;Fintype\\;\\iota]\\; (b : \\text{Basis } \\iota \\; R \\; S) : \\text{Basis } \\iota \\; (R/\\mathfrak p) \\; (S/\\mathfrak p S)$$$
Lean4
/-- Given a basis of `S`, the induced basis of `S / Ideal.map (algebraMap R S) p`. -/
noncomputable def basisQuotient [Fintype ι] (b : Basis ι R S) : Basis ι (R ⧸ p) (S ⧸ pS) :=
basisOfTopLeSpanOfCardEqFinrank (Ideal.Quotient.mk pS ∘ b)
(by
rw [Set.range_comp]
exact ((quotient_span_eq_top_iff_span_eq_top _).mpr b.span_eq).ge)
(by rw [finrank_quotient_map, finrank_eq_card_basis b])
