NYLL
Module

FundamentalGroupComposition.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.FundamentalGroupComposition
11 declarations indexed from sourceView source ↗

Module documentation

Composition of maps on geometric fundamental groups

The canonical pullback comparisons for two successive scheme morphisms give the same map on fundamental groups as the corresponding composite pullback comparison. Two factorizations of one scheme morphism therefore induce maps which differ by an explicit inner automorphism.

Imports2
Imported by9

Declarations

instance

finiteEtaleOverCategoryComposition

L28 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategoryComposition
Source context 5 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
instance finiteEtaleOverCategoryComposition (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S)
instance

finiteEtaleHasPullbacksAlongComposition

L33 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongComposition
Source context 6 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategoryComposition (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
Lean source · statement
instance finiteEtaleHasPullbacksAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
instance

finiteEtaleStableUnderBaseChangeAlongComposition

L39 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongComposition
Source context 7 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategoryComposition (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
local instance finiteEtaleHasPullbacksAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
Lean source · statement
instance finiteEtaleStableUnderBaseChangeAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
def

pullbackCompositeFiberIso

L51 ↗
AlgebraicGeometry.FiniteEtale.pullbackCompositeFiberIso
Documentation

The fiber comparison obtained by composing the two canonical pullback comparisons and the canonical comparison of iterated pullbacks.

Source context 10 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategoryComposition (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
local instance finiteEtaleHasPullbacksAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X Y Z : Scheme.{u}}
variable {Omega : Type u} [Field Omega]
Lean source · statement
def pullbackCompositeFiberIso
    (f : X ⟶ Y) (g : Y ⟶ Z) (xi : Spec (.of Omega) ⟶ X) :
    pullback (f ≫ g) ⋙ fiber xi ≅ fiber ((xi ≫ f) ≫ g)
theorem

pullbackComp_conjAut

L63 ↗
AlgebraicGeometry.FiniteEtale.pullbackComp_conjAut
Source context 10 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategoryComposition (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
local instance finiteEtaleHasPullbacksAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X Y Z : Scheme.{u}}
variable {Omega : Type u} [Field Omega]
Lean source · statement
theorem pullbackComp_conjAut
    (f : X ⟶ Y) (g : Y ⟶ Z) (xi : Spec (.of Omega) ⟶ X)
    (a : π₁ᵉᵗ(xi)) :
      (Functor.isoWhiskerRight
        (MorphismProperty.Over.pullbackComp (P := @IsFiniteEtale) (Q := ⊤) f g)
        (fiber xi)).conjAut
          (((Functor.whiskeringLeft _ _ FintypeCat).obj (pullback (f ≫ g))).mapAut
            (fiber xi) a) =
        (((Functor.whiskeringLeft _ _ FintypeCat).obj
          (pullback g ⋙ pullback f)).mapAut (fiber xi) a)
theorem

pullbackCompositeFiberIso_conjAut

L91 ↗
AlgebraicGeometry.FiniteEtale.pullbackCompositeFiberIso_conjAut
Source context 10 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategoryComposition (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
local instance finiteEtaleHasPullbacksAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X Y Z : Scheme.{u}}
variable {Omega : Type u} [Field Omega]
Lean source · statement
theorem pullbackCompositeFiberIso_conjAut
    (f : X ⟶ Y) (g : Y ⟶ Z) (xi : Spec (.of Omega) ⟶ X)
    (b : Aut (pullback (f ≫ g) ⋙ fiber xi)) :
    (pullbackCompositeFiberIso f g xi).conjAut b =
      (pullbackFiberIso g (xi ≫ f)).conjAut
        ((Functor.isoWhiskerLeft (pullback g) (pullbackFiberIso f xi)).conjAut
          ((Functor.associator (pullback g) (pullback f) (fiber xi)).conjAut
            ((Functor.isoWhiskerRight
              (MorphismProperty.Over.pullbackComp (P := @IsFiniteEtale) (Q := ⊤) f g)
              (fiber xi)).conjAut b)))
theorem

fundamentalGroupHom_comp_eq_autHomOfCompIso

L112 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_comp_eq_autHomOfCompIso
Documentation

Successive fundamental-group maps are the map induced by the composite pullback comparison.

Source context 10 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategoryComposition (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
local instance finiteEtaleHasPullbacksAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X Y Z : Scheme.{u}}
variable {Omega : Type u} [Field Omega]
Lean source · statement
theorem fundamentalGroupHom_comp_eq_autHomOfCompIso
    (f : X ⟶ Y) (g : Y ⟶ Z) (xi : Spec (.of Omega) ⟶ X)
    (a : π₁ᵉᵗ(xi)) :
    fundamentalGroupHom g (xi ≫ f) (fundamentalGroupHom f xi a) =
      CategoryTheory.PreGaloisCategory.autHomOfCompIso
        (pullback (f ≫ g)) (pullbackCompositeFiberIso f g xi) a
def

pullbackCompositeFiberIsoOfEq

L157 ↗
AlgebraicGeometry.FiniteEtale.pullbackCompositeFiberIsoOfEq
Documentation

The composite pullback comparison transported to specified equal composite morphisms and equal target geometric points.

Source context 10 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategoryComposition (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
local instance finiteEtaleHasPullbacksAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X Y Z : Scheme.{u}}
variable {Omega : Type u} [Field Omega]
Lean source · statement
def pullbackCompositeFiberIsoOfEq
    (f : X ⟶ Y) (g : Y ⟶ Z) (m : X ⟶ Z) (hm : m = f ≫ g)
    (xi : Spec (.of Omega) ⟶ X) (eta : Spec (.of Omega) ⟶ Z)
    (heta : (xi ≫ f) ≫ g = eta) :
    pullback m ⋙ fiber xi ≅ fiber eta
theorem

fundamentalGroupHom_comp_transport_eq_autHomOfCompIso

L173 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_comp_transport_eq_autHomOfCompIso
Documentation

Transporting the target point in a successive fundamental-group map gives the map induced by the transported composite pullback comparison.

Source context 10 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategoryComposition (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
local instance finiteEtaleHasPullbacksAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X Y Z : Scheme.{u}}
variable {Omega : Type u} [Field Omega]
Lean source · statement
theorem fundamentalGroupHom_comp_transport_eq_autHomOfCompIso
    (f : X ⟶ Y) (g : Y ⟶ Z) (m : X ⟶ Z) (hm : m = f ≫ g)
    (xi : Spec (.of Omega) ⟶ X) (eta : Spec (.of Omega) ⟶ Z)
    (heta : (xi ≫ f) ≫ g = eta) (a : π₁ᵉᵗ(xi)) :
    heta ▸ fundamentalGroupHom g (xi ≫ f) (fundamentalGroupHom f xi a) =
      CategoryTheory.PreGaloisCategory.autHomOfCompIso
        (pullback m) (pullbackCompositeFiberIsoOfEq f g m hm xi eta heta) a
def

fundamentalGroupFactorizationConjugator

L189 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupFactorizationConjugator
Documentation

The explicit inner automorphism comparing the fundamental-group maps obtained from two factorizations of one scheme morphism.

Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategoryComposition (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
local instance finiteEtaleHasPullbacksAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X Y Z : Scheme.{u}}
variable {Omega : Type u} [Field Omega]
variable {Y' : Scheme.{u}}
Lean source · statement
def fundamentalGroupFactorizationConjugator
    (f₁ : X ⟶ Y) (g₁ : Y ⟶ Z) (f₂ : X ⟶ Y') (g₂ : Y' ⟶ Z)
    (m : X ⟶ Z) (hm₁ : m = f₁ ≫ g₁) (hm₂ : m = f₂ ≫ g₂)
    (xi : Spec (.of Omega) ⟶ X) (eta : Spec (.of Omega) ⟶ Z)
    (heta₁ : (xi ≫ f₁) ≫ g₁ = eta)
    (heta₂ : (xi ≫ f₂) ≫ g₂ = eta) : π₁ᵉᵗ(eta)
theorem

fundamentalGroupHom_comp_conj_of_common_composite

L200 ↗
AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_comp_conj_of_common_composite
Documentation

The maps on fundamental groups associated to two factorizations of one scheme morphism agree up to the explicit inner automorphism above.

Source context 11 commands

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

noncomputable section
open CategoryTheory
open CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
local instance finiteEtaleOverCategoryComposition (S : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ S) :=
  instCategory S
local instance finiteEtaleHasPullbacksAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongComposition
    {S T : Scheme.{u}} (f : S ⟶ T) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
variable {X Y Z : Scheme.{u}}
variable {Omega : Type u} [Field Omega]
variable {Y' : Scheme.{u}}
Lean source · statement
theorem fundamentalGroupHom_comp_conj_of_common_composite
    (f₁ : X ⟶ Y) (g₁ : Y ⟶ Z) (f₂ : X ⟶ Y') (g₂ : Y' ⟶ Z)
    (m : X ⟶ Z) (hm₁ : m = f₁ ≫ g₁) (hm₂ : m = f₂ ≫ g₂)
    (xi : Spec (.of Omega) ⟶ X) (eta : Spec (.of Omega) ⟶ Z)
    (heta₁ : (xi ≫ f₁) ≫ g₁ = eta)
    (heta₂ : (xi ≫ f₂) ≫ g₂ = eta) (a : π₁ᵉᵗ(xi)) :
    heta₁ ▸ fundamentalGroupHom g₁ (xi ≫ f₁)
        (fundamentalGroupHom f₁ xi a) =
      MulAut.conj
        (fundamentalGroupFactorizationConjugator
          f₁ g₁ f₂ g₂ m hm₁ hm₂ xi eta heta₁ heta₂)
        (heta₂ ▸ fundamentalGroupHom g₂ (xi ≫ f₂)
          (fundamentalGroupHom f₂ xi a))

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