NYLL
Module

AlgebraicClosure.lean

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

Module documentation

The absolute Galois group at an algebraic-closure geometric point

An extension of separably closed fields induces a canonical map of geometric fiber functors by precomposition on geometric points. This map is invertible: after comparison with any isomorphism of fiber functors, it is an endomorphism of a fiber functor, and every such endomorphism is invertible.

Applying this to the separable closure inside the algebraic closure identifies the absolute Galois group with the fundamental group at the algebraic-closure point. The finite-action equivalence respects both this group isomorphism and the forgetful functor to the geometric fiber.

Imports6
Imported by5

Declarations

def

fieldPointExtension

L45 ↗
AlgebraicGeometry.FiniteEtale.fieldPointExtension
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u) [Field k] [Field K] [Field Ω]
  [Algebra k K] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
section Extension
variable [IsSepClosed K] [IsSepClosed Ω]
Lean source · statement
def fieldPointExtension : Over.mk (ξ k Ω) ⟶ Over.mk (ξ k K)
def

fieldFiberExtension

L49 ↗
AlgebraicGeometry.FiniteEtale.fieldFiberExtension
Documentation

Extension of the geometric-point field, defined by precomposition on points.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u) [Field k] [Field K] [Field Ω]
  [Algebra k K] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
section Extension
variable [IsSepClosed K] [IsSepClosed Ω]
Lean source · full declaration
def fieldFiberExtension : fib k K ⟶ fib k Ω where
  app X := FintypeCat.homMk fun x ↦
    (fiberObjEquivHom (ξ k Ω) X).symm
      (fieldPointExtension k K Ω ≫ fiberObjEquivHom (ξ k K) X x)
  naturality X Y f := by
    apply FintypeCat.hom_ext
    intro x
    change (fiberObjEquivHom (ξ k Ω) Y).symm
        (fieldPointExtension k K Ω ≫
          fiberObjEquivHom (ξ k K) Y ((fib k K).map f x)) =
      (fib k Ω).map f ((fiberObjEquivHom (ξ k Ω) X).symm
        (fieldPointExtension k K Ω ≫ fiberObjEquivHom (ξ k K) X x))
    rw [fiberObjEquivHom_symm_naturality,
      ← fiberObjEquivHom_naturality (ξ k K) f x, Category.assoc]
lemma

fieldFiberExtension_isIso

L64 ↗
AlgebraicGeometry.FiniteEtale.fieldFiberExtension_isIso
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u) [Field k] [Field K] [Field Ω]
  [Algebra k K] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
section Extension
variable [IsSepClosed K] [IsSepClosed Ω]
Lean source · statement
lemma fieldFiberExtension_isIso : IsIso (fieldFiberExtension k K Ω)
def

fieldFiberExtensionIso

L72 ↗
AlgebraicGeometry.FiniteEtale.fieldFiberExtensionIso
Documentation

Extending a separably closed geometric-point field preserves the fiber functor.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u) [Field k] [Field K] [Field Ω]
  [Algebra k K] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
section Extension
variable [IsSepClosed K] [IsSepClosed Ω]
Lean source · statement
def fieldFiberExtensionIso : fib k K ≅ fib k Ω
lemma

fieldFiberExtensionIso_point

L77 ↗
AlgebraicGeometry.FiniteEtale.fieldFiberExtensionIso_point
Documentation

The canonical comparison sends a geometric point to its composite with the field extension.

Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u) [Field k] [Field K] [Field Ω]
  [Algebra k K] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
section Extension
variable [IsSepClosed K] [IsSepClosed Ω]
Lean source · statement
lemma fieldFiberExtensionIso_point (X : FiniteEtale (Spec (.of k)))
    (x : (fib k K).obj X) :
    (fiberObjEquivHom (ξ k Ω) X ((fieldFiberExtensionIso k K Ω).hom.app X x)).left =
      ξ K Ω ≫ (fiberObjEquivHom (ξ k K) X x).left
