NYLL
Module

FieldFundamentalGroupConjugacy.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.FieldFundamentalGroupConjugacy
7 declarations indexed from sourceView source ↗

Module documentation

The canonical field fundamental-group map

The field-specific comparison of geometric fibers agrees with the usual fundamental-group map after transporting the composite geometric point to the chosen point. The only remaining ambiguity is the explicit inner conjugation obtained by comparing the two fiber-functor isomorphisms.

Imports1
Imported by8

Declarations

def

fieldBasePointFiberIso

L37 ↗
AlgebraicGeometry.FiniteEtale.fieldBasePointFiberIso
Documentation

Transport of the canonical composite geometric point to the geometric point defined by the composite algebra map.

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
variable (k K Omega : Type u)
variable [Field k] [Field K] [Field Omega]
variable [Algebra k K] [Algebra K Omega] [Algebra k Omega]
variable [IsScalarTower k K Omega] [IsSepClosed Omega]
Lean source · statement
def fieldBasePointFiberIso :
    fiber (ξ K Omega ≫ ξ k K) ≅ fib k Omega
def

fieldUntransportedPullbackFiberIso

L43 ↗
AlgebraicGeometry.FiniteEtale.fieldUntransportedPullbackFiberIso
Documentation

The field-specific comparison with its target transported back to the literal composite geometric 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
variable (k K Omega : Type u)
variable [Field k] [Field K] [Field Omega]
variable [Algebra k K] [Algebra K Omega] [Algebra k Omega]
variable [IsScalarTower k K Omega] [IsSepClosed Omega]
Lean source · statement
def fieldUntransportedPullbackFiberIso :
    pullback (ξ k K) ⋙ fib K Omega ≅ fiber (ξ K Omega ≫ ξ k K)
def

fieldFundamentalGroupComparisonAut

L50 ↗
AlgebraicGeometry.FiniteEtale.fieldFundamentalGroupComparisonAut
Documentation

The explicit automorphism measuring the difference between the canonical transported comparison and the field-specific comparison.

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
variable (k K Omega : Type u)
variable [Field k] [Field K] [Field Omega]
variable [Algebra k K] [Algebra K Omega] [Algebra k Omega]
variable [IsScalarTower k K Omega] [IsSepClosed Omega]
Lean source · statement
def fieldFundamentalGroupComparisonAut : Aut (fib k Omega)
theorem

conjAut_symm_cancel

L56 ↗
AlgebraicGeometry.FiniteEtale.conjAut_symm_cancel
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
variable (k K Omega : Type u)
variable [Field k] [Field K] [Field Omega]
variable [Algebra k K] [Algebra K Omega] [Algebra k Omega]
variable [IsScalarTower k K Omega] [IsSepClosed Omega]
Lean source · statement
theorem conjAut_symm_cancel
    {C : Type u} [Category C] {F G : C}
    (p : F ≅ G) (a : Aut G) :
    p.conjAut (p.symm.conjAut a) = a
theorem

conjAut_inner

L65 ↗
AlgebraicGeometry.FiniteEtale.conjAut_inner
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
variable (k K Omega : Type u)
variable [Field k] [Field K] [Field Omega]
variable [Algebra k K] [Algebra K Omega] [Algebra k Omega]
variable [IsScalarTower k K Omega] [IsSepClosed Omega]
Lean source · statement
theorem conjAut_inner
    {C : Type u} [Category C] {F G : C}
    (p : F ≅ G) (a b : Aut F) :
    p.conjAut (MulAut.conj a b) =
      MulAut.conj (p.conjAut a) (p.conjAut b)
theorem

fieldFundamentalGroupHom_eq_conj_core

L72 ↗
AlgebraicGeometry.FiniteEtale.fieldFundamentalGroupHom_eq_conj_core
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
variable (k K Omega : Type u)
variable [Field k] [Field K] [Field Omega]
variable [Algebra k K] [Algebra K Omega] [Algebra k Omega]
variable [IsScalarTower k K Omega] [IsSepClosed Omega]
Lean source · statement
theorem fieldFundamentalGroupHom_eq_conj_core
    (sigma : Aut (fib K Omega)) :
    CategoryTheory.PreGaloisCategory.autHomOfCompIso
        (pullback (ξ k K))
        (fieldUntransportedPullbackFiberIso k K Omega) sigma =
      MulAut.conj
        (G := Aut (fiber (ξ K Omega ≫ ξ k K)))
        ((pullbackFiberIso (ξ k K) (ξ K Omega)).symm ≪≫
          fieldUntransportedPullbackFiberIso k K Omega)
        (fundamentalGroupHom (ξ k K) (ξ K Omega) sigma)
theorem

fieldFundamentalGroupHom_eq_conj_fundamentalGroupHom

L89 ↗
AlgebraicGeometry.FiniteEtale.fieldFundamentalGroupHom_eq_conj_fundamentalGroupHom
Documentation

After transport along the equality of base points, the field-specific fundamental-group homomorphism differs from the usual one precisely by inner conjugation with fieldFundamentalGroupComparisonAut.

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
variable (k K Omega : Type u)
variable [Field k] [Field K] [Field Omega]
variable [Algebra k K] [Algebra K Omega] [Algebra k Omega]
variable [IsScalarTower k K Omega] [IsSepClosed Omega]
Lean source · statement
theorem fieldFundamentalGroupHom_eq_conj_fundamentalGroupHom
    (sigma : Aut (fib K Omega)) :
    fieldFundamentalGroupHom k K Omega inferInstance sigma =
      MulAut.conj (G := Aut (fib k Omega))
        (fieldFundamentalGroupComparisonAut k K Omega)
        ((fieldBasePointFiberIso k K Omega).conjAut
          (fundamentalGroupHom (ξ k K) (ξ K Omega) sigma))

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