Module

FppfCohomologyLES.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.FppfCohomologyLES

80 declarations indexed from sourceView source ↗

Module documentation

Fppf Cohomology LES

Imports15

Mathlib.AlgebraicGeometry.Sites.Fpqc
Mathlib.AlgebraicGeometry.Limits
Mathlib.Algebra.Category.Grp.AB
Mathlib.Algebra.Category.Grp.Ulift
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt
Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
Mathlib.CategoryTheory.Sites.SheafCohomology.ExactSequences
Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
Mathlib.RingTheory.ClassGroup.Basic
Mathlib.RingTheory.PicardGroup
Mathlib.Data.Int.Order.Units
Mathlib.Algebra.GroupWithZero.Units.Fintype
Mathlib.GroupTheory.QuotientGroup.Basic
Mathlib.Algebra.Group.Subgroup.Finite

Imported by1

Nyll.AlgebraicCurves.Cohomology.Sheaves.All

abbrev

constIntSheaf

L45 ↗

FppfCohomologyLES.constIntSheaf

Documentation

The constant sheaf of integers, using a universe lift for its underlying abelian group.

Source context 5 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

abbrev constIntSheaf : Sheaf J AddCommGrpCat.{w}

theorem

sheafH_eq_ext

L48 ↗

FppfCohomologyLES.sheafH_eq_ext

Source context 5 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem sheafH_eq_ext (F : Sheaf J AddCommGrpCat.{w}) (n : ℕ) :
    F.H n = Ext (constIntSheaf J) F n

def

cohomologyMap

L54 ↗

FppfCohomologyLES.cohomologyMap

Documentation

The additive map on sheaf cohomology induced by a morphism of sheaves.

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

def cohomologyMap {F G : Sheaf J AddCommGrpCat.{w}} (φ : F ⟶ G) (n : ℕ) :
    F.H n →+ G.H n

lemma

cohomologyMap_apply

L58 ↗

FppfCohomologyLES.cohomologyMap_apply

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

lemma cohomologyMap_apply {F G : Sheaf J AddCommGrpCat.{w}} (φ : F ⟶ G) (n : ℕ)
    (x : Ext (constIntSheaf J) F n) :
    cohomologyMap φ n x = x.comp (Ext.mk₀ φ) (add_zero n)

def

cohomologyδ

L64 ↗

FppfCohomologyLES.cohomologyδ

Documentation

The connecting homomorphism associated to a short exact sequence of sheaves.

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

