NYLL
Module

DerivedLocalCohomologyModuleCoefficients.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyModuleCoefficients
9 declarations indexed from sourceView source ↗

Module documentation

Linear coefficient maps on derived local cohomology

The coefficient maps and the connecting maps act on colimit representatives by postcomposition in derived Ext. Bilinearity of composition makes these maps linear for the module structure already constructed on the local-cohomology colimit. Their underlying functions retain the existing coefficient exactness, and regular multiplication is scalar multiplication.

Imports9
Imported by10

Declarations

theorem

derivedLocalCohomologyCoefficientsSecondMap_ι_apply

L39 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsSecondMap_ι_apply
Documentation

The second coefficient map acts on representatives by postcomposition with the degree-zero class of the second coefficient morphism.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsSecondMap_ι_apply
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (i n : ℕ)
    (α : CategoryTheory.Abelian.Ext.{u}
      (ModuleCat.of R (R ⧸ I ^ n)) S.X₂ i) :
    derivedLocalCohomologyCoefficientsSecondMap I hS i
        (colimit.ι (derivedLocalCohomologyPowersDiagram I S.X₂ i)
          (op (op n)) α) =
      colimit.ι (derivedLocalCohomologyPowersDiagram I S.X₃ i)
        (op (op n))
        (α.comp (CategoryTheory.Abelian.Ext.mk₀ S.g) (add_zero i))
theorem

derivedLocalCohomologyCoefficientsConnectingMap_ι_apply

L70 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsConnectingMap_ι_apply
Documentation

The connecting map acts on representatives by postcomposition with the extension class of the coefficient short exact sequence.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsConnectingMap_ι_apply
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (i n : ℕ)
    (α : CategoryTheory.Abelian.Ext.{u}
      (ModuleCat.of R (R ⧸ I ^ n)) S.X₃ i) :
    derivedLocalCohomologyCoefficientsConnectingMap I hS i
        (colimit.ι (derivedLocalCohomologyPowersDiagram I S.X₃ i)
          (op (op n)) α) =
      colimit.ι (derivedLocalCohomologyPowersDiagram I S.X₁ (i + 1))
        (op (op n)) (α.comp hS.extClass rfl)
def

derivedLocalCohomologyModuleCoefficientsFirstMap

L99 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModuleCoefficientsFirstMap
Documentation

The first coefficient map with its existing local-cohomology module structures on source and target.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · full declaration
def derivedLocalCohomologyModuleCoefficientsFirstMap
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (i : ℕ) :
    derivedLocalCohomologyModule I S.X₁ i →ₗ[R]
      derivedLocalCohomologyModule I S.X₂ i where
  toFun := ConcreteCategory.hom
    (derivedLocalCohomologyCoefficientsFirstMap I hS i)
  map_add' z w := map_add (ConcreteCategory.hom
    (derivedLocalCohomologyCoefficientsFirstMap I hS i)) z w
  map_smul' a z := by
    let : PreservesFilteredColimitsOfSize.{0, 0} (forget AddCommGrpCat.{u}) :=
      preservesSmallestFilteredColimits_of_preservesFilteredColimits _
    obtain ⟨k, α, hα⟩ :=
      Concrete.colimit_exists_rep (derivedLocalCohomologyPowersDiagram I S.X₁ i) z
    rcases k with ⟨⟨n⟩⟩
    change
      derivedLocalCohomologyCoefficientsFirstMap I hS i
          (derivedLocalCohomologyScalarMap I S.X₁ i a z) =
        derivedLocalCohomologyScalarMap I S.X₂ i a
          (derivedLocalCohomologyCoefficientsFirstMap I hS i z)
    rw [← hα]
    change CategoryTheory.Abelian.Ext.{u} (ModuleCat.of R (R ⧸ I ^ n)) S.X₁ i at α
    let ι : CategoryTheory.Abelian.Ext.{u} (ModuleCat.of R (R ⧸ I ^ n)) S.X₂ i →+
        derivedLocalCohomology I S.X₂ i :=
      (colimit.ι (derivedLocalCohomologyPowersDiagram I S.X₂ i) (op (op n))).hom
    exact (congrArg (derivedLocalCohomologyCoefficientsFirstMap I hS i)
      (derivedLocalCohomologyScalarMap_ι_apply I S.X₁ i a n α)).trans
        ((derivedLocalCohomologyCoefficientsFirstMap_ι_apply I hS i n (a • α)).trans
          ((congrArg ι
            (CategoryTheory.Abelian.Ext.smul_comp α
              (CategoryTheory.Abelian.Ext.mk₀ S.f) (add_zero i) a)).trans
            ((derivedLocalCohomologyScalarMap_ι_apply I S.X₂ i a n
              (α.comp (CategoryTheory.Abelian.Ext.mk₀ S.f) (add_zero i))).symm.trans
                (congrArg (derivedLocalCohomologyScalarMap I S.X₂ i a)
                  (derivedLocalCohomologyCoefficientsFirstMap_ι_apply I hS i n α).symm))))
