NYLL
Module

FiniteKummerSPlaceCardinality.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.FiniteKummerSPlaceCardinality
6 declarations indexed from sourceView source ↗

Module documentation

Cardinal bounds for finite-support Kummer images

Degree-two cohomology of the Kummer coefficient module is annihilated by its exponent. Its localized image embeds in the product of the actual local torsion groups. The proved kernel containment then gives a surjection from that image to the field-unit coefficient image.

Imports8
Imported by2

Declarations

theorem

kummerH2_nsmul_eq_zero

L32 ↗
ClassFieldTower.Martinet.Shafarevich.kummerH2_nsmul_eq_zero
Source context 4 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
Lean source · statement
theorem kummerH2_nsmul_eq_zero
    (G : Type) [Group G] (n : ℕ)
    (x : groupCohomology (Rep.trivial ℤ G (ULift (ZMod n))) 2) : n • x = 0
theorem

range_finite_card_le_of_nsmul

L46 ↗
ClassFieldTower.Martinet.Shafarevich.range_finite_card_le_of_nsmul
Source context 4 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
Lean source · statement
theorem range_finite_card_le_of_nsmul
    {A : Type} [AddCommGroup A] {ι : Type} [Fintype ι]
    (B : ι → Type) [∀ i, AddCommGroup (B i)]
    (f : A →+ ∀ i, B i) (n : ℕ) (hA : ∀ x : A, n • x = 0)
    (hFinite : ∀ i, Finite (B i))
    (hCard : ∀ i, Nat.card {x : B i // n • x = 0} ≤ n) :
    Finite f.range ∧ Nat.card f.range ≤ n ^ Fintype.card ι
theorem

range_finite_card_le_of_ker_le

L73 ↗
ClassFieldTower.Martinet.Shafarevich.range_finite_card_le_of_ker_le
Source context 4 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
Lean source · statement
theorem range_finite_card_le_of_ker_le
    {A B C : Type} [AddCommGroup A] [AddCommGroup B] [AddCommGroup C]
    (f : A →+ B) (g : A →+ C) (hker : f.ker ≤ g.ker) [Finite f.range] :
    Finite g.range ∧ Nat.card g.range ≤ Nat.card f.range
instance

finiteKummerSPlaceCardinalityTensorAction

L94 ↗
ClassFieldTower.Martinet.Shafarevich.finiteKummerSPlaceCardinalityTensorAction
Source context 8 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CyclicCohomology
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
instance finiteKummerSPlaceCardinalityTensorAction
    (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ
theorem

finiteKummerSPlaceH2Localization_range_finite_natCard_le

L101 ↗
ClassFieldTower.Martinet.Shafarevich.finiteKummerSPlaceH2Localization_range_finite_natCard_le
Documentation

The actual localized Kummer image lies in the product of the local n-torsion groups, so it is finite with at most n ^ S.card elements.

Source context 9 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CyclicCohomology
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance finiteKummerSPlaceCardinalityTensorAction
    (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.adicCompletion K)
Lean source · statement
theorem finiteKummerSPlaceH2Localization_range_finite_natCard_le
    (S : Finset (HeightOneSpectrum (𝓞 K))) (n : ℕ+) [Fact (n : ℕ).Prime]
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hP : IsPGroup (n : ℕ) Gal(L/K)) :
    Finite (finiteKummerSPlaceH2Localization K L S n hmu).range ∧
      Nat.card (finiteKummerSPlaceH2Localization K L S n hmu).range ≤
        (n : ℕ) ^ S.card
theorem

finiteKummerCoefficientH2Map_range_finite_natCard_le_of_unramified_outside

L123 ↗
ClassFieldTower.Martinet.Shafarevich.finiteKummerCoefficientH2Map_range_finite_natCard_le_of_unramified_outside
Documentation

The field-unit Kummer image is a quotient of the localized image under the proved kernel containment, and obeys the same finite bound.

Source context 9 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open CyclicCohomology
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance finiteKummerSPlaceCardinalityTensorAction
    (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.adicCompletion K)
Lean source · statement
theorem finiteKummerCoefficientH2Map_range_finite_natCard_le_of_unramified_outside
    (S : Finset (HeightOneSpectrum (𝓞 K))) (n : ℕ+) [Fact (n : ℕ).Prime]
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hP : IsPGroup (n : ℕ) Gal(L/K))
    (hfin : ∀ v : HeightOneSpectrum (𝓞 K), v ∉ S →
      ChosenFinitePlaceIsUnramified (K := K) (L := L) v)
    (hinf : ∀ v : InfinitePlace K, (chosenInfinitePlaceAbove (L := L) v).IsUnramified K) :
    Finite (finiteKummerCoefficientH2Map K L n hmu).hom.toAddMonoidHom.range ∧
      Nat.card (finiteKummerCoefficientH2Map K L n hmu).hom.toAddMonoidHom.range ≤
        (n : ℕ) ^ S.card

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