def cohomologyδ {S : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    S.X₃.H n₀ →+ S.X₁.H n₁

lemma

cohomologyδ_apply

L69 ↗

FppfCohomologyLES.cohomologyδ_apply

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

lemma cohomologyδ_apply {S : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (x : Ext (constIntSheaf J) S.X₃ n₀) :
    cohomologyδ hS n₀ n₁ h x = x.comp hS.extClass h

theorem

cohomologyMap_id

L74 ↗

FppfCohomologyLES.cohomologyMap_id

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

theorem cohomologyMap_id (F : Sheaf J AddCommGrpCat.{w}) (n : ℕ)
    (x : Ext (constIntSheaf J) F n) :
    cohomologyMap (𝟙 F) n x = x

theorem

cohomologyMap_comp

L79 ↗

FppfCohomologyLES.cohomologyMap_comp

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

theorem cohomologyMap_comp {F G H : Sheaf J AddCommGrpCat.{w}} (φ : F ⟶ G) (ψ : G ⟶ H)
    (n : ℕ) (x : Ext (constIntSheaf J) F n) :
    cohomologyMap (φ ≫ ψ) n x = cohomologyMap ψ n (cohomologyMap φ n x)

theorem

cohomology_exact_two

L84 ↗

FppfCohomologyLES.cohomology_exact_two

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

theorem cohomology_exact_two {S : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS : S.ShortExact) (n : ℕ) :
    Function.Exact (cohomologyMap S.f n) (cohomologyMap S.g n)

theorem

cohomology_exact_three

L91 ↗

FppfCohomologyLES.cohomology_exact_three

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

theorem cohomology_exact_three {S : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    Function.Exact (cohomologyMap S.g n₀) (cohomologyδ hS n₀ n₁ h)

theorem

cohomology_exact_one

L98 ↗

FppfCohomologyLES.cohomology_exact_one

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

theorem cohomology_exact_one {S : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    Function.Exact (cohomologyδ hS n₀ n₁ h) (cohomologyMap S.f n₁)

theorem

cohomologyMap_zero_injective_of_mono

L105 ↗

FppfCohomologyLES.cohomologyMap_zero_injective_of_mono

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

theorem cohomologyMap_zero_injective_of_mono {F G : Sheaf J AddCommGrpCat.{w}} (φ : F ⟶ G)
    [Mono φ] :
    Function.Injective (cohomologyMap φ 0)

theorem

cohomologyMap_surjective_of_section

L111 ↗

FppfCohomologyLES.cohomologyMap_surjective_of_section

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

theorem cohomologyMap_surjective_of_section {F G : Sheaf J AddCommGrpCat.{w}}
    (φ : F ⟶ G) (s : G ⟶ F) (hs : s ≫ φ = 𝟙 G) (n : ℕ) :
    Function.Surjective (cohomologyMap φ n)

theorem

sixTermLES

L118 ↗

FppfCohomologyLES.sixTermLES

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

theorem sixTermLES {S : ShortComplex (Sheaf J AddCommGrpCat.{w})} (hS : S.ShortExact) :
    Function.Injective (cohomologyMap S.f 0) ∧
    Function.Exact (cohomologyMap S.f 0) (cohomologyMap S.g 0) ∧
    Function.Exact (cohomologyMap S.g 0) (cohomologyδ hS 0 1 rfl) ∧
    Function.Exact (cohomologyδ hS 0 1 rfl) (cohomologyMap S.f 1) ∧
    Function.Exact (cohomologyMap S.f 1) (cohomologyMap S.g 1)

def

cohomologyComposableArrows

L130 ↗

FppfCohomologyLES.cohomologyComposableArrows

Documentation

The six-term segment of the cohomology sequence across two consecutive degrees.

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

def cohomologyComposableArrows {S : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    ComposableArrows AddCommGrpCat.{w'} 5

theorem

cohomologyComposableArrows_exact

L135 ↗

FppfCohomologyLES.cohomologyComposableArrows_exact

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

theorem cohomologyComposableArrows_exact {S : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    (cohomologyComposableArrows hS n₀ n₁ h).Exact

def

cohomologyZeroAddEquivHom

L141 ↗

FppfCohomologyLES.cohomologyZeroAddEquivHom

Documentation

Identify degree-zero cohomology with morphisms from the constant integer sheaf.

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

def cohomologyZeroAddEquivHom (F : Sheaf J AddCommGrpCat.{w}) :
    F.H 0 ≃+ (constIntSheaf J ⟶ F)

def

biprodSES

L147 ↗

FppfCohomologyLES.biprodSES

Documentation

The split short complex given by inclusion into a biproduct and projection to its second factor.

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

def biprodSES (F G : Sheaf J AddCommGrpCat.{w}) :
    ShortComplex (Sheaf J AddCommGrpCat.{w})

theorem

biprodSES_shortExact

L151 ↗

FppfCohomologyLES.biprodSES_shortExact

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}
omit [HasExt (Sheaf J AddCommGrpCat)] in

Lean source · statement

theorem biprodSES_shortExact (F G : Sheaf J AddCommGrpCat.{w}) :
    (biprodSES F G).ShortExact

theorem

biprodSES_delta_apply_eq_zero

L155 ↗

FppfCohomologyLES.biprodSES_delta_apply_eq_zero

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
variable {J}

Lean source · statement

theorem biprodSES_delta_apply_eq_zero (F G : Sheaf J AddCommGrpCat.{w}) (n₀ n₁ : ℕ)
    (h : n₀ + 1 = n₁) (x : Ext (constIntSheaf J) (biprodSES F G).X₃ n₀) :
    cohomologyδ (biprodSES_shortExact F G) n₀ n₁ h x = 0

instance

fppfSheavesIsGrothendieckAbelian

L169 ↗

FppfCohomologyLES.fppfSheavesIsGrothendieckAbelian

Source context 5 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry

Lean source · statement

instance fppfSheavesIsGrothendieckAbelian :
    IsGrothendieckAbelian.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})

abbrev

FppfH

L188 ↗

FppfCohomologyLES.FppfH

Documentation

Sheaf cohomology on the fppf site in the specified degree.

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

abbrev FppfH (F : Sheaf Scheme.fppfTopology.{u} Ab.{u + 1}) (n : ℕ) :
    Type (u + 1)

theorem

fppfH_eq_sheafH

L192 ↗

FppfCohomologyLES.fppfH_eq_sheafH

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppfH_eq_sheafH (F : Sheaf Scheme.fppfTopology.{u} Ab.{u + 1}) (n : ℕ) :
    FppfH F n = F.H n

theorem

fppf_les_exact_two

L195 ↗

FppfCohomologyLES.fppf_les_exact_two

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_les_exact_two {S : ShortComplex (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})}
    (hS : S.ShortExact) (n : ℕ) :
    Function.Exact (cohomologyMap S.f n) (cohomologyMap S.g n)

theorem

fppf_les_exact_three

L200 ↗

FppfCohomologyLES.fppf_les_exact_three

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_les_exact_three {S : ShortComplex (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})}
    (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    Function.Exact (cohomologyMap S.g n₀) (cohomologyδ hS n₀ n₁ h)

theorem

fppf_les_exact_one

L205 ↗

FppfCohomologyLES.fppf_les_exact_one

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_les_exact_one {S : ShortComplex (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})}
    (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    Function.Exact (cohomologyδ hS n₀ n₁ h) (cohomologyMap S.f n₁)

theorem

fppf_sixTermLES

L210 ↗

FppfCohomologyLES.fppf_sixTermLES

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_sixTermLES {S : ShortComplex (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})}
    (hS : S.ShortExact) :
    Function.Injective (cohomologyMap S.f 0) ∧
    Function.Exact (cohomologyMap S.f 0) (cohomologyMap S.g 0) ∧
    Function.Exact (cohomologyMap S.g 0) (cohomologyδ hS 0 1 rfl) ∧
    Function.Exact (cohomologyδ hS 0 1 rfl) (cohomologyMap S.f 1) ∧
    Function.Exact (cohomologyMap S.f 1) (cohomologyMap S.g 1)

theorem

fppf_composableArrowsLES_exact

L219 ↗

FppfCohomologyLES.fppf_composableArrowsLES_exact

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_composableArrowsLES_exact
    {S : ShortComplex (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})}
    (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    (cohomologyComposableArrows hS n₀ n₁ h).Exact

def

fppfCohomologyZeroAddEquivHom

L226 ↗

FppfCohomologyLES.fppfCohomologyZeroAddEquivHom

Documentation

Identify degree-zero fppf cohomology with morphisms from the constant integer sheaf.

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

def fppfCohomologyZeroAddEquivHom (F : Sheaf Scheme.fppfTopology.{u} Ab.{u + 1}) :
    FppfH F 0 ≃+ (constIntSheaf Scheme.fppfTopology.{u} ⟶ F)

theorem

fppf_satGate_biprodSES_shortExact

L230 ↗

FppfCohomologyLES.fppf_satGate_biprodSES_shortExact

Source context 8 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]
omit [HasExt (Sheaf Scheme.fppfTopology Ab)] in

Lean source · statement

theorem fppf_satGate_biprodSES_shortExact (F G : Sheaf Scheme.fppfTopology.{u} Ab.{u + 1}) :
    (biprodSES F G).ShortExact

theorem

fppf_satGate_les_applies

L234 ↗

FppfCohomologyLES.fppf_satGate_les_applies

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_satGate_les_applies (F G : Sheaf Scheme.fppfTopology.{u} Ab.{u + 1}) (n : ℕ) :
    Function.Exact (cohomologyMap (biprodSES F G).f n) (cohomologyMap (biprodSES F G).g n)

theorem

fppf_satGate_delta_eq_zero

L238 ↗

FppfCohomologyLES.fppf_satGate_delta_eq_zero

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_satGate_delta_eq_zero (F G : Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})
    (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (x : Ext (constIntSheaf Scheme.fppfTopology.{u}) (biprodSES F G).X₃ n₀) :
    cohomologyδ (biprodSES_shortExact F G) n₀ n₁ h x = 0

theorem

classGroup_int_card_eq_one

L250 ↗

FppfCohomologyLES.classGroup_int_card_eq_one

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · statement

theorem classGroup_int_card_eq_one : Fintype.card (ClassGroup ℤ) = 1

theorem

classGroup_int_subsingleton

L253 ↗

FppfCohomologyLES.classGroup_int_subsingleton

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · statement

theorem classGroup_int_subsingleton : Subsingleton (ClassGroup ℤ)

theorem

natCard_classGroup_int

L256 ↗

FppfCohomologyLES.natCard_classGroup_int

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · statement

theorem natCard_classGroup_int : Nat.card (ClassGroup ℤ) = 1

theorem

pic_int_subsingleton

L259 ↗

FppfCohomologyLES.pic_int_subsingleton

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · statement

theorem pic_int_subsingleton : Subsingleton (CommRing.Pic ℤ)

theorem

intUnits_powMonoidHom_ker_of_odd

L262 ↗

FppfCohomologyLES.intUnits_powMonoidHom_ker_of_odd

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · statement

theorem intUnits_powMonoidHom_ker_of_odd (p : ℕ) (hp : Odd p) :
    (powMonoidHom p : ℤˣ →* ℤˣ).ker = ⊥

theorem

intUnits_powMonoidHom_ker_two

L268 ↗

FppfCohomologyLES.intUnits_powMonoidHom_ker_two

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · statement

theorem intUnits_powMonoidHom_ker_two :
    (powMonoidHom 2 : ℤˣ →* ℤˣ).ker = ⊤

theorem

intUnits_powMonoidHom_range_of_odd

L274 ↗

FppfCohomologyLES.intUnits_powMonoidHom_range_of_odd

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · statement

theorem intUnits_powMonoidHom_range_of_odd (p : ℕ) (hp : Odd p) :
    (powMonoidHom p : ℤˣ →* ℤˣ).range = ⊤

theorem

intUnits_powMonoidHom_range_two

L281 ↗

FppfCohomologyLES.intUnits_powMonoidHom_range_two

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · statement

theorem intUnits_powMonoidHom_range_two :
    (powMonoidHom 2 : ℤˣ →* ℤˣ).range = ⊥

theorem

natCard_intUnits

L291 ↗

FppfCohomologyLES.natCard_intUnits

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · statement

theorem natCard_intUnits : Nat.card ℤˣ = 2

theorem

natCard_intUnits_pthTorsion

L294 ↗

FppfCohomologyLES.natCard_intUnits_pthTorsion

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · full declaration

theorem natCard_intUnits_pthTorsion (p : ℕ) (hp : p.Prime) :
    Nat.card (powMonoidHom p : ℤˣ →* ℤˣ).ker = if p = 2 then 2 else 1 := by
  split_ifs with h
  · subst h
    rw [intUnits_powMonoidHom_ker_two, Subgroup.card_top, Nat.card_eq_fintype_card,
      Fintype.card_units_int]
  · rw [intUnits_powMonoidHom_ker_of_odd p (hp.odd_of_ne_two h), Subgroup.card_bot]

theorem

natCard_intUnits_modPthPowers

L302 ↗

FppfCohomologyLES.natCard_intUnits_modPthPowers

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · full declaration

theorem natCard_intUnits_modPthPowers (p : ℕ) (hp : p.Prime) :
    Nat.card (ℤˣ ⧸ (powMonoidHom p : ℤˣ →* ℤˣ).range) = if p = 2 then 2 else 1 := by
  split_ifs with h
  · subst h
    rw [intUnits_powMonoidHom_range_two]
    rw [Nat.card_congr (QuotientGroup.quotientBot (G := ℤˣ)).toEquiv,
      Nat.card_eq_fintype_card, Fintype.card_units_int]
  · rw [intUnits_powMonoidHom_range_of_odd p (hp.odd_of_ne_two h)]
    have : Subsingleton (ℤˣ ⧸ (⊤ : Subgroup ℤˣ)) := QuotientGroup.subsingleton_quotient_top
    rw [Nat.card_eq_one_iff_unique]
    exact ⟨this, ⟨1⟩⟩

theorem

intUnits_kummer_exact_left

L314 ↗

FppfCohomologyLES.intUnits_kummer_exact_left

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · statement

theorem intUnits_kummer_exact_left (p : ℕ) :
    ((powMonoidHom p : ℤˣ →* ℤˣ).ker.subtype).range = (powMonoidHom p : ℤˣ →* ℤˣ).ker

theorem

intUnits_kummer_exact_middle

L318 ↗

FppfCohomologyLES.intUnits_kummer_exact_middle

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · statement

theorem intUnits_kummer_exact_middle (p : ℕ) :
    (powMonoidHom p : ℤˣ →* ℤˣ).range =
      (QuotientGroup.mk' (powMonoidHom p : ℤˣ →* ℤˣ).range).ker

theorem

intUnits_kummer_mk'_surjective

L323 ↗

FppfCohomologyLES.intUnits_kummer_mk'_surjective

Source context 4 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section ElementaryComputations

Lean source · statement

theorem intUnits_kummer_mk'_surjective (p : ℕ) :
    Function.Surjective (QuotientGroup.mk' (powMonoidHom p : ℤˣ →* ℤˣ).range)

theorem

cohomology_naturality_f

L340 ↗

FppfCohomologyLES.cohomology_naturality_f

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem cohomology_naturality_f {S₁ S₂ : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (φ : S₁ ⟶ S₂) (n : ℕ) (x : Ext (constIntSheaf J) S₁.X₁ n) :
    cohomologyMap φ.τ₂ n (cohomologyMap S₁.f n x) =
      cohomologyMap S₂.f n (cohomologyMap φ.τ₁ n x)

theorem

cohomology_naturality_g

L346 ↗

FppfCohomologyLES.cohomology_naturality_g

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem cohomology_naturality_g {S₁ S₂ : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (φ : S₁ ⟶ S₂) (n : ℕ) (x : Ext (constIntSheaf J) S₁.X₂ n) :
    cohomologyMap φ.τ₃ n (cohomologyMap S₁.g n x) =
      cohomologyMap S₂.g n (cohomologyMap φ.τ₂ n x)

theorem

cohomology_naturality_f_hom

L352 ↗

FppfCohomologyLES.cohomology_naturality_f_hom

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem cohomology_naturality_f_hom {S₁ S₂ : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (φ : S₁ ⟶ S₂) (n : ℕ) :
    (cohomologyMap φ.τ₂ n).comp (cohomologyMap S₁.f n) =
      (cohomologyMap S₂.f n).comp (cohomologyMap φ.τ₁ n)

theorem

cohomology_naturality_g_hom

L360 ↗

FppfCohomologyLES.cohomology_naturality_g_hom

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem cohomology_naturality_g_hom {S₁ S₂ : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (φ : S₁ ⟶ S₂) (n : ℕ) :
    (cohomologyMap φ.τ₃ n).comp (cohomologyMap S₁.g n) =
      (cohomologyMap S₂.g n).comp (cohomologyMap φ.τ₂ n)

theorem

cohomologyδ_naturality

L368 ↗

FppfCohomologyLES.cohomologyδ_naturality

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem cohomologyδ_naturality {S₁ S₂ : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (φ : S₁ ⟶ S₂) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (x : Ext (constIntSheaf J) S₁.X₃ n₀) :
    cohomologyδ hS₂ n₀ n₁ h (cohomologyMap φ.τ₃ n₀ x) =
      cohomologyMap φ.τ₁ n₁ (cohomologyδ hS₁ n₀ n₁ h x)

theorem

cohomologyδ_naturality_hom

L375 ↗

FppfCohomologyLES.cohomologyδ_naturality_hom

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem cohomologyδ_naturality_hom {S₁ S₂ : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (φ : S₁ ⟶ S₂) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    (cohomologyδ hS₂ n₀ n₁ h).comp (cohomologyMap φ.τ₃ n₀) =
      (cohomologyMap φ.τ₁ n₁).comp (cohomologyδ hS₁ n₀ n₁ h)

theorem

cohomologyδ_naturality_elem

L383 ↗

FppfCohomologyLES.cohomologyδ_naturality_elem

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem cohomologyδ_naturality_elem {S₁ S₂ : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (φ : S₁ ⟶ S₂) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    {z : Ext (constIntSheaf J) S₁.X₃ n₀} {c : Ext (constIntSheaf J) S₁.X₁ n₁}
    (hzc : cohomologyδ hS₁ n₀ n₁ h z = c) :
    cohomologyδ hS₂ n₀ n₁ h (cohomologyMap φ.τ₃ n₀ z) = cohomologyMap φ.τ₁ n₁ c

theorem

cohomologyLES_ladder

L390 ↗

FppfCohomologyLES.cohomologyLES_ladder

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem cohomologyLES_ladder {S₁ S₂ : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (φ : S₁ ⟶ S₂) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    (∀ x, cohomologyMap φ.τ₂ n₀ (cohomologyMap S₁.f n₀ x) =
        cohomologyMap S₂.f n₀ (cohomologyMap φ.τ₁ n₀ x)) ∧
    (∀ x, cohomologyMap φ.τ₃ n₀ (cohomologyMap S₁.g n₀ x) =
        cohomologyMap S₂.g n₀ (cohomologyMap φ.τ₂ n₀ x)) ∧
    (∀ x, cohomologyδ hS₂ n₀ n₁ h (cohomologyMap φ.τ₃ n₀ x) =
        cohomologyMap φ.τ₁ n₁ (cohomologyδ hS₁ n₀ n₁ h x))

def

cohomologyMapAddEquiv

L402 ↗

FppfCohomologyLES.cohomologyMapAddEquiv

Documentation

The additive equivalence on cohomology induced by an isomorphism of sheaves.

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · full declaration

def cohomologyMapAddEquiv {F G : Sheaf J AddCommGrpCat.{w}} (e : F ≅ G) (n : ℕ) :
    F.H n ≃+ G.H n where
  toFun := cohomologyMap e.hom n
  invFun := cohomologyMap e.inv n
  left_inv x := by rw [← cohomologyMap_comp, Iso.hom_inv_id, cohomologyMap_id]
  right_inv x := by rw [← cohomologyMap_comp, Iso.inv_hom_id, cohomologyMap_id]
  map_add' x y := map_add (cohomologyMap e.hom n) x y

lemma

cohomologyMapAddEquiv_apply

L410 ↗

FppfCohomologyLES.cohomologyMapAddEquiv_apply

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

lemma cohomologyMapAddEquiv_apply {F G : Sheaf J AddCommGrpCat.{w}} (e : F ≅ G) (n : ℕ)
    (x : Ext (constIntSheaf J) F n) :
    cohomologyMapAddEquiv e n x = cohomologyMap e.hom n x

lemma

cohomologyMapAddEquiv_symm_apply

L414 ↗

FppfCohomologyLES.cohomologyMapAddEquiv_symm_apply

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

lemma cohomologyMapAddEquiv_symm_apply {F G : Sheaf J AddCommGrpCat.{w}} (e : F ≅ G) (n : ℕ)
    (y : Ext (constIntSheaf J) G n) :
    (cohomologyMapAddEquiv e n).symm y = cohomologyMap e.inv n y

theorem

cohomologyMap_bijective_of_isIso

L418 ↗

FppfCohomologyLES.cohomologyMap_bijective_of_isIso

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem cohomologyMap_bijective_of_isIso {F G : Sheaf J AddCommGrpCat.{w}} (φ : F ⟶ G)
    [IsIso φ] (n : ℕ) :
    Function.Bijective (cohomologyMap φ n)

theorem

cohomologyLES_iso_compatible

L430 ↗

FppfCohomologyLES.cohomologyLES_iso_compatible

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem cohomologyLES_iso_compatible {S₁ S₂ : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (e : S₁ ≅ S₂) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    Function.Bijective (cohomologyMap e.hom.τ₁ n₀) ∧
    Function.Bijective (cohomologyMap e.hom.τ₂ n₀) ∧
    Function.Bijective (cohomologyMap e.hom.τ₃ n₀) ∧
    (∀ x, cohomologyMap e.hom.τ₂ n₀ (cohomologyMap S₁.f n₀ x) =
        cohomologyMap S₂.f n₀ (cohomologyMap e.hom.τ₁ n₀ x)) ∧
    (∀ x, cohomologyMap e.hom.τ₃ n₀ (cohomologyMap S₁.g n₀ x) =
        cohomologyMap S₂.g n₀ (cohomologyMap e.hom.τ₂ n₀ x)) ∧
    (∀ x, cohomologyδ hS₂ n₀ n₁ h (cohomologyMap e.hom.τ₃ n₀ x) =
        cohomologyMap e.hom.τ₁ n₁ (cohomologyδ hS₁ n₀ n₁ h x))

theorem

cohomologyδ_conj_of_iso

L448 ↗

FppfCohomologyLES.cohomologyδ_conj_of_iso

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem cohomologyδ_conj_of_iso {S₁ S₂ : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (e : S₁ ≅ S₂) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (x : Ext (constIntSheaf J) S₁.X₃ n₀) :
    cohomologyδ hS₁ n₀ n₁ h x =
      cohomologyMap e.inv.τ₁ n₁ (cohomologyδ hS₂ n₀ n₁ h (cohomologyMap e.hom.τ₃ n₀ x))

theorem

satGate_id_delta_naturality

L456 ↗

FppfCohomologyLES.satGate_id_delta_naturality

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem satGate_id_delta_naturality {S : ShortComplex (Sheaf J AddCommGrpCat.{w})}
    (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (x : Ext (constIntSheaf J) S.X₃ n₀) :
    cohomologyδ hS n₀ n₁ h (cohomologyMap (𝟙 S : S ⟶ S).τ₃ n₀ x) =
        cohomologyMap (𝟙 S : S ⟶ S).τ₁ n₁ (cohomologyδ hS n₀ n₁ h x) ∧
    cohomologyδ hS n₀ n₁ h (cohomologyMap (𝟙 S : S ⟶ S).τ₃ n₀ x) =
        cohomologyδ hS n₀ n₁ h x ∧
    cohomologyMap (𝟙 S : S ⟶ S).τ₁ n₁ (cohomologyδ hS n₀ n₁ h x) =
        cohomologyδ hS n₀ n₁ h x

def

biprodSESHom

L470 ↗

FppfCohomologyLES.biprodSESHom

Documentation

The morphism of split biproduct complexes induced by a morphism of the second factor.

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · full declaration

def biprodSESHom (F : Sheaf J AddCommGrpCat.{w})
    {G G' : Sheaf J AddCommGrpCat.{w}} (ψ : G ⟶ G') :
    biprodSES F G ⟶ biprodSES F G' where
  τ₁ := 𝟙 F
  τ₂ := biprod.map (𝟙 F) ψ
  τ₃ := ψ
  comm₁₂ := by simp [biprodSES]
  comm₂₃ := by simp [biprodSES]

lemma

biprodSESHom_τ₁

L480 ↗

FppfCohomologyLES.biprodSESHom_τ₁

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
omit [HasExt (Sheaf J AddCommGrpCat)] in

Lean source · statement

lemma biprodSESHom_τ₁ (F : Sheaf J AddCommGrpCat.{w}) {G G' : Sheaf J AddCommGrpCat.{w}}
    (ψ : G ⟶ G') : (biprodSESHom F ψ).τ₁ = 𝟙 F

lemma

biprodSESHom_τ₃

L484 ↗

FppfCohomologyLES.biprodSESHom_τ₃

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
omit [HasExt (Sheaf J AddCommGrpCat)] in

Lean source · statement

lemma biprodSESHom_τ₃ (F : Sheaf J AddCommGrpCat.{w}) {G G' : Sheaf J AddCommGrpCat.{w}}
    (ψ : G ⟶ G') : (biprodSESHom F ψ).τ₃ = ψ

theorem

satGate_biprodSESHom_delta_naturality

L487 ↗

FppfCohomologyLES.satGate_biprodSESHom_delta_naturality

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem satGate_biprodSESHom_delta_naturality (F : Sheaf J AddCommGrpCat.{w})
    {G G' : Sheaf J AddCommGrpCat.{w}} (ψ : G ⟶ G') (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (x : Ext (constIntSheaf J) (biprodSES F G).X₃ n₀) :
    cohomologyδ (biprodSES_shortExact F G') n₀ n₁ h
        (cohomologyMap (biprodSESHom F ψ).τ₃ n₀ x) =
      cohomologyMap (biprodSESHom F ψ).τ₁ n₁
        (cohomologyδ (biprodSES_shortExact F G) n₀ n₁ h x)

theorem

satGate_biprodSESHom_delta_zero_consistency

L497 ↗

FppfCohomologyLES.satGate_biprodSESHom_delta_zero_consistency

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem satGate_biprodSESHom_delta_zero_consistency (F : Sheaf J AddCommGrpCat.{w})
    {G G' : Sheaf J AddCommGrpCat.{w}} (ψ : G ⟶ G') (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (x : Ext (constIntSheaf J) (biprodSES F G).X₃ n₀) :
    cohomologyδ (biprodSES_shortExact F G') n₀ n₁ h
        (cohomologyMap (biprodSESHom F ψ).τ₃ n₀ x) = 0 ∧
    cohomologyMap (biprodSESHom F ψ).τ₁ n₁
        (cohomologyδ (biprodSES_shortExact F G) n₀ n₁ h x) = 0

def

biprodSESSwap

L508 ↗

FppfCohomologyLES.biprodSESSwap

Documentation

The split short complex with the two middle biproduct factors in reverse order.

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

def biprodSESSwap (F G : Sheaf J AddCommGrpCat.{w}) :
    ShortComplex (Sheaf J AddCommGrpCat.{w})

def

biprodSESSwapIso

L513 ↗

FppfCohomologyLES.biprodSESSwapIso

Documentation

The isomorphism of split complexes induced by the symmetry of the middle biproduct.

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

def biprodSESSwapIso (F G : Sheaf J AddCommGrpCat.{w}) :
    biprodSES F G ≅ biprodSESSwap F G

theorem

biprodSESSwap_shortExact

L523 ↗

FppfCohomologyLES.biprodSESSwap_shortExact

Source context 7 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]
omit [HasExt (Sheaf J AddCommGrpCat)] in

Lean source · statement

theorem biprodSESSwap_shortExact (F G : Sheaf J AddCommGrpCat.{w}) :
    (biprodSESSwap F G).ShortExact

theorem

satGate_swapIso_les_compatible

L527 ↗

FppfCohomologyLES.satGate_swapIso_les_compatible

Source context 6 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section GenericSite
variable {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
  [HasSheafify J AddCommGrpCat.{w}] [HasExt.{w'} (Sheaf J AddCommGrpCat.{w})]

Lean source · statement

theorem satGate_swapIso_les_compatible (F G : Sheaf J AddCommGrpCat.{w}) (n₀ n₁ : ℕ)
    (h : n₀ + 1 = n₁) :
    Function.Bijective (cohomologyMap (biprodSESSwapIso F G).hom.τ₁ n₀) ∧
    Function.Bijective (cohomologyMap (biprodSESSwapIso F G).hom.τ₂ n₀) ∧
    Function.Bijective (cohomologyMap (biprodSESSwapIso F G).hom.τ₃ n₀) ∧
    (∀ x, cohomologyMap (biprodSESSwapIso F G).hom.τ₂ n₀
            (cohomologyMap (biprodSES F G).f n₀ x) =
        cohomologyMap (biprodSESSwap F G).f n₀
            (cohomologyMap (biprodSESSwapIso F G).hom.τ₁ n₀ x)) ∧
    (∀ x, cohomologyMap (biprodSESSwapIso F G).hom.τ₃ n₀
            (cohomologyMap (biprodSES F G).g n₀ x) =
        cohomologyMap (biprodSESSwap F G).g n₀
            (cohomologyMap (biprodSESSwapIso F G).hom.τ₂ n₀ x)) ∧
    (∀ x, cohomologyδ (biprodSESSwap_shortExact F G) n₀ n₁ h
            (cohomologyMap (biprodSESSwapIso F G).hom.τ₃ n₀ x) =
        cohomologyMap (biprodSESSwapIso F G).hom.τ₁ n₁
            (cohomologyδ (biprodSES_shortExact F G) n₀ n₁ h x))

theorem

fppf_naturality_f

L558 ↗

FppfCohomologyLES.fppf_naturality_f

Source context 8 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_naturality_f {S₁ S₂ : ShortComplex (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})}
    (φ : S₁ ⟶ S₂) (n : ℕ) (x : Ext (constIntSheaf Scheme.fppfTopology.{u}) S₁.X₁ n) :
    cohomologyMap φ.τ₂ n (cohomologyMap S₁.f n x) =
      cohomologyMap S₂.f n (cohomologyMap φ.τ₁ n x)

theorem

fppf_naturality_g

L564 ↗

FppfCohomologyLES.fppf_naturality_g

Source context 8 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_naturality_g {S₁ S₂ : ShortComplex (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})}
    (φ : S₁ ⟶ S₂) (n : ℕ) (x : Ext (constIntSheaf Scheme.fppfTopology.{u}) S₁.X₂ n) :
    cohomologyMap φ.τ₃ n (cohomologyMap S₁.g n x) =
      cohomologyMap S₂.g n (cohomologyMap φ.τ₂ n x)

theorem

fppf_delta_naturality

L570 ↗

FppfCohomologyLES.fppf_delta_naturality

Source context 8 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_delta_naturality {S₁ S₂ : ShortComplex (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})}
    (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (φ : S₁ ⟶ S₂) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (x : Ext (constIntSheaf Scheme.fppfTopology.{u}) S₁.X₃ n₀) :
    cohomologyδ hS₂ n₀ n₁ h (cohomologyMap φ.τ₃ n₀ x) =
      cohomologyMap φ.τ₁ n₁ (cohomologyδ hS₁ n₀ n₁ h x)

theorem

fppf_delta_naturality_hom

L577 ↗

FppfCohomologyLES.fppf_delta_naturality_hom

Source context 8 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_delta_naturality_hom
    {S₁ S₂ : ShortComplex (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})}
    (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (φ : S₁ ⟶ S₂) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    (cohomologyδ hS₂ n₀ n₁ h).comp (cohomologyMap φ.τ₃ n₀) =
      (cohomologyMap φ.τ₁ n₁).comp (cohomologyδ hS₁ n₀ n₁ h)

theorem

fppf_les_ladder

L584 ↗

FppfCohomologyLES.fppf_les_ladder

Source context 8 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_les_ladder {S₁ S₂ : ShortComplex (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})}
    (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (φ : S₁ ⟶ S₂) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    (∀ x, cohomologyMap φ.τ₂ n₀ (cohomologyMap S₁.f n₀ x) =
        cohomologyMap S₂.f n₀ (cohomologyMap φ.τ₁ n₀ x)) ∧
    (∀ x, cohomologyMap φ.τ₃ n₀ (cohomologyMap S₁.g n₀ x) =
        cohomologyMap S₂.g n₀ (cohomologyMap φ.τ₂ n₀ x)) ∧
    (∀ x, cohomologyδ hS₂ n₀ n₁ h (cohomologyMap φ.τ₃ n₀ x) =
        cohomologyMap φ.τ₁ n₁ (cohomologyδ hS₁ n₀ n₁ h x))

theorem

fppf_les_iso_compatible

L594 ↗

FppfCohomologyLES.fppf_les_iso_compatible

Source context 8 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_les_iso_compatible
    {S₁ S₂ : ShortComplex (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})}
    (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (e : S₁ ≅ S₂) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    Function.Bijective (cohomologyMap e.hom.τ₁ n₀) ∧
    Function.Bijective (cohomologyMap e.hom.τ₂ n₀) ∧
    Function.Bijective (cohomologyMap e.hom.τ₃ n₀) ∧
    (∀ x, cohomologyMap e.hom.τ₂ n₀ (cohomologyMap S₁.f n₀ x) =
        cohomologyMap S₂.f n₀ (cohomologyMap e.hom.τ₁ n₀ x)) ∧
    (∀ x, cohomologyMap e.hom.τ₃ n₀ (cohomologyMap S₁.g n₀ x) =
        cohomologyMap S₂.g n₀ (cohomologyMap e.hom.τ₂ n₀ x)) ∧
    (∀ x, cohomologyδ hS₂ n₀ n₁ h (cohomologyMap e.hom.τ₃ n₀ x) =
        cohomologyMap e.hom.τ₁ n₁ (cohomologyδ hS₁ n₀ n₁ h x))

theorem

fppf_delta_conj_of_iso

L608 ↗

FppfCohomologyLES.fppf_delta_conj_of_iso

Source context 8 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_delta_conj_of_iso
    {S₁ S₂ : ShortComplex (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})}
    (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (e : S₁ ≅ S₂) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (x : Ext (constIntSheaf Scheme.fppfTopology.{u}) S₁.X₃ n₀) :
    cohomologyδ hS₁ n₀ n₁ h x =
      cohomologyMap e.inv.τ₁ n₁ (cohomologyδ hS₂ n₀ n₁ h (cohomologyMap e.hom.τ₃ n₀ x))

theorem

fppf_satGate_biprodSESHom_delta_naturality

L616 ↗

FppfCohomologyLES.fppf_satGate_biprodSESHom_delta_naturality

Source context 8 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_satGate_biprodSESHom_delta_naturality
    (F : Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})
    {G G' : Sheaf Scheme.fppfTopology.{u} Ab.{u + 1}} (ψ : G ⟶ G') (n₀ n₁ : ℕ)
    (h : n₀ + 1 = n₁)
    (x : Ext (constIntSheaf Scheme.fppfTopology.{u}) (biprodSES F G).X₃ n₀) :
    cohomologyδ (biprodSES_shortExact F G') n₀ n₁ h
        (cohomologyMap (biprodSESHom F ψ).τ₃ n₀ x) =
      cohomologyMap (biprodSESHom F ψ).τ₁ n₁
        (cohomologyδ (biprodSES_shortExact F G) n₀ n₁ h x)

theorem

fppf_satGate_id_delta_naturality

L627 ↗

FppfCohomologyLES.fppf_satGate_id_delta_naturality

Source context 8 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_satGate_id_delta_naturality
    {S : ShortComplex (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})}
    (hS : S.ShortExact) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁)
    (x : Ext (constIntSheaf Scheme.fppfTopology.{u}) S.X₃ n₀) :
    cohomologyδ hS n₀ n₁ h (cohomologyMap (𝟙 S : S ⟶ S).τ₃ n₀ x) =
        cohomologyMap (𝟙 S : S ⟶ S).τ₁ n₁ (cohomologyδ hS n₀ n₁ h x) ∧
    cohomologyδ hS n₀ n₁ h (cohomologyMap (𝟙 S : S ⟶ S).τ₃ n₀ x) =
        cohomologyδ hS n₀ n₁ h x ∧
    cohomologyMap (𝟙 S : S ⟶ S).τ₁ n₁ (cohomologyδ hS n₀ n₁ h x) =
        cohomologyδ hS n₀ n₁ h x

theorem

fppf_satGate_swapIso_les_compatible

L639 ↗

FppfCohomologyLES.fppf_satGate_swapIso_les_compatible

Source context 8 commands

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

universe w' w v u
open CategoryTheory Abelian Limits
open CategoryTheory Abelian Limits
namespace FppfCohomologyLES
section FppfSite
open AlgebraicGeometry
section WithLocalInstances
variable [HasSheafify Scheme.fppfTopology.{u} Ab.{u + 1}]
  [HasExt.{u + 1} (Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})]

Lean source · statement

theorem fppf_satGate_swapIso_les_compatible (F G : Sheaf Scheme.fppfTopology.{u} Ab.{u + 1})
    (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
    Function.Bijective (cohomologyMap (biprodSESSwapIso F G).hom.τ₁ n₀) ∧
    Function.Bijective (cohomologyMap (biprodSESSwapIso F G).hom.τ₂ n₀) ∧
    Function.Bijective (cohomologyMap (biprodSESSwapIso F G).hom.τ₃ n₀) ∧
    (∀ x, cohomologyMap (biprodSESSwapIso F G).hom.τ₂ n₀
            (cohomologyMap (biprodSES F G).f n₀ x) =
        cohomologyMap (biprodSESSwap F G).f n₀
            (cohomologyMap (biprodSESSwapIso F G).hom.τ₁ n₀ x)) ∧
    (∀ x, cohomologyMap (biprodSESSwapIso F G).hom.τ₃ n₀
            (cohomologyMap (biprodSES F G).g n₀ x) =
        cohomologyMap (biprodSESSwap F G).g n₀
            (cohomologyMap (biprodSESSwapIso F G).hom.τ₂ n₀ x)) ∧
    (∀ x, cohomologyδ (biprodSESSwap_shortExact F G) n₀ n₁ h
            (cohomologyMap (biprodSESSwapIso F G).hom.τ₃ n₀ x) =
        cohomologyMap (biprodSESSwapIso F G).hom.τ₁ n₁
            (cohomologyδ (biprodSES_shortExact F G) n₀ n₁ h x))

Module documentation

Fppf Cohomology LES

Declarations