def

absoluteGaloisToSeparableFiberAut

L95 ↗
AlgebraicGeometry.FiniteEtale.absoluteGaloisToSeparableFiberAut
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u) [Field k] [Field K] [Field Ω]
  [Algebra k K] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
section AbsoluteGalois
variable [IsSepClosure k K] [IsSepClosed Ω]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def absoluteGaloisToSeparableFiberAut : (K ≃ₐ[k] K) ≃ₜ* Aut (fib k K)
def

absoluteGaloisToExtendedFiberAut

L103 ↗
AlgebraicGeometry.FiniteEtale.absoluteGaloisToExtendedFiberAut
Documentation

The absolute Galois group acts as all automorphisms of the extended geometric fiber.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u) [Field k] [Field K] [Field Ω]
  [Algebra k K] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
section AbsoluteGalois
variable [IsSepClosure k K] [IsSepClosed Ω]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def absoluteGaloisToExtendedFiberAut : (K ≃ₐ[k] K) ≃ₜ* Aut (fib k Ω)
def

equivContActionExtendedFiberIso

L108 ↗
AlgebraicGeometry.FiniteEtale.equivContActionExtendedFiberIso
Documentation

The finite Galois-set equivalence agrees with the equivalence at the extended point.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u) [Field k] [Field K] [Field Ω]
  [Algebra k K] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
section AbsoluteGalois
variable [IsSepClosure k K] [IsSepClosed Ω]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def equivContActionExtendedFiberIso :
    (equivContAction k K).functor ≅
      PreGaloisCategory.functorToContAction (fib k Ω) ⋙
        (ContAction.resEquiv FintypeCat (absoluteGaloisToExtendedFiberAut k K Ω)).functor
def

equivContActionExtendedFiberForgetIso

L133 ↗
AlgebraicGeometry.FiniteEtale.equivContActionExtendedFiberForgetIso
Documentation

Forgetting the finite Galois action gives the fiber at the extended geometric point.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u) [Field k] [Field K] [Field Ω]
  [Algebra k K] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
section AbsoluteGalois
variable [IsSepClosure k K] [IsSepClosed Ω]
attribute [local instance] IsSepClosure.sep_closed
Lean source · statement
def equivContActionExtendedFiberForgetIso :
    (equivContAction k K).functor ⋙
      forget₂ (ContAction FintypeCat.{u} (K ≃ₐ[k] K)) FintypeCat ≅ fib k Ω
def

absoluteGaloisEquivFundamentalGroup

L146 ↗
AlgebraicGeometry.FiniteEtale.absoluteGaloisEquivFundamentalGroup
Documentation

Stacks Project, Tag 0BNE. The absolute Galois group is the étale fundamental group of the field, based at its algebraic closure.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u) [Field k] [Field K] [Field Ω]
  [Algebra k K] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
Lean source · statement
def absoluteGaloisEquivFundamentalGroup (k : Type u) [Field k] :
    (SeparableClosure k ≃ₐ[k] SeparableClosure k) ≃ₜ* Aut (fib k (AlgebraicClosure k))
def

equivContActionAlgebraicClosureForgetIso

L151 ↗
AlgebraicGeometry.FiniteEtale.equivContActionAlgebraicClosureForgetIso
Documentation

The finite-action equivalence in Tag 0BNE commutes with the algebraic-closure fiber functor.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
variable (k K Ω : Type u) [Field k] [Field K] [Field Ω]
  [Algebra k K] [Algebra K Ω] [Algebra k Ω] [IsScalarTower k K Ω]
Lean source · statement
def equivContActionAlgebraicClosureForgetIso (k : Type u) [Field k] :
    (equivContAction k (SeparableClosure k)).functor ⋙
      forget₂ (ContAction FintypeCat.{u}
        (SeparableClosure k ≃ₐ[k] SeparableClosure k)) FintypeCat ≅
      fib k (AlgebraicClosure k)

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