English
If r is regular on M and rs is weakly regular on M ⧸ rM, then rs mapped through the quotient is weakly regular on M, hence r :: rs is weakly regular on M.
Русский
Если r регулярна на M, а rs слабая регулярность на M ⧸ rM, то rs после отображения через фактор-модуль обладает слабой регулярностью, следовательно, r :: rs -- слабая регулярная на M.
LaTeX
$$$IsWeaklyRegular(M, r :: rs) \\Rightarrow IsSMulRegular(M, r) \\, \\land \\, IsWeaklyRegular(QuotSMulTop r M, rs')$ where $rs'$ is $rs$ viewed in the quotient.$$
Lean4
/-- An alternate induction principle from `IsWeaklyRegular.recIterModByRegular`
where we mod out by successive elements in both the module and the base ring.
This is useful for propagating certain properties of the initial `M`, e.g.
faithfulness or freeness, throughout the induction. -/
def recIterModByRegularWithRing
{motive :
(R : Type u) →
[CommRing R] → (M : Type v) → [AddCommGroup M] → [Module R M] → (rs : List R) → IsWeaklyRegular M rs → Sort*}
(nil : (R : Type u) → [CommRing R] → (M : Type v) → [AddCommGroup M] → [Module R M] → motive R M [] (nil R M))
(cons :
{R : Type u} →
[CommRing R] →
{M : Type v} →
[AddCommGroup M] →
[Module R M] →
(r : R) →
(rs : List R) →
(h1 : IsSMulRegular M r) →
(h2 : IsWeaklyRegular (QuotSMulTop r M) (rs.map (Ideal.Quotient.mk (Ideal.span { r })))) →
(ih :
motive (R ⧸ Ideal.span { r }) (QuotSMulTop r M)
(rs.map (Ideal.Quotient.mk (Ideal.span { r }))) h2) →
motive R M (r :: rs) (cons' h1 h2)) :
{R : Type u} →
[CommRing R] →
{M : Type v} → [AddCommGroup M] → [Module R M] → {rs : List R} → (h : IsWeaklyRegular M rs) → motive R M rs h
| R, _, M, _, _, [], _ => nil R M
| _, _, M, _, _, r :: rs, h =>
let ⟨h1, h2⟩ := (isWeaklyRegular_cons_iff' M r rs).mp h
cons r rs h1 h2 (recIterModByRegularWithRing nil cons h2)
termination_by _ _ _ _ _ rs => List.length rs
