NYLL
Module

FieldSourceGalois.lean

Nyll.EtaleFundamentalGroups.GeometricFiber.FieldSourceGalois
12 declarations indexed from sourceView source ↗

Module documentation

Generic Galois maps using the supplied separable closure

The field source is a dominant preimmersion, so it is the actual generic point, rather than a further extension of the function field. The ambient separable closure is supplied explicitly. Finite fixed subfields are characterized using their literal spectra and finite étale models.

Imports9
Imported by4

Declarations

def

suppliedGaloisEquivFundamentalGroup

L39 ↗
AlgebraicGeometry.FiniteEtale.suppliedGaloisEquivFundamentalGroup
Documentation

The canonical topological comparison for the supplied separable closure.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (F Ω : Type u) [Field F] [Field Ω] [Algebra F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
Lean source · statement
def suppliedGaloisEquivFundamentalGroup : Gal(Ω/F) ≃ₜ* Aut (fib F Ω)
def

fieldSourceAbsoluteGaloisHom

L50 ↗
AlgebraicGeometry.FiniteEtale.fieldSourceAbsoluteGaloisHom
Documentation

The actual map induced by the given generic-point morphism.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (F Ω : Type u) [Field F] [Field Ω] [Algebra F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
variable {X : Scheme.{u}} [IsIntegral X]
  (j : Spec (.of F) ⟶ X)
Lean source · statement
def fieldSourceAbsoluteGaloisHom : Gal(Ω/F) →ₜ* π₁ᵉᵗ(ξ F Ω ≫ j)
theorem

fieldSourceAbsoluteGaloisHom_surjective

L56 ↗
AlgebraicGeometry.FiniteEtale.fieldSourceAbsoluteGaloisHom_surjective
Documentation

Dominant preimmersion of the field source supplies surjectivity.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (F Ω : Type u) [Field F] [Field Ω] [Algebra F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
variable {X : Scheme.{u}} [IsIntegral X]
  (j : Spec (.of F) ⟶ X)
Lean source · statement
theorem fieldSourceAbsoluteGaloisHom_surjective [IsNormalIntegral X]
    [IsPreimmersion j] [IsDominant j] [QuasiCompact j] :
    Function.Surjective (fieldSourceAbsoluteGaloisHom F Ω j)
def

fieldSourcePullbackContActionIso

L63 ↗
AlgebraicGeometry.FiniteEtale.fieldSourcePullbackContActionIso
Documentation

Generic pullback agrees with restriction of the supplied Galois action.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (F Ω : Type u) [Field F] [Field Ω] [Algebra F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
variable {X : Scheme.{u}} [IsIntegral X]
  (j : Spec (.of F) ⟶ X)
Lean source · statement
def fieldSourcePullbackContActionIso :
    pullback j ⋙ (equivContAction F Ω).functor ≅
      functorToContAction (fiber (ξ F Ω ≫ j)) ⋙
        ContAction.res FintypeCat (fieldSourceAbsoluteGaloisHom F Ω j)
theorem

fieldSourcePullback_essImage_iff_ker_le_ker_ρAut

L78 ↗
AlgebraicGeometry.FiniteEtale.fieldSourcePullback_essImage_iff_ker_le_ker_ρAut
Documentation

A finite continuous action extends to X exactly when the actual kernel acts trivially.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (F Ω : Type u) [Field F] [Field Ω] [Algebra F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
variable {X : Scheme.{u}} [IsIntegral X]
  (j : Spec (.of F) ⟶ X)
Lean source · statement
theorem fieldSourcePullback_essImage_iff_ker_le_ker_ρAut [IsNormalIntegral X]
    [IsPreimmersion j] [IsDominant j] [QuasiCompact j]
    (Y : ContAction FintypeCat.{u} Gal(Ω/F)) :
    (pullback j ⋙ (equivContAction F Ω).functor).essImage Y ↔
      (fieldSourceAbsoluteGaloisHom F Ω j).toMonoidHom.ker ≤ (Action.ρAut Y.obj).ker
theorem

fieldSourcePullback_obj_essImage_iff_ker_le_ker_ρAut

L90 ↗
AlgebraicGeometry.FiniteEtale.fieldSourcePullback_obj_essImage_iff_ker_le_ker_ρAut
Documentation

The preceding criterion on actual finite étale objects over F.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (F Ω : Type u) [Field F] [Field Ω] [Algebra F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
variable {X : Scheme.{u}} [IsIntegral X]
  (j : Spec (.of F) ⟶ X)
Lean source · statement
theorem fieldSourcePullback_obj_essImage_iff_ker_le_ker_ρAut [IsNormalIntegral X]
    [IsPreimmersion j] [IsDominant j] [QuasiCompact j]
    (W : FiniteEtale (Spec (.of F))) :
    (pullback j).essImage W ↔
      (fieldSourceAbsoluteGaloisHom F Ω j).toMonoidHom.ker ≤
        (Action.ρAut (((equivContAction F Ω).functor.obj W).obj)).ker
def

finiteSubfieldCover

L104 ↗
AlgebraicGeometry.FiniteEtale.finiteSubfieldCover
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (F Ω : Type u) [Field F] [Field Ω] [Algebra F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
variable {X : Scheme.{u}} [IsIntegral X]
  (j : Spec (.of F) ⟶ X)
Lean source · statement
def finiteSubfieldCover (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω]
    [IsSepClosure K Ω] [IsSepClosed Ω]
    (L : IntermediateField K Ω) [FiniteDimensional K L] :
    FiniteEtale (Spec (.of K))
def

subfieldPointEquiv

L117 ↗
AlgebraicGeometry.FiniteEtale.subfieldPointEquiv
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (F Ω : Type u) [Field F] [Field Ω] [Algebra F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
variable {X : Scheme.{u}} [IsIntegral X]
  (j : Spec (.of F) ⟶ X)
Lean source · statement
def subfieldPointEquiv (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω]
    [IsSepClosure K Ω] [IsSepClosed Ω]
    (L : IntermediateField K Ω) [FiniteDimensional K L] :
    (Over.mk (ξ K Ω) ⟶ (finiteSubfieldCover K Ω L).toComma) ≃
      (L →ₐ[K] Ω)
theorem

subfieldPointEquiv_smul

L131 ↗
AlgebraicGeometry.FiniteEtale.subfieldPointEquiv_smul
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (F Ω : Type u) [Field F] [Field Ω] [Algebra F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
variable {X : Scheme.{u}} [IsIntegral X]
  (j : Spec (.of F) ⟶ X)
Lean source · statement
theorem subfieldPointEquiv_smul (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω]
    [IsSepClosure K Ω] [IsSepClosed Ω]
    (L : IntermediateField K Ω) [FiniteDimensional K L]
    (g : Ω ≃ₐ[K] Ω)
    (x : Over.mk (Spec.map (CommRingCat.ofHom (algebraMap K Ω))) ⟶
      (finiteSubfieldCover K Ω L).toComma) :
    subfieldPointEquiv K Ω L (g • x) = g.toAlgHom.comp (subfieldPointEquiv K Ω L x)
theorem

subfieldAction_ker_iff

L146 ↗
AlgebraicGeometry.FiniteEtale.subfieldAction_ker_iff
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (F Ω : Type u) [Field F] [Field Ω] [Algebra F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
variable {X : Scheme.{u}} [IsIntegral X]
  (j : Spec (.of F) ⟶ X)
Lean source · statement
theorem subfieldAction_ker_iff (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω]
    [IsSepClosure K Ω] [IsSepClosed Ω]
    (L : IntermediateField K Ω) [FiniteDimensional K L]
    (g : Ω ≃ₐ[K] Ω) :
    g ∈ (Action.ρAut
      (((equivContAction K Ω).functor.obj
        (finiteSubfieldCover K Ω L)).obj)).ker ↔
      ∀ φ : L →ₐ[K] Ω, g.toAlgHom.comp φ = φ
theorem

fieldSourceSubfieldCover_essImage_iff

L180 ↗
AlgebraicGeometry.FiniteEtale.fieldSourceSubfieldCover_essImage_iff
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (F Ω : Type u) [Field F] [Field Ω] [Algebra F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
variable {X : Scheme.{u}} [IsIntegral X]
  (j : Spec (.of F) ⟶ X)
Lean source · statement
theorem fieldSourceSubfieldCover_essImage_iff [IsNormalIntegral X]
    [IsPreimmersion j] [IsDominant j] [QuasiCompact j]
    (E : IntermediateField F Ω) [FiniteDimensional F E] :
    (pullback j).essImage (finiteSubfieldCover F Ω E) ↔
      (fieldSourceAbsoluteGaloisHom F Ω j).toMonoidHom.ker ≤ E.fixingSubgroup
theorem

fieldSourceKernel_le_fixingSubgroup_iff_exists_finiteEtale_genericFiber

L195 ↗
AlgebraicGeometry.FiniteEtale.fieldSourceKernel_le_fixingSubgroup_iff_exists_finiteEtale_genericFiber
Documentation

A literal finite subfield is fixed by the actual kernel exactly when its spectrum is the actual generic fibre of a finite étale cover of X.

Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
namespace AlgebraicGeometry.FiniteEtale
universe u
variable (F Ω : Type u) [Field F] [Field Ω] [Algebra F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
variable {X : Scheme.{u}} [IsIntegral X]
  (j : Spec (.of F) ⟶ X)
Lean source · statement
theorem fieldSourceKernel_le_fixingSubgroup_iff_exists_finiteEtale_genericFiber
    [IsNormalIntegral X] [IsPreimmersion j] [IsDominant j] [QuasiCompact j]
    (E : IntermediateField F Ω) [FiniteDimensional F E] :
    (fieldSourceAbsoluteGaloisHom F Ω j).toMonoidHom.ker ≤ E.fixingSubgroup ↔
      ∃ (Y : Scheme.{u}) (f : Y ⟶ X), IsFinite f ∧ Etale f ∧
        ∃ e : Limits.pullback f j ≅ Spec (.of E),
          e.hom ≫ Spec.map (CommRingCat.ofHom (algebraMap F E)) =
            Limits.pullback.snd f j

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