Module

ExtendedFiberGaloisAction.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.ExtendedFiberGaloisAction

2 declarations indexed from sourceView source ↗

Module documentation

The literal point action of the extended residue Galois comparison

The canonical extension of the separable-closure fiber carries a compatible automorphism to its actual spectrum action on the larger geometric point. The original fundamental-group morphism preserves this same point action.

Imports2

Imported by5

theorem

absoluteGaloisToExtendedFiberAut_point

L32 ↗

AlgebraicGeometry.FiniteEtale.absoluteGaloisToExtendedFiberAut_point

Documentation

The extended-fiber Galois comparison uses the given compatible field map on every actual geometric point.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (k C Ω : Type u) [Field k] [Field C] [Field Ω]
  [Algebra k C] [IsSepClosure k C] [Algebra C Ω] [Algebra k Ω]
  [IsScalarTower k C Ω] [IsSepClosed Ω]

Lean source · statement

theorem absoluteGaloisToExtendedFiberAut_point
    (σ : Gal(C/k)) (ρ : Ω →+* Ω)
    (hρ : ρ.comp (algebraMap C Ω) = (algebraMap C Ω).comp σ.toRingHom)
    (X : FiniteEtale (Spec (.of k))) (x : (fib k Ω).obj X) :
    (fiberObjEquivHom (ξ k Ω) X
      ((absoluteGaloisToExtendedFiberAut k C Ω σ).hom.app X x)).left =
      Spec.map (CommRingCat.ofHom ρ) ≫ (fiberObjEquivHom (ξ k Ω) X x).left

theorem

fundamentalGroupHom_point_of_point_action

L76 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_point_of_point_action