NYLL
Module

DivisorialQuotientCanonicalFundamentalGroup.lean

Nyll.EtaleFundamentalGroups.Inertia.DivisorialQuotientCanonicalFundamentalGroup
6 declarations indexed from sourceView source ↗

Module documentation

Divisorial inertia from the canonical field fundamental-group map

The finite quotient attached to the inertia fixed field factors through the usual fundamental-group map of spectra after transporting the equality of the two base points. The comparison of fiber functors contributes one explicit inner conjugation and no additional hypothesis.

Imports2
Imported by4

Declarations

def

localizedNormalizationInertiaFieldCanonicalUnconjugatedHom

L47 ↗
EtaleFundamentalGroups.Inertia.localizedNormalizationInertiaFieldCanonicalUnconjugatedHom
Documentation

The finite quotient obtained directly from the canonical fundamental-group map, with only the equality of the two geometric base points transported.

Source context 16 commands

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

noncomputable section
universe uA u
open CategoryTheory
namespace EtaleFundamentalGroups.Inertia
open AlgebraicGeometry.FiniteEtale
variable {A : Type uA} {K L : Type u}
variable [CommRing A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
section
variable (P : Ideal A) [P.IsPrime]
variable (Q : Ideal (integralClosure A L))
local notation "F" =>
  localizedNormalizationInertiaField (K := K) (L := L) P Q
local notation "Omega" => SeparableClosure L
Lean source · full declaration
def
    localizedNormalizationInertiaFieldCanonicalUnconjugatedHom :
    let : CommRing F := (inferInstance : Field F).toCommRing
    let : CommSemiring F := (inferInstance : Field F).toSemifield.toCommSemiring
    let : CommRing Omega := (inferInstance : Field Omega).toCommRing
    let : CommSemiring Omega := (inferInstance : Field Omega).toSemifield.toCommSemiring
    let : Algebra F Omega :=
      ((algebraMap L Omega).comp (algebraMap F L)).toAlgebra
    Aut (fib F Omega) →* Gal(L/K) := by
  intro hFCommRing hFCommSemiring hOmegaCommRing hOmegaCommSemiring hFOmega
  let hKOmega : Algebra K Omega :=
    ((algebraMap L Omega).comp (algebraMap K L)).toAlgebra
  let : @IsScalarTower K F Omega
      (@Algebra.toSMul K F _ _ inferInstance)
      (@Algebra.toSMul F Omega _ _ inferInstance)
      (@Algebra.toSMul K Omega _ _ inferInstance) :=
    IsScalarTower.of_algebraMap_eq' (R := K) (S := F) (A := Omega) rfl
  let : IsScalarTower K L Omega := IsScalarTower.of_algebraMap_eq' rfl
  let : IsSepClosure K Omega := by
    exact ⟨IsSepClosure.sep_closed L, Algebra.IsSeparable.trans K L Omega⟩
  exact fieldCanonicalUnconjugatedHom K F L Omega
def

localizedNormalizationInertiaFieldCanonicalConjugatingElement

L71 ↗
EtaleFundamentalGroups.Inertia.localizedNormalizationInertiaFieldCanonicalConjugatingElement
Documentation

The image in the finite Galois group of the explicit comparison automorphism between the two field-fiber comparisons.

Source context 16 commands

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

noncomputable section
universe uA u
open CategoryTheory
namespace EtaleFundamentalGroups.Inertia
open AlgebraicGeometry.FiniteEtale
variable {A : Type uA} {K L : Type u}
variable [CommRing A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
section
variable (P : Ideal A) [P.IsPrime]
variable (Q : Ideal (integralClosure A L))
local notation "F" =>
  localizedNormalizationInertiaField (K := K) (L := L) P Q
local notation "Omega" => SeparableClosure L
Lean source · statement
def
    localizedNormalizationInertiaFieldCanonicalConjugatingElement :
    Gal(L/K)
def

localizedNormalizationInertiaFieldCanonicalHom

L91 ↗
EtaleFundamentalGroups.Inertia.localizedNormalizationInertiaFieldCanonicalHom
Documentation

The canonical quotient with the explicit comparison conjugation included.

Source context 16 commands

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

noncomputable section
universe uA u
open CategoryTheory
namespace EtaleFundamentalGroups.Inertia
open AlgebraicGeometry.FiniteEtale
variable {A : Type uA} {K L : Type u}
variable [CommRing A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
section
variable (P : Ideal A) [P.IsPrime]
variable (Q : Ideal (integralClosure A L))
local notation "F" =>
  localizedNormalizationInertiaField (K := K) (L := L) P Q
local notation "Omega" => SeparableClosure L
Lean source · full declaration
def localizedNormalizationInertiaFieldCanonicalHom
    :
    let : CommRing F := (inferInstance : Field F).toCommRing
    let : CommSemiring F := (inferInstance : Field F).toSemifield.toCommSemiring
    let : CommRing Omega := (inferInstance : Field Omega).toCommRing
    let : CommSemiring Omega := (inferInstance : Field Omega).toSemifield.toCommSemiring
    let : Algebra F Omega :=
      ((algebraMap L Omega).comp (algebraMap F L)).toAlgebra
    Aut (fib F Omega) →* Gal(L/K) := by
  intro hFCommRing hFCommSemiring hOmegaCommRing hOmegaCommSemiring hFOmega
  exact (MulAut.conj
      (localizedNormalizationInertiaFieldCanonicalConjugatingElement
        (K := K) (L := L) P Q)).toMonoidHom.comp
    (localizedNormalizationInertiaFieldCanonicalUnconjugatedHom
      (K := K) (L := L) P Q)
theorem

localizedNormalizationInertiaFieldFundamentalGroupHom_eq_canonical

L109 ↗
EtaleFundamentalGroups.Inertia.localizedNormalizationInertiaFieldFundamentalGroupHom_eq_canonical
Documentation

The inertia fixed-field quotient is exactly the canonical fundamental-group quotient with its explicit inner conjugation.

Source context 16 commands

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

noncomputable section
universe uA u
open CategoryTheory
namespace EtaleFundamentalGroups.Inertia
open AlgebraicGeometry.FiniteEtale
variable {A : Type uA} {K L : Type u}
variable [CommRing A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
section
variable (P : Ideal A) [P.IsPrime]
variable (Q : Ideal (integralClosure A L))
local notation "F" =>
  localizedNormalizationInertiaField (K := K) (L := L) P Q
local notation "Omega" => SeparableClosure L
Lean source · statement
theorem localizedNormalizationInertiaFieldFundamentalGroupHom_eq_canonical
    :
    localizedNormalizationInertiaFieldFundamentalGroupHom
        (K := K) (L := L) P Q =
      localizedNormalizationInertiaFieldCanonicalHom
        (K := K) (L := L) P Q
theorem

localizedNormalizationInertiaFieldCanonicalHom_range

L157 ↗
EtaleFundamentalGroups.Inertia.localizedNormalizationInertiaFieldCanonicalHom_range
Documentation

The corrected canonical quotient has image exactly ideal inertia.

Source context 16 commands

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

noncomputable section
universe uA u
open CategoryTheory
namespace EtaleFundamentalGroups.Inertia
open AlgebraicGeometry.FiniteEtale
variable {A : Type uA} {K L : Type u}
variable [CommRing A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
section
variable (P : Ideal A) [P.IsPrime]
variable (Q : Ideal (integralClosure A L))
local notation "F" =>
  localizedNormalizationInertiaField (K := K) (L := L) P Q
local notation "Omega" => SeparableClosure L
Lean source · statement
theorem localizedNormalizationInertiaFieldCanonicalHom_range
    :
    (localizedNormalizationInertiaFieldCanonicalHom
      (K := K) (L := L) P Q).range =
        localizedNormalizationInertia (K := K) (L := L) P Q
theorem

localizedNormalizationInertiaFieldCanonicalUnconjugatedHom_range_map

L167 ↗
EtaleFundamentalGroups.Inertia.localizedNormalizationInertiaFieldCanonicalUnconjugatedHom_range_map
Documentation

Conjugating the image of the uncorrected canonical composite by the explicit finite comparison element gives exactly ideal inertia.

Source context 16 commands

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

noncomputable section
universe uA u
open CategoryTheory
namespace EtaleFundamentalGroups.Inertia
open AlgebraicGeometry.FiniteEtale
variable {A : Type uA} {K L : Type u}
variable [CommRing A]
variable [Field K] [Field L]
variable [Algebra A K] [IsFractionRing A K]
variable [Algebra K L] [Algebra A L] [IsScalarTower A K L]
variable [FiniteDimensional K L] [_root_.IsGalois K L]
section
variable (P : Ideal A) [P.IsPrime]
variable (Q : Ideal (integralClosure A L))
local notation "F" =>
  localizedNormalizationInertiaField (K := K) (L := L) P Q
local notation "Omega" => SeparableClosure L
Lean source · statement
theorem localizedNormalizationInertiaFieldCanonicalUnconjugatedHom_range_map
    :
    (localizedNormalizationInertiaFieldCanonicalUnconjugatedHom
        (K := K) (L := L) P Q).range.map
      (MulAut.conj
        (localizedNormalizationInertiaFieldCanonicalConjugatingElement
          (K := K) (L := L) P Q)).toMonoidHom =
      localizedNormalizationInertia (K := K) (L := L) P Q

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