English
A variant of the previous induction principle where the motive travels through the quotient ring R/(r). This allows propagating certain module properties through the induction while keeping track of the ring quotient.
Русский
Вариант принципа индукции, где мотив «путешествует» через факторкольцо R/(r). Это позволяет распространять некоторые свойства модуля вдоль индукции, сохраняя связь с фактор-кольцом.
LaTeX
$$$\\text{ndrecIterModByRegularWithRing}$ expresses induction with ring quotients: IsRegular(M, rs) \\Rightarrow \\text{motive}(R, M, rs)$$$
Lean4
/-- An alternate induction principle from `IsRegular.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) → IsRegular M rs → Sort*}
(nil :
(R : Type u) →
[CommRing R] → (M : Type v) → [AddCommGroup M] → [Module R M] → [Nontrivial 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 : IsRegular (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} [CommRing R] {M} [AddCommGroup M] [Module R M] {rs} (h : IsRegular M rs) : motive R M rs h :=
h.toIsWeaklyRegular.recIterModByRegularWithRing (motive := fun R _ N _ _ rs' h' => ∀ h'', motive R N rs' ⟨h', h''⟩)
(fun R _ N _ _ h' =>
haveI := (nontrivial_iff R).mp (nontrivial_of_ne _ _ h');
nil R N)
(fun r rs' h1 h2 h3 h4 =>
have ⟨h5, h6⟩ := (isRegular_cons_iff' _ _ _).mp ⟨h2.cons' h1, h4⟩
cons r rs' h5 h6 <| h3 h6.top_ne_smul)
h.top_ne_smul
