NYLL
Module

RepresenterAction.lean

Nyll.EtaleCohomology.Constructible.RepresenterAction
14 declarations indexed from sourceView source ↗

Module documentation

Descent actions supplied by a local representer

The universal section of a representer on an étale cover constructs its descent action. The unit and action laws follow from the actual naturality and uniqueness in the representing equivalence.

Imports7
Imported by4

Declarations

def

representerSection

L36 ↗
EtaleCohomology.representerSection
Documentation

The universal section of the original sheaf on the local representing scheme.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
def representerSection : G.obj.obj (op ((etalePostcompose f).obj W))
lemma

representerSection_hom_ext

L40 ↗
EtaleCohomology.representerSection_hom_ext
Documentation

Equality of maps to a representer is detected by its universal section.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
lemma representerSection_hom_ext {T : Y.Etale} (a b : T ⟶ W)
    (hab : G.obj.map ((etalePostcompose f).map a).op (representerSection f G W h) =
      G.obj.map ((etalePostcompose f).map b).op (representerSection f G W h)) : a = b
def

representerActionDomain

L47 ↗
EtaleCohomology.representerActionDomain
Documentation

The pullback on which the descent action is defined, as an object over the cover.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
def representerActionDomain : Y.Etale
def

representerActionSecond

L51 ↗
EtaleCohomology.representerActionSecond
Documentation

The second overlap projection, viewed on the original small étale site.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
def representerActionSecond :
    (etalePostcompose f).obj (representerActionDomain f W) ⟶
      (etalePostcompose f).obj W
def

representerActionHom

L58 ↗
EtaleCohomology.representerActionHom
Documentation

The original sheaf's universal section determines a map from the overlap.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
def representerActionHom : representerActionDomain f W ⟶ W
def

representerAction

L63 ↗
EtaleCohomology.representerAction
Documentation

The geometric descent action obtained from local representability.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
def representerAction : pullback f (W.hom ≫ f) ⟶ W.left
lemma

representerAction_over

L66 ↗
EtaleCohomology.representerAction_over
Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
lemma representerAction_over : representerAction f G W h ≫ W.hom =
    pullback.fst f (W.hom ≫ f)
lemma

representerAction_base

L70 ↗
EtaleCohomology.representerAction_base
Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
lemma representerAction_base : representerAction f G W h ≫ (W.hom ≫ f) =
    pullback.fst f (W.hom ≫ f) ≫ f
lemma

representerAction_section

L75 ↗
EtaleCohomology.representerAction_section
Documentation

The universal section is invariant under the constructed descent action.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
lemma representerAction_section :
    G.obj.map ((etalePostcompose f).map (representerActionHom f G W h)).op
        (representerSection f G W h) =
      G.obj.map (representerActionSecond f W).op (representerSection f G W h)
lemma

representerActionHom_naturality

L82 ↗
EtaleCohomology.representerActionHom_naturality
Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
lemma representerActionHom_naturality {T : Y.Etale}
    (a : T ⟶ representerActionDomain f W) :
    h.homEquiv (a ≫ representerActionHom f G W h) =
      G.obj.map ((etalePostcompose f).map a ≫ representerActionSecond f W).op
        (representerSection f G W h)
lemma

representerAction_unit

L97 ↗
EtaleCohomology.representerAction_unit
Documentation

Acting along the diagonal recovers the original point of the representer.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
lemma representerAction_unit :
    pullback.lift (f := f) (g := W.hom ≫ f) W.hom (𝟙 W.left)
        (Category.id_comp (W.hom ≫ f)).symm ≫
      representerAction f G W h = 𝟙 W.left
lemma

representerAction_assoc

L117 ↗
EtaleCohomology.representerAction_assoc
Documentation

The descent action satisfies the genuine triple-pullback action law.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
lemma representerAction_assoc :
    pullbackActionStep f (W.hom ≫ f) (representerAction f G W h)
        (representerAction_base f G W h) ≫ representerAction f G W h =
      pullbackSkipMiddle f (W.hom ≫ f) ≫ representerAction f G W h
def

representerOverlapIso

L155 ↗
EtaleCohomology.representerOverlapIso
Documentation

The two overlap pullbacks of a local representer are canonically isomorphic. All the action laws are supplied by the original sheaf's universal section.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
def representerOverlapIso : pullback f (W.hom ≫ f) ≅ pullback (W.hom ≫ f) f
lemma

representerOverlapIso_hom_fst

L161 ↗
EtaleCohomology.representerOverlapIso_hom_fst
Documentation

The overlap isomorphism induces exactly the constructed descent action.

Source context 7 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
Lean source · statement
lemma representerOverlapIso_hom_fst :
    (representerOverlapIso f G W h).hom ≫ pullback.fst (W.hom ≫ f) f =
      representerAction f G W h

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