NYLL
Module

FieldCoverQuotient.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.FieldCoverQuotient
10 declarations indexed from sourceView source ↗

Module documentation

Pointed finite quotients associated to finite Galois field extensions

A finite Galois extension gives a categorical Galois finite-etale cover of the base field spectrum. This file identifies its deck group and its pointed fiber-functor quotient with the usual restriction homomorphism on Galois groups.

Imports5
Imported by7

Declarations

instance

fieldSpecMap_isFiniteEtale

L38 ↗
EtaleFundamentalGroups.fieldSpecMap_isFiniteEtale
Documentation

A finite-dimensional Galois extension gives a finite-etale morphism of field spectra.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
Lean source · statement
instance fieldSpecMap_isFiniteEtale : IsFiniteEtale (ξ K L)
def

fieldAlgEquivSchemeIso

L46 ↗
EtaleFundamentalGroups.fieldAlgEquivSchemeIso
Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
Lean source · full declaration
def fieldAlgEquivSchemeIso
    (sigma : Gal(L/K)) : Spec (.of L) ≅ Spec (.of L) where
  hom := Spec.map (CommRingCat.ofHom sigma.toRingEquiv.toRingHom)
  inv := Spec.map (CommRingCat.ofHom sigma.symm.toRingEquiv.toRingHom)
  hom_inv_id := by
    rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, ← Spec.map_id]
    rw [Spec.map_injective.eq_iff]
    ext z
    simp
  inv_hom_id := by
    rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, ← Spec.map_id]
    rw [Spec.map_injective.eq_iff]
    ext z
    simp
def

fieldAlgEquivToFiniteEtaleAut

L61 ↗
EtaleFundamentalGroups.fieldAlgEquivToFiniteEtaleAut
Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
Lean source · statement
def fieldAlgEquivToFiniteEtaleAut
    (sigma : Gal(L/K)) : Aut (FiniteEtale.mk (ξ K L))
theorem

fieldAlgEquivToFiniteEtaleAut_injective

L77 ↗
EtaleFundamentalGroups.fieldAlgEquivToFiniteEtaleAut_injective
Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
Lean source · statement
theorem fieldAlgEquivToFiniteEtaleAut_injective :
    Function.Injective (fieldAlgEquivToFiniteEtaleAut K L)
theorem

fieldFiniteEtaleCover_isGalois

L91 ↗
EtaleFundamentalGroups.fieldFiniteEtaleCover_isGalois
Documentation

The finite-etale cover of a field spectrum associated to a finite Galois extension is a categorical Galois object.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
Lean source · statement
theorem fieldFiniteEtaleCover_isGalois :
    IsGalois (FiniteEtale.mk (ξ K L))
def

fieldGaloisToFiniteEtaleAutOpHom

L128 ↗
EtaleFundamentalGroups.fieldGaloisToFiniteEtaleAutOpHom
Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
Lean source · full declaration
def fieldGaloisToFiniteEtaleAutOpHom :
    Gal(L/K) →* (Aut (FiniteEtale.mk (ξ K L)))ᵐᵒᵖ where
  toFun sigma := MulOpposite.op (fieldAlgEquivToFiniteEtaleAut K L sigma)
  map_one' := by
    apply MulOpposite.unop_injective
    apply Aut.ext
    apply MorphismProperty.Over.Hom.ext
    change Spec.map (CommRingCat.ofHom ((1 : Gal(L/K)).toRingHom)) = 𝟙 _
    rw [← Spec.map_id]
    congr 1
  map_mul' sigma tau := by
    apply MulOpposite.unop_injective
    apply Aut.ext
    apply MorphismProperty.Over.Hom.ext
    change Spec.map (CommRingCat.ofHom ((sigma * tau).toRingHom)) =
      (MulOpposite.unop
        (MulOpposite.op (fieldAlgEquivToFiniteEtaleAut K L sigma) *
          MulOpposite.op (fieldAlgEquivToFiniteEtaleAut K L tau))).hom.left
    change Spec.map (CommRingCat.ofHom ((sigma * tau).toRingHom)) =
      Spec.map (CommRingCat.ofHom sigma.toRingHom) ≫
        Spec.map (CommRingCat.ofHom tau.toRingHom)
    rw [← Spec.map_comp, ← CommRingCat.ofHom_comp]
    congr 1
theorem

fieldGaloisToFiniteEtaleAutOpHom_bijective

L152 ↗
EtaleFundamentalGroups.fieldGaloisToFiniteEtaleAutOpHom_bijective
Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
Lean source · statement
theorem fieldGaloisToFiniteEtaleAutOpHom_bijective :
    Function.Bijective (fieldGaloisToFiniteEtaleAutOpHom K L)
def

fieldGaloisToFiniteEtaleAutOpMulEquiv

