NYLL
Module

DerivedLocalCohomologyLegacyComparison.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyLegacyComparison
29 declarations indexed from sourceView source ↗

Module documentation

Comparing derived and legacy local cohomology

This file constructs the projective-resolution comparison between derived-category Ext and the legacy left-derived Ext used by localCohomology. The comparison is first built in positive degree from the common cocycle quotient; its naturality in the first variable is the input needed to compare the ideal-powers diagrams and their colimits.

Imports3
Imported by2

Declarations

abbrev

projectiveResolutionForgottenLinearYonedaShortComplexSucc

L36 ↗
EtaleFundamentalGroups.projectiveResolutionForgottenLinearYonedaShortComplexSucc
Documentation

The three terms around positive degree n + 1 in the cochain complex computing legacy Ext, after forgetting the R-module structure.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · statement
abbrev projectiveResolutionForgottenLinearYonedaShortComplexSucc
    (P : ProjectiveResolution X) (Y : ModuleCat.{u} R) (n : ℕ) :
    ShortComplex AddCommGrpCat.{u}
def

projectiveResolutionCyclesToDerivedExtSucc

L44 ↗
EtaleFundamentalGroups.projectiveResolutionCyclesToDerivedExtSucc
Documentation

A cocycle in the projective-resolution complex determines its derived-category Ext class.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · full declaration
def projectiveResolutionCyclesToDerivedExtSucc
    (P : ProjectiveResolution X) (Y : ModuleCat.{u} R) (n : ℕ) :
    AddMonoidHom
      (AddMonoidHom.ker
        (projectiveResolutionForgottenLinearYonedaShortComplexSucc
          P Y n).g.hom)
      (CategoryTheory.Abelian.Ext.{u} X Y (n + 1)) where
  toFun f := P.extMk f.1 (n + 2) (by omega) (by
    change P.complex.d (n + 2) (n + 1) ≫ f.1 = 0
    exact f.2)
  map_zero' := by
    apply P.extMk_zero
  map_add' f g := by
    symm
    apply P.add_extMk
theorem

projectiveResolutionCyclesToDerivedExtSucc_surjective

L62 ↗
EtaleFundamentalGroups.projectiveResolutionCyclesToDerivedExtSucc_surjective
Documentation

Every positive-degree derived Ext class has a cocycle representative in the chosen projective resolution.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · statement
theorem projectiveResolutionCyclesToDerivedExtSucc_surjective
    (P : ProjectiveResolution X) (Y : ModuleCat.{u} R) (n : ℕ) :
    Function.Surjective
      (projectiveResolutionCyclesToDerivedExtSucc P Y n)
theorem

projectiveResolutionCyclesToDerivedExtSucc_ker_eq_range

L74 ↗
EtaleFundamentalGroups.projectiveResolutionCyclesToDerivedExtSucc_ker_eq_range
Documentation

In the cocycle group, the kernel of the map to derived Ext is exactly the subgroup of coboundaries.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · statement
theorem projectiveResolutionCyclesToDerivedExtSucc_ker_eq_range
    (P : ProjectiveResolution X) (Y : ModuleCat.{u} R) (n : ℕ) :
    AddMonoidHom.ker (projectiveResolutionCyclesToDerivedExtSucc P Y n) =
      AddMonoidHom.range
        (projectiveResolutionForgottenLinearYonedaShortComplexSucc
          P Y n).abToCycles
def

projectiveResolutionCocycleQuotientAddEquivDerivedExtSucc

L100 ↗
EtaleFundamentalGroups.projectiveResolutionCocycleQuotientAddEquivDerivedExtSucc
Documentation

The explicit cocycles-modulo-coboundaries group of the forgotten legacy Ext complex is additively equivalent to derived-category Ext.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · statement
def projectiveResolutionCocycleQuotientAddEquivDerivedExtSucc
    (P : ProjectiveResolution X) (Y : ModuleCat.{u} R) (n : ℕ) :
    ((AddMonoidHom.ker
        (projectiveResolutionForgottenLinearYonedaShortComplexSucc
          P Y n).g.hom) ⧸
      AddMonoidHom.range
        (projectiveResolutionForgottenLinearYonedaShortComplexSucc
          P Y n).abToCycles) ≃+
      CategoryTheory.Abelian.Ext.{u} X Y (n + 1)
def

projectiveResolutionForgottenLegacyExtIsoDerivedExtSucc

