induction — Mathlib

English

Let P be a property of modules M over rings R0 ⊂ R with IsScalarTower R0 R M and IsSemiprimaryRing R. If (i) P holds for all IsSemisimpleModule R M that are torsion by the Jacobson ideal, and (ii) whenever N = Jac(R)·⊤ in M, P(N) and P(M/N) imply P(M), then P(M) holds for all M. In short, there is a structural induction principle for semiprimary rings.

Русский

Пусть P — свойство над модулями M над кольцами R0 ⊂ R с тензорной структурой и IsSemiprimaryRing R. Если (i) P верно для всех IsSemisimpleModule R M, для которых M имеетJac(R)-torsion, и (ii) если N = Jac(R)·⊤ и P(N) и P(M/N) следует, тогда P(M) верно; тогда P верно для всех M. То есть существует индуктивный принцип для полуприводных колец.

LaTeX

$$$\\forall (R_0,R,M) \\; [\\text{Ring }R_0] [\\text{Ring }R] [\\text{Module }R_0M][IsScalarTower R_0R M] [IsSemiprimaryRing R],\\ P:\\text{(модули)}\\\\\\text{(модули)} \\\\left(\\bigl( \\forall M\\,[IsSemisimpleModule\\;R\\;M] \\,\\Rightarrow\, \\text{Torsion}_{R}(M) \\Rightarrow P(M) \\bigr) \\,\\land\, \\forall M \\,\\bigl( P(N) \\land P(M/N) \\Rightarrow P(M) \\bigr) \\right) \\Rightarrow \\forall M\\; P(M).$$$

Lean4

@[elab_as_elim]
protected theorem induction {P : ∀ (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M], Prop}
    (h0 :
      ∀ (M) [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] [IsSemisimpleModule R M],
        Module.IsTorsionBySet R M (Ring.jacobson R) → P M)
    (h1 :
      ∀ (M) [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M],
        let N := Ring.jacobson R • (⊤ : Submodule R M);
        P N → P (M ⧸ N) → P M) :
    P M := by
  have ⟨ss, n, hn⟩ := (isSemiprimaryRing_iff R).mp ‹_›
  set Jac := Ring.jacobson R
  replace hn : Jac ^ n ≤ Module.annihilator R M := hn ▸ bot_le
  have {M} [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] : Jac ≤ Module.annihilator R M → P M :=
    by
    rw [← SetLike.coe_subset_coe, ← Module.isTorsionBySet_iff_subset_annihilator]
    intro h
    let _ := h.module
    have := (h.semilinearMap.isSemisimpleModule_iff_of_bijective Function.bijective_id).2 inferInstance
    exact h0 _ h
  induction n generalizing M with
  | zero => rw [Jac.pow_zero, Ideal.one_eq_top] at hn; exact this (le_top.trans hn)
  | succ n ih => ?_
  obtain _ | n := n
  · rw [Jac.pow_one] at hn; exact this hn
  refine h1 _ (ih _ ?_) (ih _ ?_)
  ·
    rwa [← Submodule.annihilator_top, Submodule.le_annihilator_iff, Jac.pow_succ, Submodule.mul_smul, ←
      Submodule.le_annihilator_iff] at hn
  · rw [← SetLike.coe_subset_coe, ← Module.isTorsionBySet_iff_subset_annihilator, Module.isTorsionBySet_quotient_iff]
    exact fun m i hi ↦ Submodule.smul_mem_smul (Ideal.pow_le_self n.succ_ne_zero hi) trivial

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