Module

DerivedLocalCohomologyPrincipalPowerQuotient.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyPrincipalPowerQuotient

6 declarations indexed from sourceView source ↗

Module documentation

Principal ideal-power quotients

For a principal ideal (x), the quotient by its n-th ideal power is canonically the quotient by the submodule x ^ n R. This file records that identification and its compatibility with the standard transition maps between power quotients.

Imports3

Mathlib.Algebra.Homology.LocalCohomology
Mathlib.RingTheory.Regular.Category
Mathlib.RingTheory.QuotSMulTop

Imported by3

theorem

principalIdealPower_submodule_eq_smulTop

L33 ↗

EtaleFundamentalGroups.principalIdealPower_submodule_eq_smulTop

Documentation

The submodule underlying (x) ^ n is x ^ n R.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
section
variable {R : Type u} [CommRing R]

Lean source · statement

theorem principalIdealPower_submodule_eq_smulTop (x : R) (n : ℕ) :
    ((Ideal.span {x}) ^ n : Submodule R R) =
      x ^ n • (⊤ : Submodule R R)

def

principalPowerQuotientLinearEquiv

L46 ↗

EtaleFundamentalGroups.principalPowerQuotientLinearEquiv

Documentation

The quotient by (x) ^ n as an ideal is canonically the quotient by the submodule x ^ n R.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
section
variable {R : Type u} [CommRing R]

Lean source · statement

def principalPowerQuotientLinearEquiv (x : R) (n : ℕ) :
    (R ⧸ (Ideal.span {x}) ^ n) ≃ₗ[R] QuotSMulTop (x ^ n) R

def

principalPowerQuotientTransition

L53 ↗

EtaleFundamentalGroups.principalPowerQuotientTransition

Documentation

The standard quotient map from the m-th principal ideal-power quotient to the n-th one, for n ≤ m.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
section
variable {R : Type u} [CommRing R]

Lean source · statement

def principalPowerQuotientTransition (x : R) {n m : ℕ} (h : n ≤ m) :
    (R ⧸ (Ideal.span {x}) ^ m) →ₗ[R]
      (R ⧸ (Ideal.span {x}) ^ n)

theorem

principalPowerQuotientTransition_eq_ringModIdeals_map

L60 ↗

EtaleFundamentalGroups.principalPowerQuotientTransition_eq_ringModIdeals_map

Documentation

The preceding map is exactly the map used by the ideal-powers quotient diagram defining local cohomology.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
section
variable {R : Type u} [CommRing R]

Lean source · statement

theorem principalPowerQuotientTransition_eq_ringModIdeals_map
    (x : R) {n m : ℕ} (h : n ≤ m) :
    ModuleCat.ofHom (principalPowerQuotientTransition x h) =
      (localCohomology.ringModIdeals
        (localCohomology.idealPowersDiagram (Ideal.span {x}))).map
          (CategoryTheory.homOfLE h).op

def

quotSMulTopPowerTransition

L70 ↗

EtaleFundamentalGroups.quotSMulTopPowerTransition

Documentation

The corresponding standard quotient map between quotients by the submodules x ^ m R and x ^ n R.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
section
variable {R : Type u} [CommRing R]

Lean source · statement

def quotSMulTopPowerTransition (x : R) {n m : ℕ} (h : n ≤ m) :
    QuotSMulTop (x ^ m) R →ₗ[R] QuotSMulTop (x ^ n) R

theorem

principalPowerQuotientLinearEquiv_transition

L81 ↗

EtaleFundamentalGroups.principalPowerQuotientLinearEquiv_transition

Documentation

The canonical identifications of principal ideal-power quotients commute with their standard transition maps.

Source context 6 commands

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

noncomputable section
open scoped Pointwise
namespace EtaleFundamentalGroups
universe u
section
variable {R : Type u} [CommRing R]

Lean source · statement

theorem principalPowerQuotientLinearEquiv_transition (x : R)
    {n m : ℕ} (h : n ≤ m) :
    (quotSMulTopPowerTransition x h).comp
        (principalPowerQuotientLinearEquiv x m).toLinearMap =
      (principalPowerQuotientLinearEquiv x n).toLinearMap.comp
        (principalPowerQuotientTransition x h)

Module documentation

Principal ideal-power quotients

Declarations

principalIdealPower_submodule_eq_smulTop

principalPowerQuotientLinearEquiv

principalPowerQuotientTransition

principalPowerQuotientTransition_eq_ringModIdeals_map

quotSMulTopPowerTransition

principalPowerQuotientLinearEquiv_transition