L119 ↗
EtaleFundamentalGroups.projectiveResolutionForgottenLegacyExtIsoDerivedExtSucc
Documentation

After forgetting the R-module structure, legacy Ext computed from a chosen projective resolution is canonically isomorphic to positive-degree derived-category Ext.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · statement
def projectiveResolutionForgottenLegacyExtIsoDerivedExtSucc
    (P : ProjectiveResolution X) (Y : ModuleCat.{u} R) (n : ℕ) :
    (forget₂ (ModuleCat.{u} R) AddCommGrpCat.{u}).obj
        (((_root_.Ext R (ModuleCat.{u} R) (n + 1)).obj (op X)).obj Y) ≅
      AddCommGrpCat.of
        (CategoryTheory.Abelian.Ext.{u} X Y (n + 1))
def

projectiveResolutionLinearYonedaMap

L145 ↗
EtaleFundamentalGroups.projectiveResolutionLinearYonedaMap
Documentation

Applying the linear Yoneda functor to a lift of projective resolutions gives the contravariant map of the cochain complexes computing legacy Ext.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · statement
def projectiveResolutionLinearYonedaMap
    (phi : ProjectiveResolution.Hom P' P f)
    (Y : ModuleCat.{u} R) :
    P.complex.linearYonedaObj R Y ⟶
      P'.complex.linearYonedaObj R Y
theorem

projectiveResolution_isoExt_hom_naturality

L157 ↗
EtaleFundamentalGroups.projectiveResolution_isoExt_hom_naturality
Documentation

The projective-resolution computation of legacy Ext is natural in the first variable for any specified lift of the underlying morphism.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · statement
theorem projectiveResolution_isoExt_hom_naturality
    (phi : ProjectiveResolution.Hom P' P f)
    (Y : ModuleCat.{u} R) (i : ℕ) :
    (((_root_.Ext R (ModuleCat.{u} R) i).map f.op).app Y) ≫
        (P'.isoExt i Y).hom =
      (P.isoExt i Y).hom ≫
        HomologicalComplex.homologyMap
          (projectiveResolutionLinearYonedaMap P' P phi Y) i
def

projectiveResolutionForgottenLinearYonedaShortComplexSuccMap

L250 ↗
EtaleFundamentalGroups.projectiveResolutionForgottenLinearYonedaShortComplexSuccMap
Documentation

The adjacent positive-degree short-complex map obtained from a lift of projective resolutions, after forgetting module structure.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · statement
def projectiveResolutionForgottenLinearYonedaShortComplexSuccMap
    (phi : ProjectiveResolution.Hom P' P f)
    (Y : ModuleCat.{u} R) (n : ℕ) :
    projectiveResolutionForgottenLinearYonedaShortComplexSucc P Y n ⟶
      projectiveResolutionForgottenLinearYonedaShortComplexSucc P' Y n
theorem

projectiveResolution_homologyIsoScSucc_hom_naturality

L262 ↗
EtaleFundamentalGroups.projectiveResolution_homologyIsoScSucc_hom_naturality
Documentation

Passing from complex homology to the adjacent three-term short complex is natural for the cochain map induced by a projective-resolution lift.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · full declaration
theorem projectiveResolution_homologyIsoScSucc_hom_naturality
    (phi : ProjectiveResolution.Hom P' P f)
    (Y : ModuleCat.{u} R) (n : ℕ) :
    HomologicalComplex.homologyMap
        (projectiveResolutionLinearYonedaMap P' P phi Y) (n + 1) ≫
      ((P'.complex.linearYonedaObj R Y).homologyIsoSc'
        n (n + 1) (n + 2) (by simp) (by simp)).hom =
    ((P.complex.linearYonedaObj R Y).homologyIsoSc'
        n (n + 1) (n + 2) (by simp) (by simp)).hom ≫
      ShortComplex.homologyMap
        ((HomologicalComplex.shortComplexFunctor'
          (ModuleCat.{u} R) (ComplexShape.up ℕ)
            n (n + 1) (n + 2)).map
          (projectiveResolutionLinearYonedaMap P' P phi Y)) := by
  let e := HomologicalComplex.homologyFunctorIso'
    (ModuleCat.{u} R) (ComplexShape.up ℕ)
      n (n + 1) (n + 2) (by simp) (by simp)
  have hcomp (Q : HomologicalComplex (ModuleCat.{u} R)
      (ComplexShape.up ℕ)) :
      e.hom.app Q =
        (Q.homologyIsoSc' n (n + 1) (n + 2)
          (by simp) (by simp)).hom := by
    change (𝟙 (Q.homology (n + 1))) ≫
        ShortComplex.homologyMap
          (Q.isoSc' n (n + 1) (n + 2) (by simp) (by simp)).hom =
      ShortComplex.homologyMap
        (Q.isoSc' n (n + 1) (n + 2) (by simp) (by simp)).hom
    exact Category.id_comp _
  have h := e.hom.naturality
    (projectiveResolutionLinearYonedaMap P' P phi Y)
  rw [hcomp, hcomp] at h
  dsimp only [HomologicalComplex.homologyFunctor,
    Functor.comp_map, ShortComplex.homologyFunctor,
    HomologicalComplex.shortComplexFunctor'] at h ⊢
  exact h
def

projectiveResolutionCocycleMapSucc

L300 ↗
EtaleFundamentalGroups.projectiveResolutionCocycleMapSucc
Documentation

A lift between projective resolutions pulls a cocycle back by precomposition in the corresponding degree.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · full declaration
def projectiveResolutionCocycleMapSucc
    (phi : ProjectiveResolution.Hom P' P f)
    (Y : ModuleCat.{u} R) (n : ℕ) :
    AddMonoidHom
      (AddMonoidHom.ker
        (projectiveResolutionForgottenLinearYonedaShortComplexSucc
          P Y n).g.hom)
      (AddMonoidHom.ker
        (projectiveResolutionForgottenLinearYonedaShortComplexSucc
          P' Y n).g.hom) where
  toFun z :=
    ⟨(projectiveResolutionForgottenLinearYonedaShortComplexSuccMap
      P' P phi Y n).τ₂ z.1, by
      change (projectiveResolutionForgottenLinearYonedaShortComplexSucc
        P' Y n).g ((projectiveResolutionForgottenLinearYonedaShortComplexSuccMap
          P' P phi Y n).τ₂ z.1) = 0
      rw [← ConcreteCategory.comp_apply,
        (projectiveResolutionForgottenLinearYonedaShortComplexSuccMap
          P' P phi Y n).comm₂₃,
        ConcreteCategory.comp_apply, z.2, map_zero]⟩
  map_zero' := by
    ext
    exact map_zero _
  map_add' z z' := by
    ext
    exact map_add _ _ _
theorem

projectiveResolutionAbCyclesIsoSucc_naturality

L329 ↗
EtaleFundamentalGroups.projectiveResolutionAbCyclesIsoSucc_naturality
Documentation

The concrete kernel description of cycles is natural for the forgotten short-complex map induced by a projective-resolution lift.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · statement
theorem projectiveResolutionAbCyclesIsoSucc_naturality
    (phi : ProjectiveResolution.Hom P' P f)
    (Y : ModuleCat.{u} R) (n : ℕ) :
    (projectiveResolutionForgottenLinearYonedaShortComplexSucc
        P Y n).abCyclesIso.inv ≫
      ShortComplex.cyclesMap
        (projectiveResolutionForgottenLinearYonedaShortComplexSuccMap
          P' P phi Y n) ≫
      (projectiveResolutionForgottenLinearYonedaShortComplexSucc
        P' Y n).abCyclesIso.hom =
    AddCommGrpCat.ofHom
      (projectiveResolutionCocycleMapSucc P' P phi Y n)
theorem

projectiveResolutionCyclesToDerivedExtSucc_naturality_apply

L377 ↗
EtaleFundamentalGroups.projectiveResolutionCyclesToDerivedExtSucc_naturality_apply
Documentation

Elementwise naturality of the cocycle-to-derived-Ext map in the first variable for a specified lift between projective resolutions.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · statement
theorem projectiveResolutionCyclesToDerivedExtSucc_naturality_apply
    (phi : ProjectiveResolution.Hom P' P f)
    (Y : ModuleCat.{u} R) (n : ℕ)
    (z : AddMonoidHom.ker
      (projectiveResolutionForgottenLinearYonedaShortComplexSucc
        P Y n).g.hom) :
    derivedExtContravariantMap f Y (n + 1)
        (projectiveResolutionCyclesToDerivedExtSucc P Y n z) =
      projectiveResolutionCyclesToDerivedExtSucc P' Y n
        (projectiveResolutionCocycleMapSucc P' P phi Y n z)
theorem

projectiveResolutionCyclesToDerivedExtSucc_naturality

L401 ↗
EtaleFundamentalGroups.projectiveResolutionCyclesToDerivedExtSucc_naturality
Documentation

The cocycle-to-derived-Ext map is natural in the first variable for a specified lift between projective resolutions.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · statement
theorem projectiveResolutionCyclesToDerivedExtSucc_naturality
    (phi : ProjectiveResolution.Hom P' P f)
    (Y : ModuleCat.{u} R) (n : ℕ) :
    AddCommGrpCat.ofHom
        (projectiveResolutionCyclesToDerivedExtSucc P Y n) ≫
      derivedExtContravariantMap f Y (n + 1) =
    AddCommGrpCat.ofHom
        (projectiveResolutionCocycleMapSucc P' P phi Y n) ≫
      AddCommGrpCat.ofHom
        (projectiveResolutionCyclesToDerivedExtSucc P' Y n)
def

projectiveResolutionCocycleQuotientMapSucc

L417 ↗
EtaleFundamentalGroups.projectiveResolutionCocycleQuotientMapSucc
Documentation

The cocycle pullback induced by a lift descends to the corresponding quotients by coboundaries.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · statement
def projectiveResolutionCocycleQuotientMapSucc
    (phi : ProjectiveResolution.Hom P' P f)
    (Y : ModuleCat.{u} R) (n : ℕ) :
    ((AddMonoidHom.ker
        (projectiveResolutionForgottenLinearYonedaShortComplexSucc
          P Y n).g.hom) ⧸
      AddMonoidHom.range
        (projectiveResolutionForgottenLinearYonedaShortComplexSucc
          P Y n).abToCycles) →+
    ((AddMonoidHom.ker
        (projectiveResolutionForgottenLinearYonedaShortComplexSucc
          P' Y n).g.hom) ⧸
      AddMonoidHom.range
        (projectiveResolutionForgottenLinearYonedaShortComplexSucc
          P' Y n).abToCycles)
theorem

projectiveResolutionCocycleQuotientMapSucc_mk

L460 ↗
EtaleFundamentalGroups.projectiveResolutionCocycleQuotientMapSucc_mk
Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · statement
theorem projectiveResolutionCocycleQuotientMapSucc_mk
    (phi : ProjectiveResolution.Hom P' P f)
    (Y : ModuleCat.{u} R) (n : ℕ)
    (z : AddMonoidHom.ker
      (projectiveResolutionForgottenLinearYonedaShortComplexSucc
        P Y n).g.hom) :
    projectiveResolutionCocycleQuotientMapSucc P' P phi Y n
        (QuotientAddGroup.mk'
          (AddMonoidHom.range
            (projectiveResolutionForgottenLinearYonedaShortComplexSucc
              P Y n).abToCycles) z) =
      QuotientAddGroup.mk'
        (AddMonoidHom.range
          (projectiveResolutionForgottenLinearYonedaShortComplexSucc
            P' Y n).abToCycles)
        (projectiveResolutionCocycleMapSucc P' P phi Y n z)
theorem

projectiveResolutionAbHomologyIsoSucc_naturality

L480 ↗
EtaleFundamentalGroups.projectiveResolutionAbHomologyIsoSucc_naturality
Documentation

The explicit cocycle-quotient description of forgotten short-complex homology is natural for a projective-resolution lift.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · statement
theorem projectiveResolutionAbHomologyIsoSucc_naturality
    (phi : ProjectiveResolution.Hom P' P f)
    (Y : ModuleCat.{u} R) (n : ℕ) :
    ShortComplex.homologyMap
        (projectiveResolutionForgottenLinearYonedaShortComplexSuccMap
          P' P phi Y n) ≫
      (projectiveResolutionForgottenLinearYonedaShortComplexSucc
        P' Y n).abHomologyIso.hom =
    (projectiveResolutionForgottenLinearYonedaShortComplexSucc
        P Y n).abHomologyIso.hom ≫
      AddCommGrpCat.ofHom
        (projectiveResolutionCocycleQuotientMapSucc P' P phi Y n)
theorem

projectiveResolutionCocycleQuotientAddEquivDerivedExtSucc_mk

L525 ↗
EtaleFundamentalGroups.projectiveResolutionCocycleQuotientAddEquivDerivedExtSucc_mk
Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · statement
theorem projectiveResolutionCocycleQuotientAddEquivDerivedExtSucc_mk
    (Q : ProjectiveResolution X) (Y : ModuleCat.{u} R) (n : ℕ)
    (z : AddMonoidHom.ker
      (projectiveResolutionForgottenLinearYonedaShortComplexSucc
        Q Y n).g.hom) :
    projectiveResolutionCocycleQuotientAddEquivDerivedExtSucc Q Y n
        (QuotientAddGroup.mk'
          (AddMonoidHom.range
            (projectiveResolutionForgottenLinearYonedaShortComplexSucc
              Q Y n).abToCycles) z) =
      projectiveResolutionCyclesToDerivedExtSucc Q Y n z
theorem

projectiveResolutionCocycleQuotientAddEquivDerivedExtSucc_naturality

L541 ↗
EtaleFundamentalGroups.projectiveResolutionCocycleQuotientAddEquivDerivedExtSucc_naturality
Documentation

The positive-degree cocycle-quotient equivalence with derived Ext is natural in the first variable for a specified lift of projective resolutions.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · statement
theorem projectiveResolutionCocycleQuotientAddEquivDerivedExtSucc_naturality
    (phi : ProjectiveResolution.Hom P' P f)
    (Y : ModuleCat.{u} R) (n : ℕ) :
    AddCommGrpCat.ofHom
        (projectiveResolutionCocycleQuotientMapSucc P' P phi Y n) ≫
      (projectiveResolutionCocycleQuotientAddEquivDerivedExtSucc
        P' Y n).toAddCommGrpIso.hom =
    (projectiveResolutionCocycleQuotientAddEquivDerivedExtSucc
        P Y n).toAddCommGrpIso.hom ≫
      derivedExtContravariantMap f Y (n + 1)
theorem

projectiveResolutionForgottenLegacyExtIsoDerivedExtSucc_naturality

L574 ↗
EtaleFundamentalGroups.projectiveResolutionForgottenLegacyExtIsoDerivedExtSucc_naturality
Documentation

The full positive-degree comparison from forgotten legacy Ext to derived-category Ext is natural in the first variable for a specified lift of projective resolutions.

Source context 11 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
section FirstVariableNaturality
variable {X' : ModuleCat.{u} R}
variable (P' : ProjectiveResolution X') (P : ProjectiveResolution X)
variable {f : X' ⟶ X}
Lean source · statement
theorem projectiveResolutionForgottenLegacyExtIsoDerivedExtSucc_naturality
    (phi : ProjectiveResolution.Hom P' P f)
    (Y : ModuleCat.{u} R) (n : ℕ) :
    (forget₂ (ModuleCat.{u} R) AddCommGrpCat.{u}).map
        (((_root_.Ext R (ModuleCat.{u} R) (n + 1)).map f.op).app Y) ≫
      (projectiveResolutionForgottenLegacyExtIsoDerivedExtSucc
        P' Y n).hom =
    (projectiveResolutionForgottenLegacyExtIsoDerivedExtSucc
        P Y n).hom ≫
      derivedExtContravariantMap f Y (n + 1)
def

forgottenLegacyExtContravariantFunctor

L667 ↗
EtaleFundamentalGroups.forgottenLegacyExtContravariantFunctor
Documentation

Legacy Ext in the first variable, after evaluating the second variable and forgetting the module structure.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · statement
def forgottenLegacyExtContravariantFunctor
    (Y : ModuleCat.{u} R) (i : ℕ) :
    (ModuleCat.{u} R)ᵒᵖ ⥤ AddCommGrpCat.{u}
def

projectiveResolutionLiftHom

L676 ↗
EtaleFundamentalGroups.projectiveResolutionLiftHom
Documentation

The canonical lift of a morphism to the chosen projective resolutions, packaged with its augmentation compatibility.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · full declaration
def projectiveResolutionLiftHom
    {X' X : ModuleCat.{u} R} (f : X' ⟶ X)
    (P' : ProjectiveResolution X') (P : ProjectiveResolution X) :
    ProjectiveResolution.Hom P' P f where
  hom := ProjectiveResolution.lift f P' P
  hom_f_zero_comp_π_f_zero := by
    simpa using ProjectiveResolution.lift_commutes_zero f P' P
def

forgottenLegacyExtIsoDerivedExtSucc

L686 ↗
EtaleFundamentalGroups.forgottenLegacyExtIsoDerivedExtSucc
Documentation

The positive-degree comparison at an object, using Mathlib's chosen projective resolution.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · statement
def forgottenLegacyExtIsoDerivedExtSucc
    (X Y : ModuleCat.{u} R) (n : ℕ) :
    (forgottenLegacyExtContravariantFunctor Y (n + 1)).obj (op X) ≅
      (derivedExtContravariantFunctor Y (n + 1)).obj (op X)
def

forgottenLegacyExtNatIsoDerivedExtSucc

L695 ↗
EtaleFundamentalGroups.forgottenLegacyExtNatIsoDerivedExtSucc
Documentation

In positive degree, forgotten legacy Ext and derived-category Ext are naturally isomorphic as contravariant functors of the first variable.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · statement
def forgottenLegacyExtNatIsoDerivedExtSucc
    (Y : ModuleCat.{u} R) (n : ℕ) :
    forgottenLegacyExtContravariantFunctor Y (n + 1) ≅
      derivedExtContravariantFunctor Y (n + 1)
def

forgottenLegacyLocalCohomologyPowersDiagram

L728 ↗
EtaleFundamentalGroups.forgottenLegacyLocalCohomologyPowersDiagram
Documentation

The powers diagram of positive-degree legacy Ext, evaluated at a module and then regarded as a diagram of additive commutative groups.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · statement
def forgottenLegacyLocalCohomologyPowersDiagram
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) :
    (ℕᵒᵖ)ᵒᵖ ⥤ AddCommGrpCat.{u}
def

forgottenLegacyLocalCohomologyPowersDiagramIsoDerivedSucc

L737 ↗
EtaleFundamentalGroups.forgottenLegacyLocalCohomologyPowersDiagramIsoDerivedSucc
Documentation

At every positive degree, the evaluated forgotten legacy-Ext powers diagram is naturally isomorphic to the derived-Ext powers diagram.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · statement
def forgottenLegacyLocalCohomologyPowersDiagramIsoDerivedSucc
    (I : Ideal R) (M : ModuleCat.{u} R) (n : ℕ) :
    forgottenLegacyLocalCohomologyPowersDiagram I M (n + 1) ≅
      derivedLocalCohomologyPowersDiagram I M (n + 1)
def

forgottenLegacyLocalCohomologyPowersColimitIsoDerivedSucc

L748 ↗
EtaleFundamentalGroups.forgottenLegacyLocalCohomologyPowersColimitIsoDerivedSucc
Documentation

The colimit of the evaluated forgotten legacy-Ext powers diagram is canonically isomorphic to positive-degree derived local cohomology.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · statement
def forgottenLegacyLocalCohomologyPowersColimitIsoDerivedSucc
    (I : Ideal R) (M : ModuleCat.{u} R) (n : ℕ) :
    colimit (forgottenLegacyLocalCohomologyPowersDiagram I M (n + 1)) ≅
      derivedLocalCohomology I M (n + 1)
def

forgottenLegacyLocalCohomologyIsoPowersColimit

L757 ↗
EtaleFundamentalGroups.forgottenLegacyLocalCohomologyIsoPowersColimit
Documentation

Forgetting the legacy local-cohomology module commutes with its defining ideal-powers colimit.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · statement
def forgottenLegacyLocalCohomologyIsoPowersColimit
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) :
    (forget₂ (ModuleCat.{u} R) AddCommGrpCat.{u}).obj
        ((localCohomology I i).obj M) ≅
      colimit (forgottenLegacyLocalCohomologyPowersDiagram I M i)
def

forgottenLegacyLocalCohomologyIsoDerivedSucc

L777 ↗
EtaleFundamentalGroups.forgottenLegacyLocalCohomologyIsoDerivedSucc
Documentation

In positive degree, derived local cohomology is canonically isomorphic to Mathlib's legacy local-cohomology module after forgetting scalars.

Source context 7 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PositiveDegree
variable {R : Type u} [CommRing R]
variable {X : ModuleCat.{u} R}
Lean source · statement
def forgottenLegacyLocalCohomologyIsoDerivedSucc
    (I : Ideal R) (M : ModuleCat.{u} R) (n : ℕ) :
    (forget₂ (ModuleCat.{u} R) AddCommGrpCat.{u}).obj
        ((localCohomology I (n + 1)).obj M) ≅
      derivedLocalCohomology I M (n + 1)

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