L188 ↗
EtaleFundamentalGroups.fieldGaloisToFiniteEtaleAutOpMulEquiv
Documentation

The usual Galois group of a finite field extension is canonically the opposite deck-transformation group of the corresponding scheme cover.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
Lean source · statement
def fieldGaloisToFiniteEtaleAutOpMulEquiv :
    Gal(L/K) ≃* (Aut (FiniteEtale.mk (ξ K L)))ᵐᵒᵖ
def

fieldFiniteEtaleCoverCanonicalPoint

L198 ↗
EtaleFundamentalGroups.fieldFiniteEtaleCoverCanonicalPoint
Documentation

The canonical point of the field cover determined by the inclusion L → Omega.

Source context 9 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable (Omega : Type u) [Field Omega] [Algebra K Omega]
  [Algebra L Omega] [IsScalarTower K L Omega] [IsSepClosed Omega]
Lean source · statement
def fieldFiniteEtaleCoverCanonicalPoint :
    (fib K Omega).obj (FiniteEtale.mk (ξ K L))
theorem

fieldFiniteEtaleCoverQuotient_apply

L205 ↗
EtaleFundamentalGroups.fieldFiniteEtaleCoverQuotient_apply
Documentation

Under the canonical deck-group equivalence, the pointed finite-cover quotient is restriction of automorphisms to L.

Source context 9 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry.FiniteEtale
namespace EtaleFundamentalGroups
universe u
variable (K L : Type u) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
variable (Omega : Type u) [Field Omega] [Algebra K Omega]
  [Algebra L Omega] [IsScalarTower K L Omega] [IsSepClosed Omega]
Lean source · full declaration
theorem fieldFiniteEtaleCoverQuotient_apply
    [IsSepClosure K Omega] (sigma : Gal(Omega/K)) :
    let Y : FiniteEtale (Spec (.of K)) := FiniteEtale.mk (ξ K L)
    let hY : IsGalois Y := fieldFiniteEtaleCover_isGalois K L
    letI : IsGalois Y := hY
    let y := fieldFiniteEtaleCoverCanonicalPoint K L Omega
    (fieldGaloisToFiniteEtaleAutOpMulEquiv K L).symm
        (finiteEtaleGaloisCoverQuotientMonoidHom
          (ξ K Omega) Y hY y
          (absoluteGaloisToFiberAutMulEquiv K Omega inferInstance sigma)) =
      AlgEquiv.restrictNormalHom (F := K) (K₁ := Omega) L sigma := by
  let Y : FiniteEtale (Spec (.of K)) := FiniteEtale.mk (ξ K L)
  let hY : IsGalois Y := fieldFiniteEtaleCover_isGalois K L
  let : IsGalois Y := hY
  let y := fieldFiniteEtaleCoverCanonicalPoint K L Omega
  let E := fieldGaloisToFiniteEtaleAutOpMulEquiv K L
  apply E.injective
  rw [E.apply_symm_apply]
  apply MulOpposite.unop_injective
  apply (evaluationEquivOfIsGalois (fib K Omega) Y y).injective
  simp only [evaluationEquivOfIsGalois_apply]
  rw [finiteEtaleGaloisCoverQuotientMonoidHom_evaluation]
  change
    (absoluteGaloisToFiberAutMulEquiv K Omega inferInstance sigma).hom.app Y y =
      (fib K Omega).map
        (fieldAlgEquivToFiniteEtaleAut K L
          (AlgEquiv.restrictNormalHom (F := K) (K₁ := Omega) L sigma)).hom y
  rw [absoluteGaloisToFiberAutMulEquiv,
    CategoryTheory.PreGaloisCategory.toAutMulEquiv_apply,
    CategoryTheory.PreGaloisCategory.toAut_hom_app_apply]
  apply (fiberObjEquivHom (ξ K Omega) Y).injective
  rw [algEquiv_smul_fiber_def, Equiv.apply_symm_apply,
    ← fiberObjEquivHom_naturality]
  dsimp only [y, fieldFiniteEtaleCoverCanonicalPoint]
  rw [Equiv.apply_symm_apply]
  apply CategoryTheory.Over.OverMorphism.ext
  change Spec.map (CommRingCat.ofHom sigma.toRingEquiv.toRingHom) ≫ ξ L Omega =
    ξ L Omega ≫ Spec.map (CommRingCat.ofHom
      (AlgEquiv.restrictNormalHom (F := K) (K₁ := Omega) L sigma).toRingHom)
  rw [← Spec.map_comp, ← Spec.map_comp, ← CommRingCat.ofHom_comp,
    ← CommRingCat.ofHom_comp]
  apply congrArg Spec.map
  ext z
  exact (AlgEquiv.restrictNormal_commutes sigma L z).symm

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