NYLL
Module

Functoriality.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.Functoriality
6 declarations indexed from sourceView source ↗

Module documentation

Functoriality of the étale fundamental group

Pullback along a morphism of schemes commutes with taking the fiber at a field-valued point, in particular at a geometric point. The resulting comparison isomorphism induces the continuous homomorphism on automorphism groups of fiber functors.

Imports2
Imported by31

Declarations

instance

finiteEtaleOverCategoryFunctoriality

L31 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategoryFunctoriality
Source context 5 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
Lean source · statement
instance finiteEtaleOverCategoryFunctoriality (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X)
instance

finiteEtaleHasPullbacksAlongFunctoriality

L36 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongFunctoriality
Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryFunctoriality (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
Lean source · statement
instance finiteEtaleHasPullbacksAlongFunctoriality
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
instance

finiteEtaleStableUnderBaseChangeAlongFunctoriality

L42 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongFunctoriality
Source context 7 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryFunctoriality (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongFunctoriality
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
Lean source · statement
instance finiteEtaleStableUnderBaseChangeAlongFunctoriality
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
def

pullbackFiberIso

L53 ↗
AlgebraicGeometry.FiniteEtale.pullbackFiberIso
Documentation

Pulling a finite étale cover back along f and then taking its fiber at ξ is naturally isomorphic to taking the fiber at the composite point.

Source context 9 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryFunctoriality (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongFunctoriality
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongFunctoriality
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X Y : Scheme.{u}} {Ω : Type u} [Field Ω]
Lean source · statement
def pullbackFiberIso (f : X ⟶ Y) (ξ : Spec (.of Ω) ⟶ X) :
    pullback f ⋙ fiber ξ ≅ fiber (ξ ≫ f)
def

fundamentalGroupHom

L65 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupHom
Documentation

A morphism of schemes induces a continuous homomorphism from the automorphism group of the fiber functor at a field-valued point to that at the composite point. For a geometric point these are the étale fundamental groups.

Source context 9 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryFunctoriality (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongFunctoriality
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongFunctoriality
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X Y : Scheme.{u}} {Ω : Type u} [Field Ω]
Lean source · statement
def fundamentalGroupHom (f : X ⟶ Y) (ξ : Spec (.of Ω) ⟶ X) :
    π₁ᵉᵗ(ξ) →ₜ* π₁ᵉᵗ(ξ ≫ f)
theorem

fundamentalGroupHom_eq_conj_of_comparison

L72 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_eq_conj_of_comparison
Documentation

Replacing the canonical fiber comparison by another one changes the induced homomorphism by the corresponding inner conjugation.

Source context 9 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryFunctoriality (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) :=
  instCategory X
local instance finiteEtaleHasPullbacksAlongFunctoriality
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongFunctoriality
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X Y : Scheme.{u}} {Ω : Type u} [Field Ω]
Lean source · statement
theorem fundamentalGroupHom_eq_conj_of_comparison
    (f : X ⟶ Y) (ξ : Spec (.of Ω) ⟶ X)
    (t : pullback f ⋙ fiber ξ ≅ fiber (ξ ≫ f))
    (σ : π₁ᵉᵗ(ξ)) :
    CategoryTheory.PreGaloisCategory.autHomOfCompIso (pullback f) t σ =
      MulAut.conj (G := π₁ᵉᵗ(ξ ≫ f))
        ((pullbackFiberIso f ξ).symm ≪≫ t)
        (fundamentalGroupHom f ξ σ)

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