def

derivedLocalCohomologyModuleCoefficientsSecondMap

L137 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModuleCoefficientsSecondMap
Documentation

The second coefficient map is linear for the canonical module structure on the derived local-cohomology colimit.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · full declaration
def derivedLocalCohomologyModuleCoefficientsSecondMap
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (i : ℕ) :
    derivedLocalCohomologyModule I S.X₂ i →ₗ[R]
      derivedLocalCohomologyModule I S.X₃ i where
  toFun := ConcreteCategory.hom
    (derivedLocalCohomologyCoefficientsSecondMap I hS i)
  map_add' z w := map_add (ConcreteCategory.hom
    (derivedLocalCohomologyCoefficientsSecondMap I hS i)) z w
  map_smul' a z := by
    let : PreservesFilteredColimitsOfSize.{0, 0} (forget AddCommGrpCat.{u}) :=
      preservesSmallestFilteredColimits_of_preservesFilteredColimits _
    obtain ⟨k, α, hα⟩ :=
      Concrete.colimit_exists_rep (derivedLocalCohomologyPowersDiagram I S.X₂ i) z
    rcases k with ⟨⟨n⟩⟩
    change
      derivedLocalCohomologyCoefficientsSecondMap I hS i
          (derivedLocalCohomologyScalarMap I S.X₂ i a z) =
        derivedLocalCohomologyScalarMap I S.X₃ i a
          (derivedLocalCohomologyCoefficientsSecondMap I hS i z)
    rw [← hα]
    change CategoryTheory.Abelian.Ext.{u} (ModuleCat.of R (R ⧸ I ^ n)) S.X₂ i at α
    let ι : CategoryTheory.Abelian.Ext.{u} (ModuleCat.of R (R ⧸ I ^ n)) S.X₃ i →+
        derivedLocalCohomology I S.X₃ i :=
      (colimit.ι (derivedLocalCohomologyPowersDiagram I S.X₃ i) (op (op n))).hom
    exact (congrArg (derivedLocalCohomologyCoefficientsSecondMap I hS i)
      (derivedLocalCohomologyScalarMap_ι_apply I S.X₂ i a n α)).trans
        ((derivedLocalCohomologyCoefficientsSecondMap_ι_apply I hS i n (a • α)).trans
          ((congrArg ι
            (CategoryTheory.Abelian.Ext.smul_comp α
              (CategoryTheory.Abelian.Ext.mk₀ S.g) (add_zero i) a)).trans
            ((derivedLocalCohomologyScalarMap_ι_apply I S.X₃ i a n
              (α.comp (CategoryTheory.Abelian.Ext.mk₀ S.g) (add_zero i))).symm.trans
                (congrArg (derivedLocalCohomologyScalarMap I S.X₃ i a)
                  (derivedLocalCohomologyCoefficientsSecondMap_ι_apply I hS i n α).symm))))
def

derivedLocalCohomologyModuleCoefficientsConnectingMap

L175 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModuleCoefficientsConnectingMap
Documentation

