Module

FieldSourceGaloisPoint.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.FieldSourceGaloisPoint

1 declaration indexed from sourceView source ↗

Module documentation

The actual point action of the supplied Galois comparison

This computation is proved over abstract fields, so callers retain their original field structures without unfolding the construction of the fiber automorphism group at those concrete fields.

Imports1

Nyll.EtaleFundamentalGroups.GeometricFiber.FieldSourceGalois

Imported by3

theorem

suppliedGaloisEquivFundamentalGroup_point

L29 ↗

AlgebraicGeometry.FiniteEtale.suppliedGaloisEquivFundamentalGroup_point

Documentation

The supplied Galois automorphism acts by its literal spectrum map.

Source context 5 commands

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

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

Lean source · statement

theorem suppliedGaloisEquivFundamentalGroup_point
    (σ : Gal(Ω/F)) (X : FiniteEtale (Spec (.of F))) (x : (fib F Ω).obj X) :
    (fiberObjEquivHom (ξ F Ω) X
      ((suppliedGaloisEquivFundamentalGroup F Ω σ).hom.app X x)).left =
      Spec.map (CommRingCat.ofHom σ.toRingHom) ≫
        (fiberObjEquivHom (ξ F Ω) X x).left

Module documentation

The actual point action of the supplied Galois comparison

Declarations

suppliedGaloisEquivFundamentalGroup_point