NYLL
Module

MultiplicativeGroup.lean

Nyll.EtaleCohomology.Classical.MultiplicativeGroup
7 declarations indexed from sourceView source ↗

Module documentation

The actual multiplicative group on the small étale site

We restrict the existing fppf sheaf of units from the algebraic-curve library. Its descent proof is reused unchanged. Sections are the actual units of the actual scheme's global section ring, with ordinary pullback.

The power morphism below will be used in the étale Kummer sequence. This file does not assert its epimorphy or any higher cohomology vanishing.

Imports6
Imported by3

Declarations

def

restrictBigEtaleAbelianSheaf

L31 ↗
EtaleCohomology.restrictBigEtaleAbelianSheaf
Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
Lean source · statement
def restrictBigEtaleAbelianSheaf (X : Scheme.{u}) :
    Sheaf Scheme.etaleTopology AddCommGrpCat.{u} ⥤
      Sheaf X.smallEtaleTopology AddCommGrpCat.{u}
def

etaleMultiplicativeGroupSheaf

L50 ↗
EtaleCohomology.etaleMultiplicativeGroupSheaf
Documentation

The actual abelian sheaf of units on the small étale site, written additively and obtained from the already constructed fppf sheaf.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
Lean source · statement
def etaleMultiplicativeGroupSheaf (X : Scheme.{u}) :
    Sheaf X.smallEtaleTopology AddCommGrpCat.{u}
def

etaleMultiplicativeGroupSectionsEquiv

L62 ↗
EtaleCohomology.etaleMultiplicativeGroupSectionsEquiv
Documentation

Sections are actual units, with their multiplicative law written additively.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
Lean source · statement
def etaleMultiplicativeGroupSectionsEquiv (X : Scheme.{u}) (V : X.Etale) :
    (etaleMultiplicativeGroupSheaf X).obj.obj (op V) ≃+
      Additive ((Γ(V.left, ⊤) : Type u)ˣ)
def

etaleMultiplicativeGroupPower

L68 ↗
EtaleCohomology.etaleMultiplicativeGroupPower
Documentation

Multiplication by n on this abelian sheaf is the usual nth-power map on units.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
Lean source · statement
def etaleMultiplicativeGroupPower (X : Scheme.{u}) (n : ℕ) :
    etaleMultiplicativeGroupSheaf X ⟶ etaleMultiplicativeGroupSheaf X
theorem

etaleMultiplicativeGroupPower_apply

L72 ↗
EtaleCohomology.etaleMultiplicativeGroupPower_apply
Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
Lean source · statement
theorem etaleMultiplicativeGroupPower_apply (X : Scheme.{u}) (n : ℕ)
    (V : X.Etale) (s : (etaleMultiplicativeGroupSheaf X).obj.obj (op V)) :
    etaleMultiplicativeGroupSectionsEquiv X V
      ((etaleMultiplicativeGroupPower X n).hom.app (op V) s) =
        Additive.ofMul ((etaleMultiplicativeGroupSectionsEquiv X V s).toMul ^ n)
def

etaleMultiplicativeGroupSpecSectionsEquiv

L84 ↗
EtaleCohomology.etaleMultiplicativeGroupSpecSectionsEquiv
Documentation

On an actual affine étale object, Gm sections are the units of the original ring, via the canonical Gamma-Spec isomorphism.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
Lean source · statement
def etaleMultiplicativeGroupSpecSectionsEquiv (X : Scheme.{u})
    (R : CommRingCat.{u}) (f : Spec R ⟶ X) [Etale f] :
    (etaleMultiplicativeGroupSheaf X).obj.obj (op (Scheme.Etale.mk f)) ≃+
      Additive Rˣ
theorem

etaleMultiplicativeGroupSpecSectionsEquiv_naturality

L94 ↗
EtaleCohomology.etaleMultiplicativeGroupSpecSectionsEquiv_naturality
Documentation

Pullback on the actual unit sheaf agrees with the original ring map. In particular finite Galois deck pullback is the actual Galois action on field units; no equivariance hypothesis is supplied.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
Lean source · full declaration
theorem etaleMultiplicativeGroupSpecSectionsEquiv_naturality
    (X : Scheme.{u}) {R S : CommRingCat.{u}} (h : R ⟶ S)
    (f : Spec R ⟶ X) [Etale f] [Etale (Spec.map h)]
    (s : (etaleMultiplicativeGroupSheaf X).obj.obj (op (Scheme.Etale.mk f))) :
    etaleMultiplicativeGroupSpecSectionsEquiv X S (Spec.map h ≫ f)
      ((etaleMultiplicativeGroupSheaf X).obj.map
        (MorphismProperty.Over.homMk
          (P := show MorphismProperty Scheme.{u} from @Etale) (Q := ⊤)
          (Spec.map h) rfl).op s) =
      Additive.ofMul (Units.map h.hom.toMonoidHom
        (etaleMultiplicativeGroupSpecSectionsEquiv X R f s).toMul) := by
  apply Additive.toMul.injective
  apply Units.ext
  exact ConcreteCategory.congr_hom (Scheme.ΓSpecIso_naturality h)
    (etaleMultiplicativeGroupSectionsEquiv X (Scheme.Etale.mk f) s).toMul.val

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