English
Regular sequences on a module M over a ring R are defined inductively by two rules: (i) the empty sequence is regular on every nonzero module; (ii) if r is regular on M and rs is a regular sequence on M modulo rM, then the sequence obtained by prepending r to rs is regular on M. The associated induction principle asserts that any property defined recursively in this way holds for all regular sequences.
Русский
Регулярные последовательности на модуле M над кольцом R задаются индуктивно двумя правилами: (i) пустая последовательность регулярна на любом ненулевом модуле; (ii) если r регулярен на M и rs — регулярная последовательность на M/ rM, то последовательность, полученная добавлением r спереди к rs, регулярна на M. Связанный принцип индукции утверждает, что любая свойство, заданное таким образом, переносится на всю регулярную последовательность.
LaTeX
$$$\\forall R, M, rs:\\ \\text{IsRegular}(M, rs) \\Rightarrow \\Big(\\text{NilRule}(M) \\wedge \\text{ConsRule}(M, rs)\\Big) \\text{ induces a principle of induction for regular sequences}$$$
Lean4
/-- Regular sequences can be inductively characterized by:
* The empty sequence is regular on any nonzero module.
* If `r` is regular on `M` and `rs` is a regular sequence on `M⧸rM` then the
sequence obtained from `rs` by prepending `r` is regular on `M`.
This is the induction principle produced by the inductive definition above.
The motive will usually be valued in `Prop`, but `Sort*` works too. -/
@[induction_eliminator]
def recIterModByRegular
{motive : (M : Type v) → [AddCommGroup M] → [Module R M] → (rs : List R) → IsRegular M rs → Sort*}
(nil : (M : Type v) → [AddCommGroup M] → [Module R M] → [Nontrivial M] → motive M [] (nil R M))
(cons :
{M : Type v} →
[AddCommGroup M] →
[Module R M] →
(r : R) →
(rs : List R) →
(h1 : IsSMulRegular M r) →
(h2 : IsRegular (QuotSMulTop r M) rs) →
(ih : motive (QuotSMulTop r M) rs h2) → motive M (r :: rs) (cons h1 h2))
{M} [AddCommGroup M] [Module R M] {rs} (h : IsRegular M rs) : motive M rs h :=
h.toIsWeaklyRegular.recIterModByRegular (motive := fun N _ _ rs' h' => ∀ h'', motive N rs' ⟨h', h''⟩)
(fun N _ _ h' =>
haveI := (nontrivial_iff R).mp (nontrivial_of_ne _ _ h');
nil 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