The connecting map is linear because postcomposition by the Ext extension class commutes with scalar multiplication.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · full declaration
def derivedLocalCohomologyModuleCoefficientsConnectingMap
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (i : ℕ) :
    derivedLocalCohomologyModule I S.X₃ i →ₗ[R]
      derivedLocalCohomologyModule I S.X₁ (i + 1) where
  toFun := ConcreteCategory.hom
    (derivedLocalCohomologyCoefficientsConnectingMap I hS i)
  map_add' z w := map_add (ConcreteCategory.hom
    (derivedLocalCohomologyCoefficientsConnectingMap I hS i)) z w
  map_smul' a z := by
    let : PreservesFilteredColimitsOfSize.{0, 0} (forget AddCommGrpCat.{u}) :=
      preservesSmallestFilteredColimits_of_preservesFilteredColimits _
    obtain ⟨k, α, hα⟩ :=
      Concrete.colimit_exists_rep (derivedLocalCohomologyPowersDiagram I S.X₃ i) z
    rcases k with ⟨⟨n⟩⟩
    change
      derivedLocalCohomologyCoefficientsConnectingMap I hS i
          (derivedLocalCohomologyScalarMap I S.X₃ i a z) =
        derivedLocalCohomologyScalarMap I S.X₁ (i + 1) a
          (derivedLocalCohomologyCoefficientsConnectingMap I hS i z)
    rw [← hα]
    change CategoryTheory.Abelian.Ext.{u} (ModuleCat.of R (R ⧸ I ^ n)) S.X₃ i at α
    let ι : CategoryTheory.Abelian.Ext.{u} (ModuleCat.of R (R ⧸ I ^ n)) S.X₁ (i + 1) →+
        derivedLocalCohomology I S.X₁ (i + 1) :=
      (colimit.ι (derivedLocalCohomologyPowersDiagram I S.X₁ (i + 1)) (op (op n))).hom
    exact (congrArg (derivedLocalCohomologyCoefficientsConnectingMap I hS i)
      (derivedLocalCohomologyScalarMap_ι_apply I S.X₃ i a n α)).trans
        ((derivedLocalCohomologyCoefficientsConnectingMap_ι_apply I hS i n (a • α)).trans
          ((congrArg ι (CategoryTheory.Abelian.Ext.smul_comp α (hS.extClass) rfl a)).trans
            ((derivedLocalCohomologyScalarMap_ι_apply I S.X₁ (i + 1) a n
              (α.comp (hS.extClass) rfl)).symm.trans
                (congrArg (derivedLocalCohomologyScalarMap I S.X₁ (i + 1) a)
                  (derivedLocalCohomologyCoefficientsConnectingMap_ι_apply I hS i n α).symm))))
theorem

derivedLocalCohomologyModuleCoefficients_sameDegree_exact

L210 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModuleCoefficients_sameDegree_exact
Documentation

Same-degree exactness of the linear coefficient maps.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyModuleCoefficients_sameDegree_exact
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (i : ℕ) :
    Function.Exact (derivedLocalCohomologyModuleCoefficientsFirstMap I hS i)
      (derivedLocalCohomologyModuleCoefficientsSecondMap I hS i)
theorem

derivedLocalCohomologyModuleCoefficients_beforeConnecting_exact

L219 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModuleCoefficients_beforeConnecting_exact
Documentation

Exactness immediately before the linear connecting map.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyModuleCoefficients_beforeConnecting_exact
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (i : ℕ) :
    Function.Exact (derivedLocalCohomologyModuleCoefficientsSecondMap I hS i)
      (derivedLocalCohomologyModuleCoefficientsConnectingMap I hS i)
theorem

derivedLocalCohomologyModuleCoefficients_afterConnecting_exact

L229 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModuleCoefficients_afterConnecting_exact
Documentation

The image of the linear connecting map is the kernel of the next linear coefficient map.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyModuleCoefficients_afterConnecting_exact
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (i : ℕ) :
    Function.Exact (derivedLocalCohomologyModuleCoefficientsConnectingMap I hS i)
      (derivedLocalCohomologyModuleCoefficientsFirstMap I hS (i + 1))
theorem

derivedLocalCohomologyModuleCoefficientsFirstMap_smulShortComplex

L239 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModuleCoefficientsFirstMap_smulShortComplex
Documentation

For a regular multiplication sequence, the first linear coefficient map is multiplication by the chosen scalar.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyModuleCoefficientsFirstMap_smulShortComplex
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ)
    (x : R) (hx : IsSMulRegular M x) :
    derivedLocalCohomologyModuleCoefficientsFirstMap I
        hx.smulShortComplex_shortExact i =
      x • (LinearMap.id : derivedLocalCohomologyModule I M i →ₗ[R]
        derivedLocalCohomologyModule I M i)

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