Module

IdealQuotientMayerVietorisExt.lean

Nyll.EtaleFundamentalGroups.Purity.IdealQuotientMayerVietorisExt

11 declarations indexed from sourceView source ↗

Module documentation

Mayer--Vietoris Ext sequence for two ideal quotients

For ideals I and J, the standard sequence

0 → R/(I ∩ J) → R/I ⊕ R/J → R/(I + J) → 0

is short exact. Applying contravariant derived Ext gives its six-term exact sequence. This is the finite-stage algebraic input for a future Mayer--Vietoris construction in local cohomology; no comparison with the legacy Ext colimit used by localCohomology is asserted here.

Imports4

Mathlib.Algebra.Category.ModuleCat.Ext.HasExt
Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Mathlib.Tactic.Abel
Mathlib.RingTheory.Ideal.Quotient.Defs

Imported by2

def

idealQuotientMapOfLE

L36 ↗

EtaleFundamentalGroups.idealQuotientMapOfLE

Documentation

The linear map between ideal quotients induced by an inclusion.

Source context 5 commands

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

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

Lean source · statement

def idealQuotientMapOfLE {I J : Ideal R} (h : I ≤ J) :
    (R ⧸ I) →ₗ[R] (R ⧸ J)

theorem

idealQuotientMapOfLE_mk

L41 ↗

EtaleFundamentalGroups.idealQuotientMapOfLE_mk

Source context 5 commands

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

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

Lean source · statement

theorem idealQuotientMapOfLE_mk {I J : Ideal R} (h : I ≤ J) (r : R) :
    idealQuotientMapOfLE h (Submodule.Quotient.mk r) =
      Submodule.Quotient.mk r

def

idealQuotientMayerVietorisDiagonal

L48 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisDiagonal

Documentation

The diagonal map from the quotient by the intersection to the product of the two quotients.

Source context 5 commands

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

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

Lean source · statement

def idealQuotientMayerVietorisDiagonal (I J : Ideal R) :
    (R ⧸ I ⊓ J) →ₗ[R] (R ⧸ I) × (R ⧸ J)

def

idealQuotientMayerVietorisDifference

L55 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisDifference

Documentation

The difference map from the product of the two quotients to the quotient by their sum.

Source context 5 commands

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

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

Lean source · statement

def idealQuotientMayerVietorisDifference (I J : Ideal R) :
    ((R ⧸ I) × (R ⧸ J)) →ₗ[R] (R ⧸ I ⊔ J)

theorem

idealQuotientMayerVietorisDifference_comp_diagonal

L62 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisDifference_comp_diagonal

Source context 5 commands

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

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

Lean source · statement

theorem idealQuotientMayerVietorisDifference_comp_diagonal
    (I J : Ideal R) :
    (idealQuotientMayerVietorisDifference I J).comp
        (idealQuotientMayerVietorisDiagonal I J) = 0

theorem

idealQuotientMayerVietorisDiagonal_injective

L74 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisDiagonal_injective

Source context 5 commands

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

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

Lean source · statement

theorem idealQuotientMayerVietorisDiagonal_injective (I J : Ideal R) :
    Function.Injective (idealQuotientMayerVietorisDiagonal I J)

theorem

idealQuotientMayerVietorisDifference_surjective

L90 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisDifference_surjective

Source context 5 commands

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

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

Lean source · statement

theorem idealQuotientMayerVietorisDifference_surjective (I J : Ideal R) :
    Function.Surjective (idealQuotientMayerVietorisDifference I J)

theorem

idealQuotientMayerVietoris_functionExact

L100 ↗

EtaleFundamentalGroups.idealQuotientMayerVietoris_functionExact

Source context 5 commands

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

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

Lean source · statement

theorem idealQuotientMayerVietoris_functionExact (I J : Ideal R) :
    Function.Exact (idealQuotientMayerVietorisDiagonal I J)
      (idealQuotientMayerVietorisDifference I J)

def

idealQuotientMayerVietorisShortComplex

L142 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisShortComplex

Documentation

The standard Mayer--Vietoris short complex of ideal quotients.

Source context 5 commands

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

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

Lean source · statement

def idealQuotientMayerVietorisShortComplex (I J : Ideal R) :
    ShortComplex (ModuleCat.{u} R)

theorem

idealQuotientMayerVietorisShortComplex_shortExact

L150 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisShortComplex_shortExact

Documentation

The standard Mayer--Vietoris sequence of ideal quotients is short exact.

Source context 5 commands

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

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

Lean source · statement

theorem idealQuotientMayerVietorisShortComplex_shortExact (I J : Ideal R) :
    (idealQuotientMayerVietorisShortComplex I J).ShortExact

theorem

idealQuotientMayerVietorisExtSequence_exact

L159 ↗

EtaleFundamentalGroups.idealQuotientMayerVietorisExtSequence_exact

Documentation

Contravariant derived Ext sends the ideal-quotient Mayer--Vietoris short exact sequence to its exact six-term sequence in adjacent degrees.

Source context 5 commands

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

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

Lean source · full declaration

theorem idealQuotientMayerVietorisExtSequence_exact
    (I J : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) :
    (CategoryTheory.Abelian.Ext.contravariantSequence
      (idealQuotientMayerVietorisShortComplex_shortExact I J)
      M i (i + 1) (by omega)).Exact :=
  CategoryTheory.Abelian.Ext.contravariantSequence_exact
    (idealQuotientMayerVietorisShortComplex_shortExact I J)
    M i (i + 1) (by omega)

Module documentation

Mayer--Vietoris Ext sequence for two ideal quotients

Declarations