NYLL
Module

DivisorialPointedQuotientEndpoint.lean

Nyll.EtaleFundamentalGroups.Inertia.DivisorialPointedQuotientEndpoint
7 declarations indexed from sourceView source ↗

Module documentation

Divisorial pointed quotient endpoint

The actual pointed quotient of the finite field cover along the inertia fixed field agrees with the canonical unconjugated divisorial quotient after transporting the deck group back to the finite Galois group. Its transported range is ideal inertia, so primewise coprimality forces that inertia to vanish.

Imports7
Imported by2

Declarations

theorem

localizedNormalizationInertiaFieldPointedQuotientOfMorphism_eq_canonicalUnconjugated

L55 ↗
EtaleFundamentalGroups.Inertia.localizedNormalizationInertiaFieldPointedQuotientOfMorphism_eq_canonicalUnconjugated
Documentation

The actual pointed quotient along the inertia-field spectrum is the canonical divisorial fundamental-group quotient before its explicit comparison conjugation.

Source context 17 commands

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

noncomputable section
universe uA u
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
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 "IField" =>
  localizedNormalizationInertiaField (K := K) (L := L) P Q
local notation "Omega" => SeparableClosure L
Lean source · statement
theorem localizedNormalizationInertiaFieldPointedQuotientOfMorphism_eq_canonicalUnconjugated :
    (EtaleFundamentalGroups.fieldGaloisToFiniteEtaleAutOpMulEquiv K L).symm.toMonoidHom.comp
        (localizedNormalizationInertiaFieldPointedQuotientHom (K := K) (L := L) P Q) =
      localizedNormalizationInertiaFieldCanonicalUnconjugatedHom
        (K := K) (L := L) P Q
theorem

localizedNormalizationInertiaFieldPointedQuotientOfMorphism_range_map

L81 ↗
EtaleFundamentalGroups.Inertia.localizedNormalizationInertiaFieldPointedQuotientOfMorphism_range_map
Documentation

After transporting the actual pointed quotient through the field/deck equivalence and the explicit comparison conjugation, its image is exactly normalization-prime ideal inertia.

Source context 17 commands

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

noncomputable section
universe uA u
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
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 "IField" =>
  localizedNormalizationInertiaField (K := K) (L := L) P Q
local notation "Omega" => SeparableClosure L
Lean source · full declaration
theorem localizedNormalizationInertiaFieldPointedQuotientOfMorphism_range_map :
    let actualQuotient :=
      localizedNormalizationInertiaFieldPointedQuotientHom (K := K) (L := L) P Q
    let E := EtaleFundamentalGroups.fieldGaloisToFiniteEtaleAutOpMulEquiv K L
    let c := localizedNormalizationInertiaFieldCanonicalConjugatingElement
      (K := K) (L := L) P Q
    (actualQuotient.range.map E.symm.toMonoidHom).map
        (MulAut.conj c).toMonoidHom =
      localizedNormalizationInertia (K := K) (L := L) P Q := by
  intro actualQuotient E c
  have hcomp :
      E.symm.toMonoidHom.comp actualQuotient =
        localizedNormalizationInertiaFieldCanonicalUnconjugatedHom
          (K := K) (L := L) P Q :=
    localizedNormalizationInertiaFieldPointedQuotientOfMorphism_eq_canonicalUnconjugated
      (K := K) (L := L) P Q
  have hrange :
      (localizedNormalizationInertiaFieldCanonicalUnconjugatedHom
          (K := K) (L := L) P Q).range.map
            (MulAut.conj c).toMonoidHom =
        localizedNormalizationInertia (K := K) (L := L) P Q :=
    localizedNormalizationInertiaFieldCanonicalUnconjugatedHom_range_map
      (K := K) (L := L) P Q
  calc
    (actualQuotient.range.map E.symm.toMonoidHom).map
          (MulAut.conj c).toMonoidHom =
        (E.symm.toMonoidHom.comp actualQuotient).range.map
          (MulAut.conj c).toMonoidHom := by
      rw [MonoidHom.range_comp]
    _ = (localizedNormalizationInertiaFieldCanonicalUnconjugatedHom
          (K := K) (L := L) P Q).range.map
            (MulAut.conj c).toMonoidHom := by
      rw [hcomp]
    _ = localizedNormalizationInertia (K := K) (L := L) P Q := hrange
instance

pointedComparison_fieldCoverIsGalois

L118 ↗
EtaleFundamentalGroups.Inertia.pointedComparison_fieldCoverIsGalois
Source context 18 commands

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

noncomputable section
universe uA u
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
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 "IField" =>
  localizedNormalizationInertiaField (K := K) (L := L) P Q
local notation "Omega" => SeparableClosure L
local notation "FieldCover" => FiniteEtale.mk (ξ K L)
Lean source · statement
instance pointedComparison_fieldCoverIsGalois : IsGalois FieldCover
instance

pointedComparison_fieldCoverIsConnected

L121 ↗
EtaleFundamentalGroups.Inertia.pointedComparison_fieldCoverIsConnected
Source context 19 commands

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

