Module

DeckOverComparison.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.DeckOverComparison

7 declarations indexed from sourceView source ↗

Module documentation

Geometric deck pullback and the over-category

Pullback along an actual deck automorphism of a finite étale cover is identified with inverse postcomposition in its over-category. The comparison is the actual first projection of the scheme pullback.

Imports1

Nyll.EtaleFundamentalGroups.GeometricFiber.PointedCover

Imported by2

def

deckSchemeIso

L28 ↗

AlgebraicGeometry.FiniteEtale.deckSchemeIso

Documentation

The scheme isomorphism underlying an actual deck transformation.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} (A : FiniteEtale S) (σ : Aut A)

Lean source · full declaration

def deckSchemeIso : A.left ≅ A.left where
  hom := σ.hom.left
  inv := σ.inv.left
  hom_inv_id := congrArg (fun f : A ⟶ A => f.left) σ.hom_inv_id
  inv_hom_id := congrArg (fun f : A ⟶ A => f.left) σ.inv_hom_id

theorem

deck_hom_inv

L34 ↗

AlgebraicGeometry.FiniteEtale.deck_hom_inv

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} (A : FiniteEtale S) (σ : Aut A)

Lean source · statement

theorem deck_hom_inv :
    σ.hom.left ≫ σ.inv.left = 𝟙 A.left

theorem

deck_inv_hom

L38 ↗

AlgebraicGeometry.FiniteEtale.deck_inv_hom

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} (A : FiniteEtale S) (σ : Aut A)

Lean source · statement

theorem deck_inv_hom :
    σ.inv.left ≫ σ.hom.left = 𝟙 A.left

def

deckPullbackSourceIso

L42 ↗

AlgebraicGeometry.FiniteEtale.deckPullbackSourceIso

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} (A : FiniteEtale S) (σ : Aut A)

Lean source · full declaration

def deckPullbackSourceIso (B : FiniteEtale A.left) :
    Limits.pullback B.hom σ.hom.left ≅ B.left where
  hom := Limits.pullback.fst B.hom σ.hom.left
  inv := Limits.pullback.lift (𝟙 B.left) (B.hom ≫ σ.inv.left) (by
    rw [Category.id_comp, Category.assoc, deck_inv_hom A σ]
    exact (Category.comp_id B.hom).symm)
  hom_inv_id := by
    apply Limits.pullback.hom_ext
    · rw [Category.assoc, Limits.pullback.lift_fst, Category.comp_id,
        Category.id_comp]
    · rw [Category.assoc, Limits.pullback.lift_snd, ← Category.assoc,
        Limits.pullback.condition, Category.assoc,
        deck_hom_inv A σ, Category.comp_id, Category.id_comp]
  inv_hom_id := Limits.pullback.lift_fst _ _ _

def

deckPullbackOverObjIso

L57 ↗

AlgebraicGeometry.FiniteEtale.deckPullbackOverObjIso

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} (A : FiniteEtale S) (σ : Aut A)

Lean source · statement

def deckPullbackOverObjIso (B : FiniteEtale A.left) :
    (overEquiv A).functor.obj ((pullback σ.hom.left).obj B) ≅
      (Over.map σ.inv).obj ((overEquiv A).functor.obj B)

def

deckPullbackOverIso

L76 ↗

AlgebraicGeometry.FiniteEtale.deckPullbackOverIso

Documentation

Actual scheme pullback by a deck transformation is inverse postcomposition under the finite-étale over-category equivalence.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} (A : FiniteEtale S) (σ : Aut A)

Lean source · statement

def deckPullbackOverIso :
    pullback σ.hom.left ⋙ (overEquiv A).functor ≅
      (overEquiv A).functor ⋙ Over.map σ.inv

theorem

deckPullbackOverIso_hom_left

L89 ↗

AlgebraicGeometry.FiniteEtale.deckPullbackOverIso_hom_left

Documentation

The comparison uses the actual first projection, not a chosen isomorphism between the covering schemes.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
variable {S : Scheme.{u}} (A : FiniteEtale S) (σ : Aut A)

Lean source · statement

theorem deckPullbackOverIso_hom_left (B : FiniteEtale A.left) :
    ((deckPullbackOverIso A σ).hom.app B).left.left =
      Limits.pullback.fst B.hom σ.hom.left

Module documentation

Geometric deck pullback and the over-category

Declarations

deckSchemeIso

deck_hom_inv

deck_inv_hom

deckPullbackSourceIso

deckPullbackOverObjIso

deckPullbackOverIso

deckPullbackOverIso_hom_left