Module

FieldSourceBasePointComparison.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.FieldSourceBasePointComparison

3 declarations indexed from sourceView source ↗

Module documentation

Comparing the strict-fraction and canonical fraction-point maps

The actual field comparison used for the inertia image is whiskered through the original scheme pullback. This constructs the target base-point comparison and proves the map square exactly, including its inner conjugator.

Imports3

Imported by2

theorem

fundamentalGroupHom_conjAut

L27 ↗

AlgebraicGeometry.FiniteEtale.fundamentalGroupHom_conjAut

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 fundamentalGroupHom_conjAut
    {S X : Scheme.{u}} {Ω Ω' : Type u} [Field Ω] [Field Ω']
    (r : S ⟶ X) (p : Spec (.of Ω) ⟶ S) (p' : Spec (.of Ω') ⟶ S)
    (s : fiber p ≅ fiber p') (τ : π₁ᵉᵗ(p)) :
    ((pullbackFiberIso r p).symm ≪≫
      Functor.isoWhiskerLeft (pullback r) s ≪≫ pullbackFiberIso r p').conjAut
        (fundamentalGroupHom r p τ) =
      fundamentalGroupHom r p' (s.conjAut τ)

def

fieldSourceComparisonFiberIso

L57 ↗

AlgebraicGeometry.FiniteEtale.fieldSourceComparisonFiberIso

Documentation

The base-point comparison on X induced by the actual field comparison used to identify the strict fraction-field inertia image.

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 E L : Type u) [Field F] [Field E] [Field L]
  [Algebra F E] [Algebra E L] [Algebra F L] [IsScalarTower F E L]
  [IsSepClosure F L] [IsSepClosed L]
  {X : Scheme.{u}} (r : Spec (.of F) ⟶ X)

Lean source · statement

def fieldSourceComparisonFiberIso :
    fiber ((ξ E L ≫ ξ F E) ≫ r) ≅ fiber (ξ F L ≫ r)

theorem

fieldSourceAbsoluteGaloisHom_comparison

L66 ↗

AlgebraicGeometry.FiniteEtale.fieldSourceAbsoluteGaloisHom_comparison

Documentation

The canonical Galois map and the strict-fraction comparison commute under the explicitly constructed target fibre isomorphism.

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 E L : Type u) [Field F] [Field E] [Field L]
  [Algebra F E] [Algebra E L] [Algebra F L] [IsScalarTower F E L]
  [IsSepClosure F L] [IsSepClosed L]
  {X : Scheme.{u}} (r : Spec (.of F) ⟶ X)

Lean source · statement

theorem fieldSourceAbsoluteGaloisHom_comparison
    (τ : π₁ᵉᵗ(ξ E L ≫ ξ F E)) :
    (fieldSourceComparisonFiberIso F E L r).conjAut
        (fundamentalGroupHom r (ξ E L ≫ ξ F E) τ) =
      fieldSourceAbsoluteGaloisHom F L r
        (((fieldBasePointFiberIso F E L).conjAut.trans
          (MulAut.conj (fieldFundamentalGroupComparisonAut F E L))).trans
            (absoluteGaloisToFiberAutMulEquiv F L inferInstance).symm τ)

Module documentation

Comparing the strict-fraction and canonical fraction-point maps

Declarations

fundamentalGroupHom_conjAut

fieldSourceComparisonFiberIso

fieldSourceAbsoluteGaloisHom_comparison