NYLL
Module

IdealQuotientMayerVietorisDerivedExtMiddle.lean

Nyll.EtaleFundamentalGroups.Purity.IdealQuotientMayerVietorisDerivedExtMiddle
13 declarations indexed from sourceView source ↗

Module documentation

The middle term of the derived Mayer--Vietoris sequence

The middle object in the ideal-quotient Mayer--Vietoris sequence is a Cartesian product of quotient modules. This file identifies its derived-Ext diagram with the pointwise biproduct of the two ideal-power diagrams. Since filtered colimits in abelian groups are additive, the middle colimit is the biproduct of the two derived local-cohomology objects.

Imports4
Imported by2

Declarations

def

pointwiseBiprodFunctor

L31 ↗
EtaleFundamentalGroups.pointwiseBiprodFunctor
Documentation

The explicit pointwise binary biproduct of two diagrams.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
Lean source · full declaration
def pointwiseBiprodFunctor
    {C : Type u} [Category.{v} C] [Preadditive C]
    [HasBinaryBiproducts C]
    {D : Type w} [Category D]
    (A B : D ⥤ C) : D ⥤ C where
  obj d := A.obj d ⊞ B.obj d
  map f := biprod.map (A.map f) (B.map f)
  map_id d := by ext <;> simp
  map_comp f g := by ext <;> simp
def

diagramOpBiprodIso

L43 ↗
EtaleFundamentalGroups.diagramOpBiprodIso
Documentation

Taking opposites carries a pointwise biproduct diagram to the pointwise biproduct of the opposite diagrams.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
Lean source · statement
def diagramOpBiprodIso
    {C : Type u} [Category.{v} C] [Preadditive C]
    [HasBinaryBiproducts C]
    {D : Type w} [Category D]
    (A B : D ⥤ C) :
    (pointwiseBiprodFunctor A B).op ≅
      pointwiseBiprodFunctor A.op B.op
def

additiveFunctorCompBiprodIso

L69 ↗
EtaleFundamentalGroups.additiveFunctorCompBiprodIso
Documentation

An additive functor carries an explicit pointwise biproduct diagram to the corresponding pointwise biproduct of the composite diagrams.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
Lean source · statement
def additiveFunctorCompBiprodIso
    {C : Type u} [Category.{v} C] [Preadditive C]
    [HasBinaryBiproducts C]
    {E : Type w} [Category E] [Preadditive E]
    [HasBinaryBiproducts E]
    {D : Type*} [Category D]
    (A B : D ⥤ C) (F : C ⥤ E) [F.Additive] :
    pointwiseBiprodFunctor A B ⋙ F ≅
      pointwiseBiprodFunctor (A ⋙ F) (B ⋙ F)
def

pointwiseBiprodFunctorIso

L99 ↗
EtaleFundamentalGroups.pointwiseBiprodFunctorIso
Documentation

The explicit pointwise biproduct diagram is canonically isomorphic to the chosen binary biproduct in the functor category.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
Lean source · statement
def pointwiseBiprodFunctorIso
    {C : Type u} [Category.{v} C] [Preadditive C]
    [HasBinaryBiproducts C]
    {D : Type w} [Category D]
    (A B : D ⥤ C) :
    pointwiseBiprodFunctor A B ≅ A ⊞ B
def

pointwiseBiprodColimitIso

L112 ↗
EtaleFundamentalGroups.pointwiseBiprodColimitIso
Documentation

Colimits carry explicit pointwise binary biproducts to binary biproducts.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
Lean source · statement
def pointwiseBiprodColimitIso
    {C : Type u} [Category.{v} C] [Preadditive C]
    [HasBinaryBiproducts C]
    {D : Type w} [Category D] [HasColimitsOfShape D C]
    (A B : D ⥤ C) :
    colimit (pointwiseBiprodFunctor A B) ≅
      colimit A ⊞ colimit B
instance

derivedExtContravariantFunctor_additive

L127 ↗
EtaleFundamentalGroups.derivedExtContravariantFunctor_additive
Documentation

Derived Ext in its contravariant variable is additive.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
variable {R : Type u} [CommRing R]
Lean source · statement
instance derivedExtContravariantFunctor_additive
    (M : ModuleCat.{u} R) (n : ℕ) :
    (derivedExtContravariantFunctor M n).Additive
def

idealQuotientMayerVietorisProductPowersDiagram

L135 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisProductPowersDiagram
Documentation

The middle quotient-product term of the powers Mayer--Vietoris diagram.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
variable {R : Type u} [CommRing R]
Lean source · statement
def idealQuotientMayerVietorisProductPowersDiagram (I J : Ideal R) :
    ℕᵒᵖ ⥤ ModuleCat.{u} R
def

idealQuotientPowersBiprodDiagram

L140 ↗
EtaleFundamentalGroups.idealQuotientPowersBiprodDiagram
Documentation

The pointwise biproduct of the two quotient-module powers diagrams.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
variable {R : Type u} [CommRing R]
Lean source · statement
def idealQuotientPowersBiprodDiagram (I J : Ideal R) :
    ℕᵒᵖ ⥤ ModuleCat.{u} R
def

idealQuotientMayerVietorisProductPowersIso

L148 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisProductPowersIso
Documentation

