Krull–Schmidt

Results named in Tau Ceti's TauCeti.RingTheory.KrullSchmidt modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremAzumaya's exchange lemma#

Let M be the internal direct sum of a finite family Q of indecomposable submodules, and let N be a direct summand of M whose endomorphism ring is local (so in particular N is nonzero). Then N is isomorphic to one of the Q i₀, and can be exchanged for it: N and the remaining summands ⨆ j ≠ i₀, Q j are complementary in M.

The locality of Module.End A N is what Fitting's lemma TauCeti.isLocalRing_end_of_isIndecomposable supplies when M has finite length.

TauCeti.exists_linearEquiv_and_isCompl_biSup_ne.{u, v, w} {A : Type u} {M : Type v} [Ring A]
  [AddCommGroup M] [_root_.Module A M] {ι : Type w} [Finite ι] {Q : ι → Submodule A M}
  (hQi : iSupIndep Q) (hQt : ⨆ i, Q i = ⊤)
  (hQind : ∀ (i : ι), TauCeti.IsIndecomposableModule A ↥(Q i)) {N S : Submodule A M}
  [IsLocalRing (Module.End A ↥N)] (hNS : IsCompl N S) :
  ∃ i₀, Nonempty (↥N ≃ₗ[A] ↥(Q i₀)) ∧ IsCompl N (⨆ j, ⨆ (_ : j ≠ i₀), Q j)
Lean

Formalized in Tau Ceti as TauCeti.exists_linearEquiv_and_isCompl_biSup_ne.

Sources
LeanTauCeti.exists_linearEquiv_and_isCompl_biSup_ne
Used by 1
Used byThe Krull-Schmidt theorem

TheoremFitting's lemma#

an endomorphism of an indecomposable module that is both Noetherian and Artinian is either nilpotent or bijective.

For a large enough exponent m, Mathlib's Fitting decomposition splits M as ker (f ^ m) ⊕ range (f ^ m). Indecomposability collapses one of the two summands: if the range vanishes then f ^ m = 0, and if the kernel vanishes then f is injective while the range, being everything, forces f to be surjective.

TauCeti.IsIndecomposableModule.isNilpotent_or_bijective.{u, v} {A : Type u} {M : Type v} [Ring A]
  [AddCommGroup M] [_root_.Module A M] [IsNoetherian A M] [IsArtinian A M]
  (h : TauCeti.IsIndecomposableModule A M) (f : Module.End A M) :
  IsNilpotent f ∨ Function.Bijective ⇑f
Lean

Formalized in Tau Ceti as TauCeti.IsIndecomposableModule.isNilpotent_or_bijective.

Other forms

Fitting's lemma, restated. Formalized in Tau Ceti as TauCeti.IsIndecomposableModule.isNilpotent_or_isUnit.

TauCeti.IsIndecomposableModule.isNilpotent_or_isUnit.{u, v} {A : Type u} {M : Type v} [Ring A]
  [AddCommGroup M] [_root_.Module A M] [IsNoetherian A M] [IsArtinian A M]
  (h : TauCeti.IsIndecomposableModule A M) (f : Module.End A M) : IsNilpotent f ∨ IsUnit f
Sources
LeanTauCeti.IsIndecomposableModule.isNilpotent_or_bijective · TauCeti.IsIndecomposableModule.isNilpotent_or_isUnit
Used by 4
Used byFitting's lemma, categorically · TauCeti.isLocalRing_end_of_indecomposable · The finite level of the generator theorem (NSW, proof of (7.4.1)) · The Krull-Schmidt theorem

TheoremThe Krull-Schmidt theorem#

The Krull-Schmidt theorem, in the Finset packaging that TauCeti.exists_indecomposable_decomposition produces: two Finsets of indecomposable submodules each presenting the module as an internal direct sum are matched by a bijection under which corresponding summands are isomorphic.

TauCeti.exists_equiv_linearEquiv_of_finset.{u, v} {A : Type u} [Ring A] {M : Type v}
  [AddCommGroup M] [_root_.Module A M] (hM : IsFiniteLength A M) {s t : Finset (Submodule A M)}
  (hs : ∀ N ∈ s, TauCeti.IsIndecomposableModule A ↥N) (hsi : DirectSum.IsInternal fun N => ↑N)
  (ht : ∀ N ∈ t, TauCeti.IsIndecomposableModule A ↥N) (hti : DirectSum.IsInternal fun N => ↑N) :
  ∃ e, ∀ (N : ↥s), Nonempty (↥↑N ≃ₗ[A] ↥↑(e N))
Lean

Formalized in Tau Ceti as TauCeti.exists_equiv_linearEquiv_of_finset.

Other forms

The Krull-Schmidt theorem. Formalized in Tau Ceti as TauCeti.exists_equiv_linearEquiv_of_iSupIndep.

TauCeti.exists_equiv_linearEquiv_of_iSupIndep.{u, v, w, x} {A : Type u} [Ring A] {M : Type v}
  [AddCommGroup M] [_root_.Module A M] [IsNoetherian A M] [IsArtinian A M] {ι : Type w} {κ : Type x}
  {P : ι → Submodule A M} {Q : κ → Submodule A M} (hP : iSupIndep P) (hPt : ⨆ i, P i = ⊤)
  (hPind : ∀ (i : ι), TauCeti.IsIndecomposableModule A ↥(P i)) (hQ : iSupIndep Q)
  (hQt : ⨆ j, Q j = ⊤) (hQind : ∀ (j : κ), TauCeti.IsIndecomposableModule A ↥(Q j)) :
  ∃ e, ∀ (i : ι), Nonempty (↥(P i) ≃ₗ[A] ↥(Q (e i)))

