NYLL
Module

IdealQuotientMayerVietorisDerivedExtColimit.lean

Nyll.EtaleFundamentalGroups.Purity.IdealQuotientMayerVietorisDerivedExtColimit
8 declarations indexed from sourceView source ↗

Module documentation

Filtered colimits of derived-Ext Mayer--Vietoris sequences

An objectwise exact diagram of finite composable sequences determines an exact short complex of functors on every adjacent three-term window. Exact filtered colimits then give the corresponding exact short complex of colimit objects. The final section applies this construction to the derived-Ext Mayer--Vietoris diagram along simultaneous ideal powers.

Imports4
Imported by3

Declarations

def

exactComposableArrowsDiagramAdjacentShortComplex

L39 ↗
EtaleFundamentalGroups.exactComposableArrowsDiagramAdjacentShortComplex
Documentation

The adjacent three-term window beginning at k in an objectwise exact diagram of n composable arrows, regarded as a short complex in the functor category.

Source context 8 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section AdjacentWindow
variable {C : Type u} [Category.{v} C] [Abelian C]
variable {D : Type*} [Category D]
variable {n : ℕ}
Lean source · full declaration
def exactComposableArrowsDiagramAdjacentShortComplex
    (Q : D ⥤ ComposableArrows C n) (hQ : ∀ d, (Q.obj d).Exact)
    (k : ℕ) (hk : k + 2 ≤ n) : ShortComplex (D ⥤ C) where
  X₁ := Q ⋙ (evaluation (Fin (n + 1)) C).obj ⟨k, by omega⟩
  X₂ := Q ⋙ (evaluation (Fin (n + 1)) C).obj ⟨k + 1, by omega⟩
  X₃ := Q ⋙ (evaluation (Fin (n + 1)) C).obj ⟨k + 2, by omega⟩
  f :=
    { app := fun d => (Q.obj d).map' k (k + 1)
      naturality := fun _ _ φ =>
        (ComposableArrows.naturality' (Q.map φ) k (k + 1)).symm }
  g :=
    { app := fun d => (Q.obj d).map' (k + 1) (k + 2)
      naturality := fun _ _ φ =>
        (ComposableArrows.naturality' (Q.map φ) (k + 1) (k + 2)).symm }
  zero := by
    ext d
    exact (hQ d).toIsComplex.zero k hk
theorem

exactComposableArrowsDiagramAdjacentShortComplex_exact

L59 ↗
EtaleFundamentalGroups.exactComposableArrowsDiagramAdjacentShortComplex_exact
Documentation

Objectwise exactness of the finite sequences produces exactness of every adjacent short complex in the functor category.

Source context 8 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section AdjacentWindow
variable {C : Type u} [Category.{v} C] [Abelian C]
variable {D : Type*} [Category D]
variable {n : ℕ}
Lean source · statement
theorem exactComposableArrowsDiagramAdjacentShortComplex_exact
    (Q : D ⥤ ComposableArrows C n) (hQ : ∀ d, (Q.obj d).Exact)
    (k : ℕ) (hk : k + 2 ≤ n) :
    (exactComposableArrowsDiagramAdjacentShortComplex Q hQ k hk).Exact
def

shortComplexExactColimit

L83 ↗
EtaleFundamentalGroups.shortComplexExactColimit
Documentation

The short complex obtained by applying the chosen colimit functor to all three terms and both maps of a short complex of diagrams.

Source context 8 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section ExactColimit
variable {C : Type u} [Category.{v} C] [Abelian C]
variable {D : Type*} [Category D]
variable [HasColimitsOfShape D C] [HasExactColimitsOfShape D C]
Lean source · statement
def shortComplexExactColimit (S : ShortComplex (D ⥤ C)) : ShortComplex C
theorem

shortComplexExactColimit_exact

L96 ↗
EtaleFundamentalGroups.shortComplexExactColimit_exact
Documentation

Exact colimits preserve exactness of the standard colimit short complex. This is the direct colim.exact_mapShortComplex interface used by the Mayer--Vietoris powers diagram.

Source context 8 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe w v u
section ExactColimit
variable {C : Type u} [Category.{v} C] [Abelian C]
variable {D : Type*} [Category D]
variable [HasColimitsOfShape D C] [HasExactColimitsOfShape D C]
Lean source · statement
theorem shortComplexExactColimit_exact
    (S : ShortComplex (D ⥤ C)) (hS : S.Exact) :
    (shortComplexExactColimit S).Exact
def

idealQuotientMayerVietorisDerivedExtPowersAdjacentShortComplex

L112 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersAdjacentShortComplex
Documentation

An adjacent three-term window in the six-term derived-Ext Mayer--Vietoris diagram along simultaneous powers of I and J.

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 IdealPowersColimit
variable {R : Type u} [CommRing R]
Lean source · statement
def idealQuotientMayerVietorisDerivedExtPowersAdjacentShortComplex
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁)
    (k : ℕ) (hk : k + 2 ≤ 5) :
    ShortComplex ((ℕᵒᵖ)ᵒᵖ ⥤ AddCommGrpCat.{u})
theorem

idealQuotientMayerVietorisDerivedExtPowersAdjacentShortComplex_exact

L125 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersAdjacentShortComplex_exact
Documentation

Every adjacent three-term window of the powers-derived-Ext diagram is exact in the functor category.

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 IdealPowersColimit
variable {R : Type u} [CommRing R]
Lean source · statement
theorem idealQuotientMayerVietorisDerivedExtPowersAdjacentShortComplex_exact
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁)
    (k : ℕ) (hk : k + 2 ≤ 5) :
    (idealQuotientMayerVietorisDerivedExtPowersAdjacentShortComplex
      I J M n₀ n₁ h k hk).Exact
def

idealQuotientMayerVietorisDerivedExtPowersAdjacentColimitShortComplex

L139 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersAdjacentColimitShortComplex
Documentation

The chosen filtered colimits of an adjacent three-term window in the powers-derived-Ext diagram.

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 IdealPowersColimit
variable {R : Type u} [CommRing R]
Lean source · statement
def idealQuotientMayerVietorisDerivedExtPowersAdjacentColimitShortComplex
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁)
    (k : ℕ) (hk : k + 2 ≤ 5) :
    ShortComplex AddCommGrpCat.{u}
theorem

idealQuotientMayerVietorisDerivedExtPowersAdjacentColimitShortComplex_exact

L150 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersAdjacentColimitShortComplex_exact
Documentation

Filtered colimits preserve exactness of every adjacent three-term window in the powers-derived-Ext Mayer--Vietoris diagram.

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 IdealPowersColimit
variable {R : Type u} [CommRing R]
Lean source · statement
theorem
    idealQuotientMayerVietorisDerivedExtPowersAdjacentColimitShortComplex_exact
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁)
    (k : ℕ) (hk : k + 2 ≤ 5) :
    (idealQuotientMayerVietorisDerivedExtPowersAdjacentColimitShortComplex
      I J M n₀ n₁ h k hk).Exact

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