Module

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

TheoremThe free part of the structure theorem#

In a finitely generated graded k[X]-module over a field on which X lowers degree by d ≠ 0, the torsion submodule has a complement spanned by a k[X]-linearly independent family of homogeneous elements: M is its torsion submodule plus a graded free module, one X-tower for each element of the family.

TauCeti.InternalGrading.exists_linearIndependent_isCompl_torsion.{u, u_1} {k : Type u_1}
  {M : Type u} [Field k] [AddCommGroup M] [_root_.Module k M] [_root_.Module (Polynomial k) M]
  [IsScalarTower k (Polynomial k) M] [Module.Finite (Polynomial k) M]
  {G : TauCeti.InternalGrading k M ℤ} {d : ℕ} (hd : d ≠ 0)
  (hX : ∀ ⦃p : ℤ⦄ ⦃x : M⦄, x ∈ G.piece ℤ p → Polynomial.X • x ∈ G.piece ℤ (p - ↑d)) :
  ∃ ι b deg,
    (∀ (i : ι), b i ∈ G.piece ℤ (deg i)) ∧
      LinearIndependent (Polynomial k) b ∧
        IsCompl (Submodule.torsion (Polynomial k) M) (Submodule.span (Polynomial k) (Set.range b))
Lean

Formalized in Tau Ceti as TauCeti.InternalGrading.exists_linearIndependent_isCompl_torsion.

Sources
LeanTauCeti.InternalGrading.exists_linearIndependent_isCompl_torsion
Used by 1
Used byThe structure theorem for finitely generated graded k[X]-modules

TheoremThe Ikeda--Nakayama annihilator criterion, for a left self-injective ring#

if every r with r * a i = 0 for all i also satisfies r * x = 0, then x lies in the right ideal generated by the a i.

TauCeti.exists_eq_sum_mul_of_forall_mul_eq_zero.{u, w} {R : Type u} [Ring R] {ι : Type w}
  [Fintype ι] {a : ι → R} {x : R} [Module.Injective R R]
  (h : ∀ (r : R), (∀ (i : ι), r * a i = 0) → r * x = 0) : ∃ c, x = ∑ i, a i * c i
Lean

Formalized in Tau Ceti as TauCeti.exists_eq_sum_mul_of_forall_mul_eq_zero.

Other forms

The Ikeda--Nakayama annihilator criterion, for a right self-injective ring. Formalized in Tau Ceti as TauCeti.exists_eq_sum_mul_of_forall_mul_eq_zero'.

TauCeti.exists_eq_sum_mul_of_forall_mul_eq_zero'.{u, w} {R : Type u} [Ring R] {ι : Type w}
  [Fintype ι] {a : ι → R} {x : R} [Module.Injective Rᵐᵒᵖ R]
  (h : ∀ (r : R), (∀ (i : ι), a i * r = 0) → x * r = 0) : ∃ c, x = ∑ i, c i * a i
Sources
LeanTauCeti.exists_eq_sum_mul_of_forall_mul_eq_zero · TauCeti.exists_eq_sum_mul_of_forall_mul_eq_zero'

TheoremNakayama's lemma for a nilpotent ideal#

If I is a nilpotent ideal then I • M is superfluous in M.

Unlike TauCeti.isSuperfluous_jacobson, which asks the submodule lattice of M to be coatomic (for instance M finitely generated) and takes the radical of M, nilpotence of I buys the conclusion for an arbitrary module: a submodule K with I • M ⊔ K = ⊤ absorbs I ^ k • M into I ^ (k + 1) • M for every k, and a power of I vanishes.

TauCeti.isSuperfluous_smul_top_of_isNilpotent.{u, v} {R : Type u} {M : Type v} [Semiring R]
  [AddCommMonoid M] [_root_.Module R M] {I : Ideal R} (hI : IsNilpotent I) :
  TauCeti.IsSuperfluous (I • ⊤)
Lean

Formalized in Tau Ceti as TauCeti.isSuperfluous_smul_top_of_isNilpotent.