noncomputable section
universe uA u
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
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 "IField" =>
  localizedNormalizationInertiaField (K := K) (L := L) P Q
local notation "Omega" => SeparableClosure L
local notation "FieldCover" => FiniteEtale.mk (ξ K L)
local instance pointedComparison_fieldCoverIsGalois : IsGalois FieldCover :=
  EtaleFundamentalGroups.fieldFiniteEtaleCover_isGalois K L
Lean source · statement
instance pointedComparison_fieldCoverIsConnected : IsConnected FieldCover
instance

pointedComparison_fieldCoverAutFinite

L124 ↗
EtaleFundamentalGroups.Inertia.pointedComparison_fieldCoverAutFinite
Source context 20 commands

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

noncomputable section
universe uA u
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
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 "IField" =>
  localizedNormalizationInertiaField (K := K) (L := L) P Q
local notation "Omega" => SeparableClosure L
local notation "FieldCover" => FiniteEtale.mk (ξ K L)
local instance pointedComparison_fieldCoverIsGalois : IsGalois FieldCover :=
  EtaleFundamentalGroups.fieldFiniteEtaleCover_isGalois K L
local instance pointedComparison_fieldCoverIsConnected : IsConnected FieldCover :=
  inferInstance
Lean source · statement
instance pointedComparison_fieldCoverAutFinite : Finite (Aut FieldCover)
instance

pointedComparison_fieldCoverAutOpFinite

L127 ↗
EtaleFundamentalGroups.Inertia.pointedComparison_fieldCoverAutOpFinite
Source context 21 commands

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

noncomputable section
universe uA u
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
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 "IField" =>
  localizedNormalizationInertiaField (K := K) (L := L) P Q
local notation "Omega" => SeparableClosure L
local notation "FieldCover" => FiniteEtale.mk (ξ K L)
local instance pointedComparison_fieldCoverIsGalois : IsGalois FieldCover :=
  EtaleFundamentalGroups.fieldFiniteEtaleCover_isGalois K L
local instance pointedComparison_fieldCoverIsConnected : IsConnected FieldCover :=
  inferInstance
local instance pointedComparison_fieldCoverAutFinite : Finite (Aut FieldCover) :=
  inferInstance
Lean source · statement
instance pointedComparison_fieldCoverAutOpFinite :
    Finite ((Aut FieldCover)ᵐᵒᵖ)
theorem

localizedNormalizationInertia_eq_bot_of_pointedQuotient_coprime_every_prime

L133 ↗
EtaleFundamentalGroups.Inertia.localizedNormalizationInertia_eq_bot_of_pointedQuotient_coprime_every_prime
Documentation

If the same actual pointed inertia image has cardinality prime to every rational prime, then normalization-prime ideal inertia is trivial.

Source context 22 commands

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

noncomputable section
universe uA u
open CategoryTheory AlgebraicGeometry
open CategoryTheory.PreGaloisCategory
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 "IField" =>
  localizedNormalizationInertiaField (K := K) (L := L) P Q
local notation "Omega" => SeparableClosure L
local notation "FieldCover" => FiniteEtale.mk (ξ K L)
local instance pointedComparison_fieldCoverIsGalois : IsGalois FieldCover :=
  EtaleFundamentalGroups.fieldFiniteEtaleCover_isGalois K L
local instance pointedComparison_fieldCoverIsConnected : IsConnected FieldCover :=
  inferInstance
local instance pointedComparison_fieldCoverAutFinite : Finite (Aut FieldCover) :=
  inferInstance
local instance pointedComparison_fieldCoverAutOpFinite :
    Finite ((Aut FieldCover)ᵐᵒᵖ) :=
  Finite.of_injective MulOpposite.unop MulOpposite.unop_injective
Lean source · full declaration
theorem localizedNormalizationInertia_eq_bot_of_pointedQuotient_coprime_every_prime :
    let actualQuotient :=
      localizedNormalizationInertiaFieldPointedQuotientHom (K := K) (L := L) P Q
    (∀ p : ℕ, p.Prime → Nat.Coprime (Nat.card actualQuotient.range) p) →
      localizedNormalizationInertia (K := K) (L := L) P Q = ⊥ := by
  intro actualQuotient hCoprime
  let E := EtaleFundamentalGroups.fieldGaloisToFiniteEtaleAutOpMulEquiv K L
  let c := localizedNormalizationInertiaFieldCanonicalConjugatingElement
    (K := K) (L := L) P Q
  have hrange :
      (actualQuotient.range.map E.symm.toMonoidHom).map
          (MulAut.conj c).toMonoidHom =
        localizedNormalizationInertia (K := K) (L := L) P Q :=
    localizedNormalizationInertiaFieldPointedQuotientOfMorphism_range_map
      (K := K) (L := L) P Q
  have hq : actualQuotient.range = ⊥ :=
    ProCGroups.Boundary.subgroup_eq_bot_of_card_coprime_every_prime
      actualQuotient.range hCoprime
  rw [hq] at hrange
  simpa only [Subgroup.map_bot] using hrange.symm

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