Nyll.EtaleFundamentalGroups.Inertia.DivisorialPointedQuotientComparison

theorem

fieldComposite_isSepClosure

EtaleFundamentalGroups.Inertia.fieldComposite_isSepClosure

Source context 5 commands

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

noncomputable section
universe uA u
open CategoryTheory AlgebraicGeometry
namespace EtaleFundamentalGroups.Inertia
open AlgebraicGeometry.FiniteEtale

Lean source · statement

theorem fieldComposite_isSepClosure
    (F E Omega : Type u)
    [Field F] [Field E] [Field Omega]
    [Algebra F E] [Algebra E Omega] [hFOmega : Algebra F Omega]
    [Algebra.IsSeparable F E] [IsSepClosure E Omega]
    (hcomp : algebraMap F Omega =
      (algebraMap E Omega).comp (algebraMap F E)) :
    IsSepClosure F Omega

theorem

fieldFiniteEtaleCoverQuotientHom_eq_restriction

L51 ↗

EtaleFundamentalGroups.Inertia.fieldFiniteEtaleCoverQuotientHom_eq_restriction

Documentation

For the canonical point of the field cover Spec L → Spec K, the categorical pointed quotient is the usual restriction homomorphism from the chosen separable closure.

Source context 7 commands

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

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

Lean source · full declaration

theorem fieldFiniteEtaleCoverQuotientHom_eq_restriction :
    let Omega := SeparableClosure L
    let : CommRing Omega := (inferInstance : Field Omega).toCommRing
    let : CommSemiring Omega := (inferInstance : Field Omega).toSemifield.toCommSemiring
    let : Algebra K Omega :=
      ((algebraMap L Omega).comp (algebraMap K L)).toAlgebra
    let : IsScalarTower K L Omega := IsScalarTower.of_algebraMap_eq' rfl
    let Y := FiniteEtale.mk (ξ K L)
    let hY := EtaleFundamentalGroups.fieldFiniteEtaleCover_isGalois K L
    let : CategoryTheory.PreGaloisCategory.IsGalois Y := hY
    let y := EtaleFundamentalGroups.fieldFiniteEtaleCoverCanonicalPoint K L Omega
    (EtaleFundamentalGroups.fieldGaloisToFiniteEtaleAutOpMulEquiv K L).symm.toMonoidHom.comp
        (EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom
          (ξ K Omega) Y hY y) =
      finiteGaloisSeparableClosureQuotientHom (K := K) (L := L) := by
  intro Omega hOmegaCommRing hOmegaCommSemiring hKOmega hKLOmega Y hY hYGalois y
  let : IsSepClosure K Omega := fieldComposite_isSepClosure K L Omega rfl
  apply MonoidHom.ext
  intro a
  let eK := absoluteGaloisToFiberAutMulEquiv K Omega inferInstance
  let sigma : Gal(Omega/K) := eK.symm a
  have hq := EtaleFundamentalGroups.fieldFiniteEtaleCoverQuotient_apply
    K L Omega sigma
  change
    (EtaleFundamentalGroups.fieldGaloisToFiniteEtaleAutOpMulEquiv K L).symm
        (EtaleFundamentalGroups.finiteEtaleGaloisCoverQuotientMonoidHom
          (ξ K Omega) Y hY y a) =
      AlgEquiv.restrictNormalHom (F := K) (K₁ := Omega) L (eK.symm a)
  simpa only [sigma, eK, MulEquiv.apply_symm_apply] using hq

DivisorialPointedQuotientComparison.lean

Module documentation

Pointed finite-cover realization of divisorial inertia quotients

fieldComposite_isSepClosure

fieldFiniteEtaleCoverQuotientHom_eq_restriction

Module documentation

Pointed finite-cover realization of divisorial inertia quotients

Declarations

fieldComposite_isSepClosure

fieldFiniteEtaleCoverQuotientHom_eq_restriction