Module

IdealPowerTorsionSum.lean

Nyll.EtaleFundamentalGroups.Purity.IdealPowerTorsionSum

5 declarations indexed from sourceView source ↗

Module documentation

Power torsion for the sum of two ideals

The binomial bound (I + J)^(n + m) ≤ I^n + J^m identifies power torsion for a sum with the intersection of the two power-torsion submodules. This also constructs the linear equivalence needed to iterate principal torsion in the finite Čech complex.

Imports3

Mathlib.Algebra.Module.Torsion.PrimaryComponent
Mathlib.RingTheory.Ideal.Operations
Mathlib.Algebra.Module.Submodule.Equiv

Imported by3

theorem

primaryComponent_ideal_sup

L29 ↗

EtaleFundamentalGroups.Purity.primaryComponent_ideal_sup

Documentation

Power torsion for a sum is the intersection of the power-torsion submodules for the two summands.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
variable (M : Type u) [AddCommGroup M] [Module R M]

Lean source · statement

theorem primaryComponent_ideal_sup (I J : Ideal R) :
    Ideal.primaryComponent M (I ⊔ J) =
      Ideal.primaryComponent M I ⊓ Ideal.primaryComponent M J

theorem

primaryComponent_submodule

L51 ↗

EtaleFundamentalGroups.Purity.primaryComponent_submodule

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
variable (M : Type u) [AddCommGroup M] [Module R M]

Lean source · statement

theorem primaryComponent_submodule (N : Submodule R M) (J : Ideal R) :
    Ideal.primaryComponent N J = (Ideal.primaryComponent M J).comap N.subtype

theorem

primaryComponent_iterated_eq_comap

L64 ↗

EtaleFundamentalGroups.Purity.primaryComponent_iterated_eq_comap

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
variable (M : Type u) [AddCommGroup M] [Module R M]

Lean source · statement

theorem primaryComponent_iterated_eq_comap (I J : Ideal R) :
    Ideal.primaryComponent (Ideal.primaryComponent M I) J =
      (Ideal.primaryComponent M (I ⊔ J)).comap (Ideal.primaryComponent M I).subtype

def

primaryComponentIteratedLinearEquiv

L76 ↗

EtaleFundamentalGroups.Purity.primaryComponentIteratedLinearEquiv

Documentation

Iterating ideal-power torsion is canonically equivalent to torsion for the sum ideal.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
variable (M : Type u) [AddCommGroup M] [Module R M]

Lean source · statement

def primaryComponentIteratedLinearEquiv (I J : Ideal R) :
    Ideal.primaryComponent (Ideal.primaryComponent M I) J ≃ₗ[R]
      Ideal.primaryComponent M (I ⊔ J)

theorem

primaryComponentIteratedLinearEquiv_apply_val

L84 ↗

EtaleFundamentalGroups.Purity.primaryComponentIteratedLinearEquiv_apply_val

Documentation

The iterated torsion equivalence preserves the underlying vector.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
variable (M : Type u) [AddCommGroup M] [Module R M]

Lean source · statement

theorem primaryComponentIteratedLinearEquiv_apply_val (I J : Ideal R)
    (z : Ideal.primaryComponent (Ideal.primaryComponent M I) J) :
    (primaryComponentIteratedLinearEquiv M I J z : M) = (z.1 : M)

Module documentation

Power torsion for the sum of two ideals

Declarations

primaryComponent_ideal_sup

primaryComponent_submodule

primaryComponent_iterated_eq_comap

primaryComponentIteratedLinearEquiv

primaryComponentIteratedLinearEquiv_apply_val