The quotient-product diagram is the pointwise biproduct of its two coordinate quotient diagrams.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
variable {R : Type u} [CommRing R]
Lean source · statement
def idealQuotientMayerVietorisProductPowersIso (I J : Ideal R) :
    idealQuotientMayerVietorisProductPowersDiagram I J ≅
      idealQuotientPowersBiprodDiagram I J
def

idealQuotientMayerVietorisDerivedExtPowersMiddleTermRefl

L194 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersMiddleTermRefl
Documentation

The index-four term of the six-term diagram is derived Ext of the middle quotient-product diagram.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
variable {R : Type u} [CommRing R]
Lean source · full declaration
def idealQuotientMayerVietorisDerivedExtPowersMiddleTermRefl
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) :
    (idealQuotientMayerVietorisDerivedExtPowersDiagram
        I J M n₀ n₁ h ⋙
      (evaluation (Fin 6) AddCommGrpCat.{u}).obj ⟨4, by omega⟩) ≅
      (idealQuotientMayerVietorisProductPowersDiagram I J).op ⋙
        derivedExtContravariantFunctor M n₁ :=
  Iso.refl _
def

idealQuotientMayerVietorisDerivedExtPowersMiddleTermIso

L206 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersMiddleTermIso
Documentation

The index-four term is naturally the pointwise biproduct of the two derived local-cohomology powers diagrams.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
variable {R : Type u} [CommRing R]
Lean source · full declaration
def idealQuotientMayerVietorisDerivedExtPowersMiddleTermIso
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) :
    (idealQuotientMayerVietorisDerivedExtPowersDiagram
        I J M n₀ n₁ h ⋙
      (evaluation (Fin 6) AddCommGrpCat.{u}).obj ⟨4, by omega⟩) ≅
      pointwiseBiprodFunctor
        (derivedLocalCohomologyPowersDiagram I M n₁)
        (derivedLocalCohomologyPowersDiagram J M n₁) :=
  idealQuotientMayerVietorisDerivedExtPowersMiddleTermRefl
      I J M n₀ n₁ h ≪≫
    Functor.isoWhiskerRight
      (NatIso.op (idealQuotientMayerVietorisProductPowersIso I J).symm)
      (derivedExtContravariantFunctor M n₁) ≪≫
    Functor.isoWhiskerRight
      (diagramOpBiprodIso
        (localCohomology.ringModIdeals
          (localCohomology.idealPowersDiagram I))
        (localCohomology.ringModIdeals
          (localCohomology.idealPowersDiagram J)))
      (derivedExtContravariantFunctor M n₁) ≪≫
    additiveFunctorCompBiprodIso
      (localCohomology.ringModIdeals
        (localCohomology.idealPowersDiagram I)).op
      (localCohomology.ringModIdeals
        (localCohomology.idealPowersDiagram J)).op
      (derivedExtContravariantFunctor M n₁)
def

idealQuotientMayerVietorisDerivedExtPowersMiddleColimitIso

L236 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersMiddleColimitIso
Documentation

The colimit of the index-four term is the biproduct of the two derived local-cohomology objects.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
variable {R : Type u} [CommRing R]
Lean source · full declaration
def idealQuotientMayerVietorisDerivedExtPowersMiddleColimitIso
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁) :
    colimit
        (idealQuotientMayerVietorisDerivedExtPowersDiagram
            I J M n₀ n₁ h ⋙
          (evaluation (Fin 6) AddCommGrpCat.{u}).obj ⟨4, by omega⟩) ≅
      derivedLocalCohomology I M n₁ ⊞
        derivedLocalCohomology J M n₁ :=
  HasColimit.isoOfNatIso
      (idealQuotientMayerVietorisDerivedExtPowersMiddleTermIso
        I J M n₀ n₁ h) ≪≫
    pointwiseBiprodColimitIso
      (derivedLocalCohomologyPowersDiagram I M n₁)
      (derivedLocalCohomologyPowersDiagram J M n₁)
theorem

idealQuotientMayerVietorisDerivedExtPowersMiddleColimit_isZero

L254 ↗
EtaleFundamentalGroups.idealQuotientMayerVietorisDerivedExtPowersMiddleColimit_isZero
Documentation

If both support-local-cohomology objects vanish, then the middle colimit in the Mayer--Vietoris sequence vanishes.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v w
variable {R : Type u} [CommRing R]
Lean source · full declaration
theorem idealQuotientMayerVietorisDerivedExtPowersMiddleColimit_isZero
    (I J : Ideal R) (M : ModuleCat.{u} R)
    (n₀ n₁ : ℕ) (h : 1 + n₀ = n₁)
    (hI : IsZero (derivedLocalCohomology I M n₁))
    (hJ : IsZero (derivedLocalCohomology J M n₁)) :
    IsZero
      (colimit
        (idealQuotientMayerVietorisDerivedExtPowersDiagram
            I J M n₀ n₁ h ⋙
          (evaluation (Fin 6) AddCommGrpCat.{u}).obj ⟨4, by omega⟩)) :=
  (idealQuotientMayerVietorisDerivedExtPowersMiddleColimitIso
      I J M n₀ n₁ h).isZero_iff.mpr
    ((biprod_isZero_iff _ _).mpr ⟨hI, hJ⟩)

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