NYLL
Module

IntegerFiberSections.lean

Nyll.EtaleFundamentalGroups.Cohomology.IntegerFiberSections
4 declarations indexed from sourceView source ↗

Module documentation

Global lifts of one and vanishing of the actual extension class

A global section of the fiber over the constant integer section 1 gives a splitting of the original quotient morphism, by taking integral multiples and using the sheafification adjunction. Conversely a splitting gives such a section. Thus this torsor has a global point precisely when the actual Ext class vanishes.

Imports4
Imported by2

Declarations

def

integerLiftMap

L35 ↗
EtaleFundamentalGroups.Cohomology.integerLiftMap
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {K E : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : K ⟶ E)
  (p : E ⟶ (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
    (AddCommGrpCat.of (ULift.{u} ℤ))) (h : i ≫ p = 0)
Lean source · full declaration
def integerLiftMap
    (d : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶
      (extensionFiber (ShortComplex.mk i p h) (integerUnitSection X)).obj) :
    (Functor.const X.Etaleᵒᵖ).obj (AddCommGrpCat.of (ULift.{u} ℤ)) ⟶ E.obj where
  app U := AddCommGrpCat.ofHom (uliftZMultiplesHom (E.obj.obj U) (d.app U PUnit.unit).val)
  naturality U V f := by
    apply (AddCommGrpCat.uliftZMultiplesAddEquiv (E.obj.obj V)).injective
    change (uliftZMultiplesHom (E.obj.obj V) (d.app V PUnit.unit).val) (ULift.up 1) =
      E.obj.map f ((uliftZMultiplesHom (E.obj.obj U) (d.app U PUnit.unit).val) (ULift.up 1))
    rw [uliftZMultiplesHom_apply_apply, uliftZMultiplesHom_apply_apply]
    change (1 : ℤ) • (d.app V PUnit.unit).val = E.obj.map f ((1 : ℤ) • (d.app U PUnit.unit).val)
    rw [one_zsmul, one_zsmul]
    exact congrArg Subtype.val (ConcreteCategory.congr_hom (d.naturality f) PUnit.unit)
theorem

exists_section_of_integerFiber_section

L50 ↗
EtaleFundamentalGroups.Cohomology.exists_section_of_integerFiber_section
Documentation

A global lift of the section 1 splits the actual extension quotient.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {K E : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : K ⟶ E)
  (p : E ⟶ (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
    (AddCommGrpCat.of (ULift.{u} ℤ))) (h : i ≫ p = 0)
Lean source · statement
theorem exists_section_of_integerFiber_section
    (d : (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶
      (extensionFiber (ShortComplex.mk i p h) (integerUnitSection X)).obj) :
    ∃ s : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
        (AddCommGrpCat.of (ULift.{u} ℤ)) ⟶ E, s ≫ p = 𝟙 _
def

integerFiberSectionOfSection

L76 ↗
EtaleFundamentalGroups.Cohomology.integerFiberSectionOfSection
Documentation

A splitting gives a section of the actual fiber over 1.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {K E : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : K ⟶ E)
  (p : E ⟶ (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
    (AddCommGrpCat.of (ULift.{u} ℤ))) (h : i ≫ p = 0)
Lean source · full declaration
def integerFiberSectionOfSection
    (s : (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
      (AddCommGrpCat.of (ULift.{u} ℤ)) ⟶ E) (hs : s ≫ p = 𝟙 _) :
    (Functor.const X.Etaleᵒᵖ).obj PUnit ⟶
      (extensionFiber (ShortComplex.mk i p h) (integerUnitSection X)).obj where
  app U := ↾fun _ => ⟨s.hom.app U ((integerUnitSection X).app U PUnit.unit), by
    have hh := ConcreteCategory.congr_hom
      (congrArg (fun k => k.hom.app U) hs) ((integerUnitSection X).app U PUnit.unit)
    exact hh⟩
  naturality U V f := by
    apply ConcreteCategory.hom_ext
    intro a
    apply Subtype.ext
    have hn := ConcreteCategory.congr_hom (s.hom.naturality f)
      ((integerUnitSection X).app U PUnit.unit)
    have ht := ConcreteCategory.congr_hom ((integerUnitSection X).naturality f) PUnit.unit
    exact (congrArg (s.hom.app V) ht).trans hn
theorem

extClass_eq_zero_iff_integerFiber_section

L96 ↗
EtaleFundamentalGroups.Cohomology.extClass_eq_zero_iff_integerFiber_section
Documentation

The actual extension class is zero precisely when its fiber over 1 has a global section.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X : Scheme.{u}} {K E : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
  (i : K ⟶ E)
  (p : E ⟶ (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u}).obj
    (AddCommGrpCat.of (ULift.{u} ℤ))) (h : i ≫ p = 0)
Lean source · statement
theorem extClass_eq_zero_iff_integerFiber_section (hs : (ShortComplex.mk i p h).ShortExact) :
    hs.extClass = 0 ↔ Nonempty ((Functor.const X.Etaleᵒᵖ).obj PUnit ⟶
      (extensionFiber (ShortComplex.mk i p h) (integerUnitSection X)).obj)

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