English
A further alteration of regInduction that tracks how a sequence behaves after successively modding out by ring elements, enabling preservation of properties like faithfulness and freeness along the induction path.
Русский
Дальнейшее изменение индукции регулярной последовательности, отслеживающее поведение последовательности после последовательного взятия фактор-модулей по элементам кольца; позволяет сохранять такие свойства, как верности и свободы вдоль хода индукции.
LaTeX
$$$\\text{ndrecIterModByRegularWithRing}$ provides induction with map over rs in the quotient rings $R/(r)$$$
Lean4
/-- A simplified version of `IsRegular.recIterModByRegularWithRing` where the
motive is not allowed to depend on the proof of `IsRegular`. -/
def ndrecIterModByRegularWithRing
{motive : (R : Type u) → [CommRing R] → (M : Type v) → [AddCommGroup M] → [Module R M] → (rs : List R) → Sort*}
(nil :
(R : Type u) → [CommRing R] → (M : Type v) → [AddCommGroup M] → [Module R M] → [Nontrivial M] → motive R M [])
(cons :
{R : Type u} →
[CommRing R] →
{M : Type v} →
[AddCommGroup M] →
[Module R M] →
(r : R) →
(rs : List R) →
IsSMulRegular M r →
IsRegular (QuotSMulTop r M) (rs.map (Ideal.Quotient.mk (Ideal.span { r }))) →
motive (R ⧸ Ideal.span { r }) (QuotSMulTop r M)
(rs.map (Ideal.Quotient.mk (Ideal.span { r }))) →
motive R M (r :: rs))
{R} [CommRing R] {M} [AddCommGroup M] [Module R M] {rs} : IsRegular M rs → motive R M rs :=
recIterModByRegularWithRing (motive := fun R _ M _ _ rs _ => motive R M rs) nil cons
