map_first_exact_on_four_term_right_exact_of_isSMulRegular_last

English

A more detailed version of Ring-Induction that tracks a map on rs and its images under quotient maps, enabling inductive control of the isomorphism-induced regularity.

Русский

Улучшенная версия рег-индукции, отслеживающая отображение по rs и их образам в фактор-мепах, что позволяет контролировать регулярность через изоморфизмы.

LaTeX

$$$\\text{recIterModByRegularWithRing}$ tracks $rs$ under $R/(r)$ and propagates regularity.$$

Lean4

theorem map_first_exact_on_four_term_right_exact_of_isSMulRegular_last {rs : List R} {f₁ : M →ₗ[R] M₂}
    {f₂ : M₂ →ₗ[R] M₃} {f₃ : M₃ →ₗ[R] M₄} (h₁₂ : Exact f₁ f₂) (h₂₃ : Exact f₂ f₃) (h₃ : Surjective f₃)
    (h₄ : IsWeaklyRegular M₄ rs) :
    Exact (mapQ _ _ _ (smul_top_le_comap_smul_top (Ideal.ofList rs) f₁))
      (mapQ _ _ _ (smul_top_le_comap_smul_top (Ideal.ofList rs) f₂)) :=
  by
  induction h₄ generalizing M M₂ M₃ with
  | nil =>
    apply (Exact.iff_of_ladder_linearEquiv ?_ ?_).mp h₁₂
    any_goals exact quotEquivOfEqBot _ <| Eq.trans (congrArg (· • ⊤) Ideal.ofList_nil) (bot_smul ⊤)
    all_goals exact quot_hom_ext _ _ _ fun _ => rfl
  | cons r rs h₄ _
    ih =>
    specialize
      ih (map_first_exact_on_four_term_exact_of_isSMulRegular_last h₁₂ h₂₃ h₄) (map_exact r h₂₃ h₃)
        (map_surjective r h₃)
    have H₁ := quotOfListConsSMulTopEquivQuotSMulTopInner_naturality r rs f₁
    have H₂ := quotOfListConsSMulTopEquivQuotSMulTopInner_naturality r rs f₂
    exact (Exact.iff_of_ladder_linearEquiv H₁.symm H₂.symm).mp ih

Похожие утверждения