Module

TorsionQuotientSupportDimension.lean

Nyll.EtaleFundamentalGroups.Purity.TorsionQuotientSupportDimension

3 declarations indexed from sourceView source ↗

Module documentation

Support dimension after removing maximal-ideal-power torsion

The maximal-ideal-primary component is supported only at the closed point. Positive support dimension supplies a nonclosed point in the support of the coefficient module; this point survives in the quotient. The quotient is consequently nonzero, so its support contains the closed point too. The short exact support formula now identifies the entire supports, and hence their dimensions.

Imports11

Mathlib.Algebra.Exact.Basic
Mathlib.Algebra.Module.Torsion.Basic
Mathlib.Algebra.Module.Torsion.PrimaryComponent
Mathlib.LinearAlgebra.Quotient.Basic
Mathlib.Order.KrullDimension
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.Ideal.Prime
Mathlib.RingTheory.KrullDimension.Module
Mathlib.RingTheory.Spectrum.Prime.Module
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.RingTheory.Support

Imported by2

theorem

support_primaryComponent_maximalIdeal_subset_closedPoint

L39 ↗

EtaleFundamentalGroups.Purity.support_primaryComponent_maximalIdeal_subset_closedPoint

Source context 5 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v
open IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem support_primaryComponent_maximalIdeal_subset_closedPoint :
    Module.support R (Ideal.primaryComponent M (maximalIdeal R)) ⊆
      {closedPoint R}

theorem

support_quotient_primaryComponent_maximalIdeal_eq_of_supportDim_pos

L62 ↗

EtaleFundamentalGroups.Purity.support_quotient_primaryComponent_maximalIdeal_eq_of_supportDim_pos

Documentation

Removing maximal-ideal-power torsion preserves support whenever the original module has positive support dimension.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v
open IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem support_quotient_primaryComponent_maximalIdeal_eq_of_supportDim_pos
    (hpos : 0 < Module.supportDim R M) :
    Module.support R (M ⧸ Ideal.primaryComponent M (maximalIdeal R)) =
      Module.support R M

theorem

supportDim_quotient_primaryComponent_maximalIdeal_eq_of_pos

L96 ↗

EtaleFundamentalGroups.Purity.supportDim_quotient_primaryComponent_maximalIdeal_eq_of_pos

Documentation

Quotienting by the maximal-ideal-primary component preserves every positive support dimension.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v
open IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem supportDim_quotient_primaryComponent_maximalIdeal_eq_of_pos
    (hpos : 0 < Module.supportDim R M) :
    Module.supportDim R (M ⧸ Ideal.primaryComponent M (maximalIdeal R)) =
      Module.supportDim R M

Module documentation

Support dimension after removing maximal-ideal-power torsion

Declarations

support_primaryComponent_maximalIdeal_subset_closedPoint

support_quotient_primaryComponent_maximalIdeal_eq_of_supportDim_pos

supportDim_quotient_primaryComponent_maximalIdeal_eq_of_pos