Module

IdealQuotientMayerVietorisPowers.lean

Nyll.EtaleFundamentalGroups.Purity.IdealQuotientMayerVietorisPowers

11 declarations indexed from sourceView source ↗

Module documentation

Power-compatible Mayer--Vietoris complexes of ideal quotients

This file makes the finite-stage ideal-quotient Mayer--Vietoris sequence functorial in inclusions of both ideals. In particular, the sequences for the powers of two fixed ideals form a diagram indexed by ℕᵒᵖ. This is the source-level compatibility needed before applying contravariant Ext and filtered colimits in a local-cohomology Mayer--Vietoris construction.

Imports2

Nyll.EtaleFundamentalGroups.Purity.IdealQuotientMayerVietorisExt
Mathlib.RingTheory.Ideal.Operations

Imported by2

def

idealQuotientMayerVietorisProductMap

L31 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisProductMap

Documentation

The product of the quotient maps induced by inclusions of two ideals.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

def idealQuotientMayerVietorisProductMap
    {I J I' J' : Ideal R} (hI : I ≤ I') (hJ : J ≤ J') :
    ((R ⧸ I) × (R ⧸ J)) →ₗ[R] ((R ⧸ I') × (R ⧸ J'))

theorem

idealQuotientMayerVietorisProductMap_apply

L37 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisProductMap_apply

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem idealQuotientMayerVietorisProductMap_apply
    {I J I' J' : Ideal R} (hI : I ≤ I') (hJ : J ≤ J')
    (z : (R ⧸ I) × (R ⧸ J)) :
    idealQuotientMayerVietorisProductMap hI hJ z =
      (idealQuotientMapOfLE hI z.1, idealQuotientMapOfLE hJ z.2)

theorem

idealQuotientMapOfLE_comp

L45 ↗

EtaleFundamentalGroups.idealQuotientMapOfLE_comp

Documentation

Quotient maps induced by ideal inclusions compose.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem idealQuotientMapOfLE_comp
    {I I' I'' : Ideal R} (h : I ≤ I') (h' : I' ≤ I'') :
    (idealQuotientMapOfLE h').comp (idealQuotientMapOfLE h) =
      idealQuotientMapOfLE (h.trans h')

theorem

idealQuotientMapOfLE_refl

L55 ↗

EtaleFundamentalGroups.idealQuotientMapOfLE_refl

Documentation

The quotient map induced by a reflexive inclusion is the identity.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem idealQuotientMapOfLE_refl (I : Ideal R) :
    idealQuotientMapOfLE (le_refl I) = LinearMap.id

theorem

idealQuotientMayerVietorisDiagonal_naturality

L64 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisDiagonal_naturality

Documentation

The diagonal maps in the ideal-quotient Mayer--Vietoris complexes are natural in inclusions of both ideals.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem idealQuotientMayerVietorisDiagonal_naturality
    {I J I' J' : Ideal R} (hI : I ≤ I') (hJ : J ≤ J') :
    (idealQuotientMayerVietorisDiagonal I' J').comp
        (idealQuotientMapOfLE (inf_le_inf hI hJ)) =
      (idealQuotientMayerVietorisProductMap hI hJ).comp
        (idealQuotientMayerVietorisDiagonal I J)

theorem

idealQuotientMayerVietorisDifference_naturality

L77 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisDifference_naturality

Documentation

The difference maps in the ideal-quotient Mayer--Vietoris complexes are natural in inclusions of both ideals.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem idealQuotientMayerVietorisDifference_naturality
    {I J I' J' : Ideal R} (hI : I ≤ I') (hJ : J ≤ J') :
    (idealQuotientMayerVietorisDifference I' J').comp
        (idealQuotientMayerVietorisProductMap hI hJ) =
      (idealQuotientMapOfLE (sup_le_sup hI hJ)).comp
        (idealQuotientMayerVietorisDifference I J)

def

idealQuotientMayerVietorisHom

L92 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisHom

Documentation

Inclusions of two pairs of ideals induce a morphism between their ideal-quotient Mayer--Vietoris short complexes.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

def idealQuotientMayerVietorisHom
    {I J I' J' : Ideal R} (hI : I ≤ I') (hJ : J ≤ J') :
    idealQuotientMayerVietorisShortComplex I J ⟶
      idealQuotientMayerVietorisShortComplex I' J'

theorem

idealQuotientMayerVietorisHom_refl

L120 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisHom_refl

Documentation

The morphism induced by reflexive inclusions is the identity morphism of the Mayer--Vietoris short complex.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem idealQuotientMayerVietorisHom_refl (I J : Ideal R) :
    idealQuotientMayerVietorisHom (le_refl I) (le_refl J) =
      𝟙 (idealQuotientMayerVietorisShortComplex I J)

theorem

idealQuotientMayerVietorisHom_comp

L137 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisHom_comp

Documentation

Mayer--Vietoris morphisms induced by inclusions compose.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem idealQuotientMayerVietorisHom_comp
    {I₀ J₀ I₁ J₁ I₂ J₂ : Ideal R}
    (hI₀₁ : I₀ ≤ I₁) (hJ₀₁ : J₀ ≤ J₁)
    (hI₁₂ : I₁ ≤ I₂) (hJ₁₂ : J₁ ≤ J₂) :
    idealQuotientMayerVietorisHom hI₀₁ hJ₀₁ ≫
        idealQuotientMayerVietorisHom hI₁₂ hJ₁₂ =
      idealQuotientMayerVietorisHom (hI₀₁.trans hI₁₂)
        (hJ₀₁.trans hJ₁₂)

def

idealQuotientMayerVietorisPowersDiagram

L159 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisPowersDiagram

Documentation

The standard quotient Mayer--Vietoris short complexes for simultaneous powers Iⁿ and Jⁿ, together with their source-produced transition maps.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]

Lean source · full declaration

def idealQuotientMayerVietorisPowersDiagram (I J : Ideal R) :
    ℕᵒᵖ ⥤ ShortComplex (ModuleCat.{u} R) where
  obj n := idealQuotientMayerVietorisShortComplex
    (I ^ unop n) (J ^ unop n)
  map {m n} f := idealQuotientMayerVietorisHom
    (Ideal.pow_le_pow_right f.unop.down.down)
    (Ideal.pow_le_pow_right f.unop.down.down)
  map_id n := by
    apply idealQuotientMayerVietorisHom_refl
  map_comp f g := by
    rw [idealQuotientMayerVietorisHom_comp]

theorem

idealQuotientMayerVietorisPowersDiagram_obj_shortExact

L173 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisPowersDiagram_obj_shortExact

Documentation

Every object of the powers diagram is the standard short exact ideal-quotient Mayer--Vietoris sequence.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]

Lean source · statement

theorem idealQuotientMayerVietorisPowersDiagram_obj_shortExact
    (I J : Ideal R) (n : ℕᵒᵖ) :
    ((idealQuotientMayerVietorisPowersDiagram I J).obj n).ShortExact

Module documentation

Power-compatible Mayer--Vietoris complexes of ideal quotients

Declarations