Sources
LeanTauCeti.isSuperfluous_smul_top_of_isNilpotent
Used by 2
Used byModuleCat.exists_isAlmostSplit_X₃_eq_iff · The Auslander–Reiten theorem, existence

TheoremSchanuel's lemma in automorphism form#

If a : A → E and b : B → E are maps from projective modules with the same range, then a ∘ fst and b ∘ snd, as maps A × B → E, differ by an automorphism of A × B.

For surjective a and b this is Schanuel's lemma: the automorphism carries ker (a ∘ fst) = ker a × B onto ker (b ∘ snd) = A × ker b.

TauCeti.exists_linearEquiv_comp_fst_eq_comp_snd_comp.{u_1, u_2, u_3, u_4} {R : Type u_1}
  [Semiring R] {A : Type u_2} {B : Type u_3} {E : Type u_4} [AddCommMonoid E] [_root_.Module R E]
  [AddCommGroup A] [_root_.Module R A] [AddCommGroup B] [_root_.Module R B] [Module.Projective R A]
  [Module.Projective R B] {a : A →ₗ[R] E} {b : B →ₗ[R] E} (h : a.range = b.range) :
  ∃ e, a ∘ₗ LinearMap.fst R A B = b ∘ₗ LinearMap.snd R A B ∘ₗ ↑e
Lean

Formalized in Tau Ceti as TauCeti.exists_linearEquiv_comp_fst_eq_comp_snd_comp.

Sources
LeanTauCeti.exists_linearEquiv_comp_fst_eq_comp_snd_comp
Used by 2
Used byThe finite level of the generator theorem (NSW, proof of (7.4.1)) · Nakayama–Rim, Sylow form

TheoremSerre's lemma on the Tate module#

An endomorphism of finite order of T_p A that induces the identity on A[p ^ k], with p ^ k ≥ 3, is the identity.

TauCeti.TateModule.eq_one_of_isOfFinOrder_of_forall_proj_eq.{u_1} {p : ℕ} {A : Type u_1}
  [AddCommGroup A] [hp : Fact (Nat.Prime p)] {φ : Module.End ℤ_[p] (TauCeti.TateModule p A)}
  (hφ : IsOfFinOrder φ) {k : ℕ} (hk : 3 ≤ p ^ k)
  (hfix :
    ∀ (t : TauCeti.TateModule p A),
      (TauCeti.TateModule.proj k) (φ t) = (TauCeti.TateModule.proj k) t) :
  φ = 1
Lean

Formalized in Tau Ceti as TauCeti.TateModule.eq_one_of_isOfFinOrder_of_forall_proj_eq.

Sources
LeanTauCeti.TateModule.eq_one_of_isOfFinOrder_of_forall_proj_eq
Uses 1 · Used by 1
Proof usesSerre's lemma
Used bySerre's lemma for the ℓ-adic representation

TheoremStructure theorem for finitely generated modules over a discrete valuation ring#

A finitely generated module over a discrete valuation ring R with uniformizer ϖ is isomorphic to R ^ n × ∏ i : Fin m, R ⧸ (ϖ ^ e i) with every exponent e i positive.

TauCeti.Module.equiv_pi_prod_pi_quotient_span_pow.{u, v} (R : Type u) (M : Type v) [CommRing R]
  [IsDomain R] [IsDiscreteValuationRing R] [AddCommGroup M] [_root_.Module R M] [Module.Finite R M]
  {ϖ : R} (hϖ : Irreducible ϖ) :
  ∃ n m e,
    (∀ (i : Fin m), 0 < e i) ∧ Nonempty (M ≃ₗ[R] (Fin n → R) × ((i : Fin m) → R ⧸ R ∙ ϖ ^ e i))
Lean

Formalized in Tau Ceti as TauCeti.Module.equiv_pi_prod_pi_quotient_span_pow.

Sources
LeanTauCeti.Module.equiv_pi_prod_pi_quotient_span_pow
Used by 1
Used byStructure theorem for topologically finitely generated abelian pro-p groups

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.