NYLL
Module

HenselianSpecializationConjugacy.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.HenselianSpecializationConjugacy
2 declarations indexed from sourceView source ↗

Module documentation

Point actions under the canonical specialization conjugation

The explicit natural fiber comparison transports the actual generic point action to the actual residue point action. Equality of geometric-point maps also preserves the literal point-action formula.

Imports2
Imported by6

Declarations

theorem

point_action_of_eqToIso

L27 ↗
AlgebraicGeometry.FiniteEtale.point_action_of_eqToIso
Documentation

Transport along equality of geometric points preserves a literal point action.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
theorem point_action_of_eqToIso
    {S : Scheme.{u}} {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    {s t : Spec (.of Ω) ⟶ S} (h : s = t)
    (a : π₁ᵉᵗ(s)) (ρ : Ω →+* Ω)
    (ha : ∀ (X : FiniteEtale S) (x : (fiber s).obj X),
      (fiberObjEquivHom s X (a.hom.app X x)).left =
        Spec.map (CommRingCat.ofHom ρ) ≫ (fiberObjEquivHom s X x).left)
    (X : FiniteEtale S) (x : (fiber t).obj X) :
    (fiberObjEquivHom t X
      ((continuousConjAut (eqToIso (congrArg fiber h)) a).hom.app X x)).left =
      Spec.map (CommRingCat.ofHom ρ) ≫ (fiberObjEquivHom t X x).left
theorem

henselianSpecializationFundamentalGroupEquiv_point

L48 ↗
AlgebraicGeometry.FiniteEtale.henselianSpecializationFundamentalGroupEquiv_point
Documentation

Conjugation by the actual specialization identifies the two actual point actions.

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 (H R L : Type u) [CommRing H] [CommRing R]
  [HenselianLocalRing R] [IsIntegrallyClosed R] [Field L]
  [Algebra H R] [Algebra R L] [IsFractionRing R L]
  [Algebra H L] [IsScalarTower H R L]
  [IsSepClosed L] [IsSepClosed (IsLocalRing.ResidueField R)]
Lean source · statement
theorem henselianSpecializationFundamentalGroupEquiv_point
    (τ : R ≃ₐ[H] R) (σ : L ≃ₐ[H] L)
    (hσ : ∀ r : R, σ (algebraMap R L r) = algebraMap R L (τ r))
    (a : π₁ᵉᵗ(Spec.algebraMap H L))
    (ha : ∀ (X : FiniteEtale (Spec (.of H))) (x : (fiber (Spec.algebraMap H L)).obj X),
      (fiberObjEquivHom (Spec.algebraMap H L) X (a.hom.app X x)).left =
        Spec.map (CommRingCat.ofHom σ.toRingHom) ≫
          (fiberObjEquivHom (Spec.algebraMap H L) X x).left)
    (X : FiniteEtale (Spec (.of H)))
    (x : (fiber (Spec.algebraMap H (IsLocalRing.ResidueField R))).obj X) :
    (fiberObjEquivHom (Spec.algebraMap H (IsLocalRing.ResidueField R)) X
      ((henselianSpecializationFundamentalGroupEquiv H R L a).hom.app X x)).left =
      Spec.map (CommRingCat.ofHom (SchemeTheory.residueAlgEquiv H R τ).toRingHom) ≫
        (fiberObjEquivHom (Spec.algebraMap H (IsLocalRing.ResidueField R)) X x).left

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