Nyll.EtaleFundamentalGroups.GeometricFiber.TransportedFieldSourcePoint

Module documentation

The complete point calculation for a transported actual field-source map

The supplied Galois comparison, the actual scheme-induced map, equality of geometric points, and the final projection to a geometric point are computed at abstract field and scheme structures. A caller supplies its proved actual automorphism and coefficient equalities, with no concrete fiber expansion.

theorem

transportedFieldSourceAbsoluteGaloisHom_point

L33 ↗

AlgebraicGeometry.FiniteEtale.transportedFieldSourceAbsoluteGaloisHom_point

Documentation

The complete actual field-source point action, after the specified geometric-point equality and the proved automorphism computation.

Source context 5 commands

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

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

Lean source · statement

theorem transportedFieldSourceAbsoluteGaloisHom_point
    (j : Spec (.of F) ⟶ S) (t : Spec (.of Ω) ⟶ S)
    (hpoint : ξ F Ω ≫ j = t)
    (σ : Gal(Ω/F)) (ρ : Ω →+* Ω) (hσ : σ.toRingHom = ρ)
    (a : π₁ᵉᵗ(t))
    (ha : a = continuousConjAut (eqToIso (congrArg fiber hpoint))
      (fieldSourceAbsoluteGaloisHom F Ω j σ))
    (X : FiniteEtale S) (x : (fiber t).obj X) :
    (fiberObjEquivHom t X (a.hom.app X x)).left =
      Spec.map (CommRingCat.ofHom ρ) ≫ (fiberObjEquivHom t X x).left

Module documentation

The complete point calculation for a transported actual field-source map

Declarations

transportedFieldSourceAbsoluteGaloisHom_point