Module

SelfProduct.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.SelfProduct

4 declarations indexed from sourceView source ↗

Module documentation

The self-product of an actual Galois cover

The graphs of deck transformations decompose the self-product of a Galois object. Applied to finite etale covers, the categorical product is the actual fiber product over the base scheme. This supplies the geometric relation space needed to replace Cech descent by Galois invariance.

The proof uses the established fiber functor and its actual simply transitive deck action; no splitting or comparison is assumed.

Imports4

Nyll.EtaleFundamentalGroups.GaloisCovers.Basic
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
Mathlib.CategoryTheory.Limits.Types.Colimits

Imported by2

def

galoisSelfProductMap

L33 ↗

CategoryTheory.PreGaloisCategory.galoisSelfProductMap

Documentation

The union of the actual graphs of all deck transformations.

Source context 5 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u} [Category.{v} C] [GaloisCategory C]

Lean source · full declaration

def galoisSelfProductMap (X : C) [IsGalois X] :
    (∐ fun _ : Aut X => X) ⟶ X ⨯ X :=
  Sigma.desc (fun σ : Aut X => prod.lift (𝟙 X) σ.hom)

theorem

galoisSelfProductMap_isIso

L39 ↗

CategoryTheory.PreGaloisCategory.galoisSelfProductMap_isIso

Documentation

Graphs of deck transformations give the self-product decomposition of a Galois object.

Source context 5 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u} [Category.{v} C] [GaloisCategory C]

Lean source · statement

theorem galoisSelfProductMap_isIso (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
    (X : C) [IsGalois X] : IsIso (galoisSelfProductMap X)

def

galoisSelfProductIso

L89 ↗

CategoryTheory.PreGaloisCategory.galoisSelfProductIso

Documentation

The canonical decomposition, with the graph map as its forward map.

Source context 5 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u} [Category.{v} C] [GaloisCategory C]

Lean source · full declaration

def galoisSelfProductIso (X : C) [IsGalois X] :
    (∐ fun _ : Aut X => X) ≅ X ⨯ X := by
  have : IsIso (galoisSelfProductMap X) :=
    galoisSelfProductMap_isIso (CategoryTheory.GaloisCategory.getFiberFunctor C) X
  exact asIso (galoisSelfProductMap X)

theorem

galoisSelfProductIso_ι

L95 ↗

CategoryTheory.PreGaloisCategory.galoisSelfProductIso_ι

Source context 5 commands

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

noncomputable section
universe u v w
open CategoryTheory Limits
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u} [Category.{v} C] [GaloisCategory C]

Lean source · full declaration

theorem galoisSelfProductIso_ι (X : C) [IsGalois X] (σ : Aut X) :
    Sigma.ι (fun _ : Aut X => X) σ ≫ (galoisSelfProductIso X).hom =
      prod.lift (𝟙 X) σ.hom := by
  change Sigma.ι (fun _ : Aut X => X) σ ≫ galoisSelfProductMap X = _
  exact Sigma.ι_comp_desc _ σ

Module documentation

The self-product of an actual Galois cover

Declarations

galoisSelfProductMap

galoisSelfProductMap_isIso

galoisSelfProductIso

galoisSelfProductIso_ι