Module

FieldPointedQuotient.lean

Nyll.EtaleFundamentalGroups.Inertia.FieldPointedQuotient

5 declarations indexed from sourceView source ↗

Module documentation

Pointed finite quotients over abstract fields

The actual pointed quotient and its canonical restriction map are constructed and compared before choosing an intermediate field or a separable closure. Their geometric points therefore use the same field structures throughout.

Imports6

Imported by3

def

fieldFiniteGaloisRestrictionHom

L41 ↗

EtaleFundamentalGroups.Inertia.fieldFiniteGaloisRestrictionHom

Documentation

Restriction from the chosen geometric-fiber fundamental group to a finite Galois extension.

Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups.Inertia
section Restriction
variable (K L Omega : Type u) [Field K] [Field L] [Field Omega]
variable [Algebra K L] [Algebra K Omega] [Algebra L Omega]
variable [IsScalarTower K L Omega]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable [IsSepClosed Omega] [IsSepClosure K Omega]

Lean source · statement

def fieldFiniteGaloisRestrictionHom :
    Aut (fib K Omega) →* Gal(L/K)

theorem

fieldCoverQuotient_eq_restriction

L46 ↗

EtaleFundamentalGroups.Inertia.fieldCoverQuotient_eq_restriction

Source context 11 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups.Inertia
section Restriction
variable (K L Omega : Type u) [Field K] [Field L] [Field Omega]
variable [Algebra K L] [Algebra K Omega] [Algebra L Omega]
variable [IsScalarTower K L Omega]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable [IsSepClosed Omega] [IsSepClosure K Omega]

Lean source · statement

theorem fieldCoverQuotient_eq_restriction :
    (EtaleFundamentalGroups.fieldGaloisToFiniteEtaleAutOpMulEquiv K L).symm.toMonoidHom.comp
      (EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom
        (ξ K Omega) (FiniteEtale.mk (ξ K L))
        (EtaleFundamentalGroups.fieldFiniteEtaleCover_isGalois K L)
        (EtaleFundamentalGroups.fieldFiniteEtaleCoverCanonicalPoint K L Omega)) =
      fieldFiniteGaloisRestrictionHom K L Omega

def

fieldPointedQuotientHom

L86 ↗

EtaleFundamentalGroups.Inertia.fieldPointedQuotientHom

Documentation

The actual pointed quotient of Spec L → Spec K along Spec F → Spec K, transporting the point induced by L → Omega along p. The default is the canonical comparison of the composite geometric point.

Source context 13 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups.Inertia
section Pointed
variable (K F L Omega : Type u)
variable [Field K] [Field F] [Field L] [Field Omega]
variable [Algebra K L] [Algebra K F]
variable [Algebra K Omega] [Algebra F Omega] [Algebra L Omega]
variable [IsScalarTower K L Omega] [IsScalarTower K F Omega]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable [IsSepClosed Omega] [IsSepClosure K Omega]

-- The nine data-bearing instances are the four fields and five algebras.
-- Each scalar target has one owner; the tower and closure witnesses are propositions.

Lean source · statement

def fieldPointedQuotientHom
    (p : fiber (ξ F Omega ≫ ξ K F) ≅ fib K Omega :=
      fieldBasePointFiberIso K F Omega) :
    Aut (fib F Omega) →* (Aut (FiniteEtale.mk (ξ K L)))ᵐᵒᵖ

def

fieldCanonicalUnconjugatedHom

L99 ↗

EtaleFundamentalGroups.Inertia.fieldCanonicalUnconjugatedHom

Documentation

The fundamental-group map followed by restriction to the finite Galois extension, with the composite geometric point transported along p. The default comparison is the canonical one.

Source context 13 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups.Inertia
section Pointed
variable (K F L Omega : Type u)
variable [Field K] [Field F] [Field L] [Field Omega]
variable [Algebra K L] [Algebra K F]
variable [Algebra K Omega] [Algebra F Omega] [Algebra L Omega]
variable [IsScalarTower K L Omega] [IsScalarTower K F Omega]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable [IsSepClosed Omega] [IsSepClosure K Omega]

-- The nine data-bearing instances are the four fields and five algebras.
-- Each scalar target has one owner; the tower and closure witnesses are propositions.

Lean source · statement

def fieldCanonicalUnconjugatedHom
    (p : fiber (ξ F Omega ≫ ξ K F) ≅ fib K Omega :=
      fieldBasePointFiberIso K F Omega) :
    Aut (fib F Omega) →* Gal(L/K)

theorem

fieldPointedQuotientHom_eq_canonicalUnconjugatedHom

L109 ↗

EtaleFundamentalGroups.Inertia.fieldPointedQuotientHom_eq_canonicalUnconjugatedHom

Documentation

Transporting the deck group of the actual pointed quotient to the finite Galois group gives the canonical unconjugated restriction map.

Source context 13 commands

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

noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups.Inertia
section Pointed
variable (K F L Omega : Type u)
variable [Field K] [Field F] [Field L] [Field Omega]
variable [Algebra K L] [Algebra K F]
variable [Algebra K Omega] [Algebra F Omega] [Algebra L Omega]
variable [IsScalarTower K L Omega] [IsScalarTower K F Omega]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable [IsSepClosed Omega] [IsSepClosure K Omega]

-- The nine data-bearing instances are the four fields and five algebras.
-- Each scalar target has one owner; the tower and closure witnesses are propositions.

Lean source · statement

theorem fieldPointedQuotientHom_eq_canonicalUnconjugatedHom
    (p : fiber (ξ F Omega ≫ ξ K F) ≅ fib K Omega :=
      fieldBasePointFiberIso K F Omega) :
    (EtaleFundamentalGroups.fieldGaloisToFiniteEtaleAutOpMulEquiv K L).symm.toMonoidHom.comp
      (fieldPointedQuotientHom K F L Omega p) =
      fieldCanonicalUnconjugatedHom K F L Omega p

Module documentation

Pointed finite quotients over abstract fields

Declarations

fieldFiniteGaloisRestrictionHom

fieldCoverQuotient_eq_restriction

fieldPointedQuotientHom

fieldCanonicalUnconjugatedHom

fieldPointedQuotientHom_eq_canonicalUnconjugatedHom