NYLL
Module

AffineRepresenterCoaction.lean

Nyll.EtaleCohomology.Constructible.AffineRepresenterCoaction
9 declarations indexed from sourceView source ↗

Module documentation

Algebra descent data supplied by an affine local representer

An actual representer on an affine étale cover supplies the geometric action. Tensor coordinates then construct the algebra overlap equivalence and prove its diagonal and full cocycle laws. These laws are derived from the original sheaf's universal section, with no assumed descent comparison.

Imports11
Imported by2

Declarations

abbrev

affineRepresenterEtale

L44 ↗
EtaleCohomology.affineRepresenterEtale
Documentation

The literal spectrum morphism as an object of the cover's small étale site.

Source context 9 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Algebra.Descent
open scoped TensorProduct
namespace EtaleCohomology
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
variable [Etale (Spec.map (CommRingCat.ofHom (algebraMap R B)))]
  [Etale (Spec.map (CommRingCat.ofHom (algebraMap B C)))]
variable (G : Sheaf (Spec (.of R)).smallEtaleTopology (Type u))
Lean source · statement
abbrev affineRepresenterEtale : (Spec (.of B)).Etale
def

affineRepresenterOverlapIso

L58 ↗
EtaleCohomology.affineRepresenterOverlapIso
Documentation

The actual overlap isomorphism of the affine local representer, in tensor coordinates.

Source context 11 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Algebra.Descent
open scoped TensorProduct
namespace EtaleCohomology
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
variable [Etale (Spec.map (CommRingCat.ofHom (algebraMap R B)))]
  [Etale (Spec.map (CommRingCat.ofHom (algebraMap B C)))]
variable (G : Sheaf (Spec (.of R)).smallEtaleTopology (Type u))
variable (h : ((etalePostcompose (Spec.map (CommRingCat.ofHom (algebraMap R B)))).op ⋙
    G.obj).RepresentableBy
  (affineRepresenterEtale B C))
include h
Lean source · statement
def affineRepresenterOverlapIso :
    Spec (.of (B ⊗[R] C)) ≅ Spec (.of (C ⊗[R] B))
lemma

affineRepresenterOverlapIso_base

L74 ↗
EtaleCohomology.affineRepresenterOverlapIso_base
Documentation

Both coordinates over the cover's self-pullback are preserved.

Source context 11 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Algebra.Descent
open scoped TensorProduct
namespace EtaleCohomology
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
variable [Etale (Spec.map (CommRingCat.ofHom (algebraMap R B)))]
  [Etale (Spec.map (CommRingCat.ofHom (algebraMap B C)))]
variable (G : Sheaf (Spec (.of R)).smallEtaleTopology (Type u))
variable (h : ((etalePostcompose (Spec.map (CommRingCat.ofHom (algebraMap R B)))).op ⋙
    G.obj).RepresentableBy
  (affineRepresenterEtale B C))
include h
Lean source · statement
lemma affineRepresenterOverlapIso_base :
    (affineRepresenterOverlapIso R B C G h).hom ≫
        Spec.map (CommRingCat.ofHom (affineOverlapSourceBase R B C).toRingHom) =
      Spec.map (CommRingCat.ofHom (affineOverlapTargetBase R B C).toRingHom)
lemma

affineRepresenterOverlapIso_diagonal

L104 ↗
EtaleCohomology.affineRepresenterOverlapIso_diagonal
Documentation

The universal section's unit law supplies diagonal normalization.

Source context 11 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Algebra.Descent
open scoped TensorProduct
namespace EtaleCohomology
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
variable [Etale (Spec.map (CommRingCat.ofHom (algebraMap R B)))]
  [Etale (Spec.map (CommRingCat.ofHom (algebraMap B C)))]
variable (G : Sheaf (Spec (.of R)).smallEtaleTopology (Type u))
variable (h : ((etalePostcompose (Spec.map (CommRingCat.ofHom (algebraMap R B)))).op ⋙
    G.obj).RepresentableBy
  (affineRepresenterEtale B C))
include h
Lean source · statement
lemma affineRepresenterOverlapIso_diagonal :
    Spec.map (CommRingCat.ofHom (tensorTargetDiagonal R B C).toRingHom) ≫
        (affineRepresenterOverlapIso R B C G h).hom =
      Spec.map (CommRingCat.ofHom (tensorSourceDiagonal R B C).toRingHom)
lemma

affineRepresenterOverlapIso_action

L135 ↗
EtaleCohomology.affineRepresenterOverlapIso_action
Documentation

The extracted action is the representer's actual geometric action in the changed coordinates.

Source context 11 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Algebra.Descent
open scoped TensorProduct
namespace EtaleCohomology
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
variable [Etale (Spec.map (CommRingCat.ofHom (algebraMap R B)))]
  [Etale (Spec.map (CommRingCat.ofHom (algebraMap B C)))]
variable (G : Sheaf (Spec (.of R)).smallEtaleTopology (Type u))
variable (h : ((etalePostcompose (Spec.map (CommRingCat.ofHom (algebraMap R B)))).op ⋙
    G.obj).RepresentableBy
  (affineRepresenterEtale B C))