The Krull-Schmidt theorem, in Azumaya's generality. Formalized in Tau Ceti as TauCeti.exists_equiv_linearEquiv_of_isLocalRing_end.

TauCeti.exists_equiv_linearEquiv_of_isLocalRing_end.{u, v, w, x} {A : Type u} [Ring A] {M : Type v}
  [AddCommGroup M] [_root_.Module A M] {ι : Type w} {κ : Type x} [Finite ι] [Finite κ]
  {P : ι → Submodule A M} {Q : κ → Submodule A M} (hP : iSupIndep P) (hPt : ⨆ i, P i = ⊤)
  (hPloc : ∀ (i : ι), IsLocalRing (Module.End A ↥(P i))) (hQ : iSupIndep Q) (hQt : ⨆ j, Q j = ⊤)
  (hQind : ∀ (j : κ), TauCeti.IsIndecomposableModule A ↥(Q j)) :
  ∃ e, ∀ (i : ι), Nonempty (↥(P i) ≃ₗ[A] ↥(Q (e i)))

The Krull-Schmidt theorem for external direct sums. Formalized in Tau Ceti as TauCeti.exists_equiv_linearEquiv_of_directSum.

TauCeti.exists_equiv_linearEquiv_of_directSum.{u, v, w, x, y, z} {A : Type u} [Ring A] {M : Type v}
  [AddCommGroup M] [_root_.Module A M] {ι : Type w} {κ : Type x} {N : ι → Type y}
  [(i : ι) → AddCommGroup (N i)] [(i : ι) → _root_.Module A (N i)] {Q : κ → Type z}
  [(j : κ) → AddCommGroup (Q j)] [(j : κ) → _root_.Module A (Q j)] [IsNoetherian A M]
  [IsArtinian A M] (eN : M ≃ₗ[A] DirectSum ι fun i => N i) (eQ : M ≃ₗ[A] DirectSum κ fun j => Q j)
  (hN : ∀ (i : ι), TauCeti.IsIndecomposableModule A (N i))
  (hQ : ∀ (j : κ), TauCeti.IsIndecomposableModule A (Q j)) :
  ∃ e, ∀ (i : ι), Nonempty (N i ≃ₗ[A] Q (e i))

The Krull-Schmidt theorem for external direct sums, in Azumaya's generality. Formalized in Tau Ceti as TauCeti.exists_equiv_linearEquiv_of_directSum_of_isLocalRing_end.

TauCeti.exists_equiv_linearEquiv_of_directSum_of_isLocalRing_end.{u, v, w, x, y, z} {A : Type u}
  [Ring A] {M : Type v} [AddCommGroup M] [_root_.Module A M] {ι : Type w} {κ : Type x}
  {N : ι → Type y} [(i : ι) → AddCommGroup (N i)] [(i : ι) → _root_.Module A (N i)] {Q : κ → Type z}
  [(j : κ) → AddCommGroup (Q j)] [(j : κ) → _root_.Module A (Q j)] [Finite ι] [Finite κ]
  (eN : M ≃ₗ[A] DirectSum ι fun i => N i) (eQ : M ≃ₗ[A] DirectSum κ fun j => Q j)
  (hN : ∀ (i : ι), IsLocalRing (Module.End A (N i)))
  (hQ : ∀ (j : κ), TauCeti.IsIndecomposableModule A (Q j)) :
  ∃ e, ∀ (i : ι), Nonempty (N i ≃ₗ[A] Q (e i))

The Krull-Schmidt theorem for two abstract families of summands. Formalized in Tau Ceti as TauCeti.exists_equiv_linearEquiv_of_directSumEquiv.

TauCeti.exists_equiv_linearEquiv_of_directSumEquiv.{u, w, x, y, z} {A : Type u} [Ring A]
  {ι : Type w} {κ : Type x} {N : ι → Type y} [(i : ι) → AddCommGroup (N i)]
  [(i : ι) → _root_.Module A (N i)] {Q : κ → Type z} [(j : κ) → AddCommGroup (Q j)]
  [(j : κ) → _root_.Module A (Q j)] [Finite ι] [Finite κ]
  (e : (DirectSum ι fun i => N i) ≃ₗ[A] DirectSum κ fun j => Q j)
  (hN : ∀ (i : ι), IsLocalRing (Module.End A (N i)))
  (hQ : ∀ (j : κ), TauCeti.IsIndecomposableModule A (Q j)) :
  ∃ f, ∀ (i : ι), Nonempty (N i ≃ₗ[A] Q (f i))
Sources
LeanTauCeti.exists_equiv_linearEquiv_of_finset · TauCeti.exists_equiv_linearEquiv_of_iSupIndep · TauCeti.exists_equiv_linearEquiv_of_isLocalRing_end · TauCeti.exists_equiv_linearEquiv_of_directSum · TauCeti.exists_equiv_linearEquiv_of_directSum_of_isLocalRing_end · TauCeti.exists_equiv_linearEquiv_of_directSumEquiv
Uses 2 · Used by 3
Proof usesAzumaya's exchange lemma · Fitting's lemma
Used byThe Krull-Schmidt theorem with no ambient object · Cartan-matrix unimodularity · The general-field Cartan/Ext-Euler identity

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.