NYLL
Module

IdealQuotientMayerVietorisDerivedExtPowers.lean

Nyll.EtaleFundamentalGroups.Purity.IdealQuotientMayerVietorisDerivedExtPowers
12 declarations indexed from sourceView source ↗

Module documentation

Derived-Ext Mayer--Vietoris sequences along powers

The contravariant six-term derived-Ext sequence of a short exact complex is functorial in morphisms of short complexes. Applying that naturality to the power-compatible ideal-quotient Mayer--Vietoris complexes produces the exact sequence diagram that precedes an AB5 filtered-colimit argument.

Imports1
Imported by3

Declarations

def

derivedExtContravariantMap

L32 ↗
EtaleFundamentalGroups.derivedExtContravariantMap
Documentation

The map on derived Ext induced contravariantly by a morphism in the first argument.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section ContravariantSequence
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
Lean source · statement
def derivedExtContravariantMap {X X' : C} (f : X ⟶ X') (Y : C) (n : ℕ) :
    AddCommGrpCat.of (CategoryTheory.Abelian.Ext.{w} X' Y n) ⟶
      AddCommGrpCat.of (CategoryTheory.Abelian.Ext.{w} X Y n)
theorem

derivedExtContravariantMap_id

L40 ↗
EtaleFundamentalGroups.derivedExtContravariantMap_id
Documentation

Contravariant derived-Ext sends an identity to an identity.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section ContravariantSequence
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
Lean source · statement
theorem derivedExtContravariantMap_id (X Y : C) (n : ℕ) :
    derivedExtContravariantMap (𝟙 X) Y n = 𝟙 _
theorem

derivedExtContravariantMap_comp

L48 ↗
EtaleFundamentalGroups.derivedExtContravariantMap_comp
Documentation

Composition law for the contravariant maps on derived Ext.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section ContravariantSequence
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
Lean source · statement
theorem derivedExtContravariantMap_comp
    {X₁ X₂ X₃ : C} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
    (Y : C) (n : ℕ) :
    derivedExtContravariantMap g Y n ≫
        derivedExtContravariantMap f Y n =
      derivedExtContravariantMap (f ≫ g) Y n
theorem

derivedExtContravariantMap_square

L65 ↗
EtaleFundamentalGroups.derivedExtContravariantMap_square
Documentation

Contravariant derived-Ext maps carry a commutative square in the first argument to a commutative square of Ext groups.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section ContravariantSequence
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
Lean source · statement
theorem derivedExtContravariantMap_square
    {X₁ X₂ X₁' X₂' : C}
    (a : X₁ ⟶ X₂) (b : X₁' ⟶ X₂')
    (f₁ : X₁ ⟶ X₁') (f₂ : X₂ ⟶ X₂')
    (hsq : f₁ ≫ b = a ≫ f₂) (Y : C) (n : ℕ) :
    AddCommGrpCat.ofHom
          ((CategoryTheory.Abelian.Ext.mk₀ b).precomp Y (zero_add n)) ≫
        derivedExtContravariantMap f₁ Y n =
      derivedExtContravariantMap f₂ Y n ≫
        AddCommGrpCat.ofHom
          ((CategoryTheory.Abelian.Ext.mk₀ a).precomp Y (zero_add n))
theorem

derivedExtConnectingMap_naturality

L91 ↗
EtaleFundamentalGroups.derivedExtConnectingMap_naturality
Documentation

The connecting morphism in the contravariant derived-Ext sequence is natural in morphisms of short exact complexes.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section ContravariantSequence
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
Lean source · statement
theorem derivedExtConnectingMap_naturality
    {S₁ S₂ : ShortComplex C}
    (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂)
    (Y : C) (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) :
    AddCommGrpCat.ofHom (h₂.extClass.precomp Y h) ≫
        derivedExtContravariantMap f.τ₃ Y n₁ =
      derivedExtContravariantMap f.τ₁ Y n₀ ≫
        AddCommGrpCat.ofHom (h₁.extClass.precomp Y h)
def

derivedExtContravariantSequenceMap

L121 ↗
EtaleFundamentalGroups.derivedExtContravariantSequenceMap
Documentation

A morphism of short exact complexes induces, contravariantly, a morphism between their six-term derived-Ext sequences.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section ContravariantSequence
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
Lean source · statement
def derivedExtContravariantSequenceMap
    {S₁ S₂ : ShortComplex C}
    (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂)
    (Y : C) (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) :
    CategoryTheory.Abelian.Ext.contravariantSequence h₂ Y n₀ n₁ h ⟶
      CategoryTheory.Abelian.Ext.contravariantSequence h₁ Y n₀ n₁ h
theorem

derivedExtContravariantSequenceMap_id

L147 ↗
EtaleFundamentalGroups.derivedExtContravariantSequenceMap_id
Documentation

The contravariant map of six-term sequences induced by an identity is the identity.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section ContravariantSequence
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
Lean source · statement
theorem derivedExtContravariantSequenceMap_id
    {S : ShortComplex C} (hS : S.ShortExact)
    (Y : C) (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) :
    derivedExtContravariantSequenceMap hS hS (𝟙 S) Y n₀ n₁ h = 𝟙 _
theorem

derivedExtContravariantSequenceMap_comp

L167 ↗
EtaleFundamentalGroups.derivedExtContravariantSequenceMap_comp
Documentation

Composition law for the contravariant maps of six-term sequences.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section ContravariantSequence
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
Lean source · statement
theorem derivedExtContravariantSequenceMap_comp
    {S₁ S₂ S₃ : ShortComplex C}
    (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (h₃ : S₃.ShortExact)
    (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃)
    (Y : C) (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) :
    derivedExtContravariantSequenceMap h₂ h₃ g Y n₀ n₁ h ≫
        derivedExtContravariantSequenceMap h₁ h₂ f Y n₀ n₁ h =
      derivedExtContravariantSequenceMap h₁ h₃ (f ≫ g) Y n₀ n₁ h
def

derivedExtContravariantSequenceDiagram

L205 ↗
EtaleFundamentalGroups.derivedExtContravariantSequenceDiagram
Documentation

An objectwise short exact diagram gives a contravariant diagram of its six-term derived-Ext sequences.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section ContravariantSequence
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
variable {D : Type*} [Category D]
Lean source · full declaration
def derivedExtContravariantSequenceDiagram
    (F : D ⥤ ShortComplex C) (hF : ∀ d, (F.obj d).ShortExact)
    (Y : C) (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) :
    Dᵒᵖ ⥤ ComposableArrows AddCommGrpCat.{w} 5 where
  obj d := CategoryTheory.Abelian.Ext.contravariantSequence
    (hF (unop d)) Y n₀ n₁ h
  map {d e} f := derivedExtContravariantSequenceMap
    (hF (unop e)) (hF (unop d)) (F.map f.unop) Y n₀ n₁ h
  map_id d := by
    dsimp
    rw [F.map_id]
    apply derivedExtContravariantSequenceMap_id
  map_comp f g := by
    dsimp
    rw [F.map_comp]
    symm
    apply derivedExtContravariantSequenceMap_comp
theorem

derivedExtContravariantSequenceDiagram_obj_exact

L224 ↗
EtaleFundamentalGroups.derivedExtContravariantSequenceDiagram_obj_exact
Documentation

Each six-term sequence in the contravariant diagram is exact.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section ContravariantSequence
variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]
variable {D : Type*} [Category D]
Lean source · statement
theorem derivedExtContravariantSequenceDiagram_obj_exact
    (F : D ⥤ ShortComplex C) (hF : ∀ d, (F.obj d).ShortExact)
    (Y : C) (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) (d : Dᵒᵖ) :
    ((derivedExtContravariantSequenceDiagram F hF Y n₀ n₁ h).obj d).Exact
def

idealQuotientMayerVietorisDerivedExtPowersDiagram

L241 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersDiagram
Documentation

The exact six-term derived-Ext sequences of the ideal-quotient Mayer--Vietoris complexes, assembled along simultaneous powers of I and J. The index category is the opposite of the quotient-complex powers diagram because Ext is contravariant in its first argument.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
def idealQuotientMayerVietorisDerivedExtPowersDiagram
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) :
    (ℕᵒᵖ)ᵒᵖ ⥤ ComposableArrows AddCommGrpCat.{u} 5
theorem

idealQuotientMayerVietorisDerivedExtPowersDiagram_obj_exact

L252 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersDiagram_obj_exact
Documentation

Every object of the powers-derived-Ext diagram is an exact six-term sequence.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section IdealPowers
variable {R : Type u} [CommRing R]
Lean source · statement
theorem idealQuotientMayerVietorisDerivedExtPowersDiagram_obj_exact
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) (d : (ℕᵒᵖ)ᵒᵖ) :
    ((idealQuotientMayerVietorisDerivedExtPowersDiagram
      I J M n₀ n₁ h).obj d).Exact

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.