include h
Lean source · statement
lemma affineRepresenterOverlapIso_action :
    affineOverlapAction R B C (affineRepresenterOverlapIso R B C G h) =
      pullbackActionCongr (Spec.map (CommRingCat.ofHom (algebraMap R B))) (Spec.map
        (CommRingCat.ofHom
        (algebraMap B C))) (Spec.map (CommRingCat.ofHom (algebraMap R C))) (specMap_tower R B C)
        (representerAction (Spec.map (CommRingCat.ofHom (algebraMap R B))) G
          (affineRepresenterEtale B C) h)
lemma

affineRepresenterOverlapIso_actionLaw

L147 ↗
EtaleCohomology.affineRepresenterOverlapIso_actionLaw
Documentation

The genuine triple-pullback action law of the local representer.

Source context 11 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Algebra.Descent
open scoped TensorProduct
namespace EtaleCohomology
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
variable [Etale (Spec.map (CommRingCat.ofHom (algebraMap R B)))]
  [Etale (Spec.map (CommRingCat.ofHom (algebraMap B C)))]
variable (G : Sheaf (Spec (.of R)).smallEtaleTopology (Type u))
variable (h : ((etalePostcompose (Spec.map (CommRingCat.ofHom (algebraMap R B)))).op ⋙
    G.obj).RepresentableBy
  (affineRepresenterEtale B C))
include h
Lean source · statement
lemma affineRepresenterOverlapIso_actionLaw :
    pullbackActionStep (Spec.map (CommRingCat.ofHom (algebraMap R B))) (Spec.map (CommRingCat.ofHom
      (algebraMap R C)))
        (affineOverlapAction R B C (affineRepresenterOverlapIso R B C G h))
        (affineOverlapAction_base R B C _ (affineRepresenterOverlapIso_base R B C G h)) ≫
          affineOverlapAction R B C (affineRepresenterOverlapIso R B C G h) =
      pullbackSkipMiddle (Spec.map (CommRingCat.ofHom (algebraMap R B))) (Spec.map
        (CommRingCat.ofHom
        (algebraMap R C))) ≫
        affineOverlapAction R B C (affineRepresenterOverlapIso R B C G h)
def

affineRepresenterAlgEquiv

L170 ↗
EtaleCohomology.affineRepresenterAlgEquiv
Documentation

The algebra overlap equivalence supplied by the actual affine local representer.

Source context 11 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Algebra.Descent
open scoped TensorProduct
namespace EtaleCohomology
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
variable [Etale (Spec.map (CommRingCat.ofHom (algebraMap R B)))]
  [Etale (Spec.map (CommRingCat.ofHom (algebraMap B C)))]
variable (G : Sheaf (Spec (.of R)).smallEtaleTopology (Type u))
variable (h : ((etalePostcompose (Spec.map (CommRingCat.ofHom (algebraMap R B)))).op ⋙
    G.obj).RepresentableBy
  (affineRepresenterEtale B C))
include h
Lean source · statement
def affineRepresenterAlgEquiv : C ⊗[R] B ≃ₐ[B] B ⊗[R] C
lemma

affineRepresenterAlgEquiv_diagonal

L175 ↗
EtaleCohomology.affineRepresenterAlgEquiv_diagonal
Documentation

The constructed algebra overlap is normalized on the diagonal.

Source context 11 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Algebra.Descent
open scoped TensorProduct
namespace EtaleCohomology
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
variable [Etale (Spec.map (CommRingCat.ofHom (algebraMap R B)))]
  [Etale (Spec.map (CommRingCat.ofHom (algebraMap B C)))]
variable (G : Sheaf (Spec (.of R)).smallEtaleTopology (Type u))
variable (h : ((etalePostcompose (Spec.map (CommRingCat.ofHom (algebraMap R B)))).op ⋙
    G.obj).RepresentableBy
  (affineRepresenterEtale B C))
include h
Lean source · statement
lemma affineRepresenterAlgEquiv_diagonal :
    (tensorTargetDiagonal R B C).comp (affineRepresenterAlgEquiv R B C G h).toAlgHom =
      tensorSourceDiagonal R B C
lemma

affineRepresenterAlgEquiv_cocycle

L182 ↗
EtaleCohomology.affineRepresenterAlgEquiv_cocycle
Documentation

The full tensor cocycle follows from the original sheaf's representing equivalence.

Source context 11 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Algebra.Descent
open scoped TensorProduct
namespace EtaleCohomology
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
variable [Etale (Spec.map (CommRingCat.ofHom (algebraMap R B)))]
  [Etale (Spec.map (CommRingCat.ofHom (algebraMap B C)))]
variable (G : Sheaf (Spec (.of R)).smallEtaleTopology (Type u))
variable (h : ((etalePostcompose (Spec.map (CommRingCat.ofHom (algebraMap R B)))).op ⋙
    G.obj).RepresentableBy
  (affineRepresenterEtale B C))
include h
Lean source · statement
lemma affineRepresenterAlgEquiv_cocycle :
    tensorCocycleLeft R B C (affineRepresenterAlgEquiv R B C G h) =
      tensorCocycleRight R B C (affineRepresenterAlgEquiv R B C G h)

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