NYLL
Module

IdeleClassPGroupH1.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.IdeleClassPGroupH1
13 declarations indexed from sourceView source ↗

Module documentation

Degree-one vanishing for actual finite p-extensions of number fields

The rational idele-class formation satisfies the cyclic class-field axiom. The abstract p-group induction therefore gives degree-one vanishing. Here we transport that source theorem to the actual relative idele-class representation of Gal(L/K).

The transport is explicit: relative ideles are sent to absolute ideles, then to the chosen image of L in the rational separable closure. The coefficient equivalence is checked against the actual Galois action before using functoriality of group cohomology.

Instance audit: no global instances are introduced. The relative class action is fixed once locally. The only auxiliary tower setup is the quotient-restriction lemma (four canonical data instances and one normality proof); no setup is repeated in the cohomology transport.

Imports4
Imported by2

Declarations

theorem

adeleCongr_refl_apply

L41 ↗
ClassFieldTower.Martinet.Shafarevich.adeleCongr_refl_apply
Source context 6 commands

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

open CategoryTheory NumberField
open scoped NumberField TensorProduct
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFormation CyclicCohomology
open AlgebraicNumberTheory LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
noncomputable section
Lean source · statement
theorem adeleCongr_refl_apply
    (K : Type) [Field K] [NumberField K]
    (a : NumberField.AdeleRing (𝓞 K) K) :
    adeleCongr (AlgEquiv.refl : K ≃ₐ[ℚ] K) a = a
instance

(anonymous instance)

L57 ↗
Source context 8 commands

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

open CategoryTheory NumberField
open scoped NumberField TensorProduct
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFormation CyclicCohomology
open AlgebraicNumberTheory LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
noncomputable section
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
instance : MulDistribMulAction (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L)
theorem

relativeClassCongr_refl_base_eq_smul

L61 ↗
ClassFieldTower.Martinet.Shafarevich.relativeClassCongr_refl_base_eq_smul
Source context 10 commands

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

open CategoryTheory NumberField
open scoped NumberField TensorProduct
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFormation CyclicCohomology
open AlgebraicNumberTheory LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
noncomputable section
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
local instance : MulDistribMulAction (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L) :=
  RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · full declaration
theorem relativeClassCongr_refl_base_eq_smul
    (sigma : L ≃ₐ[K] L) (c : RelativeIdeleGroup.ClassGroup K L) :
    relativeIdeleClassCongrOfAlgEquiv
      (AlgEquiv.refl : K ≃ₐ[ℚ] K) (sigma.restrictScalars ℚ)
      (fun x => sigma.commutes x) c = sigma • c := by
  let tau : L ≃ₐ[ℚ] L := sigma.restrictScalars ℚ
  have h : ∀ x : K, tau (algebraMap K L x) = algebraMap K L
      ((AlgEquiv.refl : K ≃ₐ[ℚ] K) x) := fun x => sigma.commutes x
  change relativeIdeleClassCongrOfAlgEquiv (AlgEquiv.refl : K ≃ₐ[ℚ] K) tau h c = _
  refine QuotientGroup.induction_on c ?_
  intro a
  change relativeIdeleClassCongrOfAlgEquiv (AlgEquiv.refl : K ≃ₐ[ℚ] K) tau h
      (QuotientGroup.mk' (RelativeIdeleGroup.principalSubgroup K L) a) =
    sigma • (QuotientGroup.mk' (RelativeIdeleGroup.principalSubgroup K L) a)
  rw [relativeIdeleClassCongrOfAlgEquiv_mk, RelativeIdeleGroup.Cohomology.ideleClass_smul_mk]
  congr 1
  apply Units.ext
  change relativeAdeleCongrOfAlgEquiv
    (AlgEquiv.refl : K ≃ₐ[ℚ] K) tau h a =
      RelativeIdeleGroup.conjugation K L sigma a
  induction (a : RelativeAdeleRing K L) using TensorProduct.inductionOn with
  | add x y hx hy => simpa only [map_add] using congrArg₂ (· + ·) hx hy
  | tmul b x =>
      rw [relativeAdeleCongrOfAlgEquiv_tmul
        (AlgEquiv.refl : K ≃ₐ[ℚ] K) tau h b x,
        RelativeIdeleGroup.conjugation_tmul K L sigma b x,
        adeleCongr_refl_apply K b]
      exact congrArg (fun y : L => b ⊗ₜ[K] y)
        (AlgEquiv.restrictScalars_apply (R := ℚ) sigma x)
theorem

relativeIdeleClassBaseChange_smul

L93 ↗
ClassFieldTower.Martinet.Shafarevich.relativeIdeleClassBaseChange_smul
Documentation

Relative-to-absolute idele-class base change intertwines the Galois action.

Source context 10 commands

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

open CategoryTheory NumberField
open scoped NumberField TensorProduct
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFormation CyclicCohomology
open AlgebraicNumberTheory LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
noncomputable section
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
local instance : MulDistribMulAction (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L) :=
  RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
omit [IsGalois K L] in
Lean source · statement
theorem relativeIdeleClassBaseChange_smul
    (sigma : L ≃ₐ[K] L) (c : RelativeIdeleGroup.ClassGroup K L) :
    relativeIdeleClassBaseChangeMulEquiv (K := K) (L := L) (sigma • c) =
      ideleClassCongr (sigma.restrictScalars ℚ)
        (relativeIdeleClassBaseChangeMulEquiv (K := K) (L := L) c)
def

relativeIdeleClassEquivRationalFixed

L105 ↗
ClassFieldTower.Martinet.Shafarevich.relativeIdeleClassEquivRationalFixed
Documentation

Actual relative idele classes are the fixed coefficients in the rational idele-class formation at the chosen copy of the top field.

Source context 9 commands

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

open CategoryTheory NumberField
open scoped NumberField TensorProduct
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFormation CyclicCohomology
open AlgebraicNumberTheory LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
noncomputable section
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
local instance : MulDistribMulAction (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L) :=
  RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
Lean source · statement
def relativeIdeleClassEquivRationalFixed :
    Additive (RelativeIdeleGroup.ClassGroup K L) ≃+
      KummerTheory.ambientFixedAddSubgroup rationalIdeleClassRepresentation
        (numberFieldTowerTopSubgroup L)
theorem

towerQuotientGalois_mk_apply

L114 ↗
ClassFieldTower.Martinet.Shafarevich.towerQuotientGalois_mk_apply
Source context 9 commands

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

open CategoryTheory NumberField
open scoped NumberField TensorProduct
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFormation CyclicCohomology
open AlgebraicNumberTheory LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
noncomputable section
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
local instance : MulDistribMulAction (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L) :=
  RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
Lean source · statement
theorem towerQuotientGalois_mk_apply
    (sigma : (numberFieldTowerBaseSubgroup K L).toSubgroup) (x : L) :
    numberFieldSeparableClosureEmbedding L
        (numberFieldTowerExtensionQuotientEquivGaloisGroup K L
          ((numberFieldTowerFiniteGaloisSubextension K L).extensionQuotientMk sigma) x) =
      sigma.1 (numberFieldSeparableClosureEmbedding L x)
theorem

ideleClassCongr_conjugate

L133 ↗
ClassFieldTower.Martinet.Shafarevich.ideleClassCongr_conjugate
Source context 10 commands

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

open CategoryTheory NumberField
open scoped NumberField TensorProduct
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFormation CyclicCohomology
open AlgebraicNumberTheory LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
noncomputable section
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
local instance : MulDistribMulAction (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L) :=
  RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem ideleClassCongr_conjugate
    {E : Type} [Field E] [NumberField E]
    (e : L ≃ₐ[ℚ] E) (tau : L ≃ₐ[ℚ] L) (c : IdeleClassGroup L) :
    ideleClassCongr ((e.symm.trans tau).trans e) (ideleClassCongr e c) =
      ideleClassCongr e (ideleClassCongr tau c)
theorem

rationalFixed_conjugate_action

L145 ↗
ClassFieldTower.Martinet.Shafarevich.rationalFixed_conjugate_action
Source context 10 commands

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

open CategoryTheory NumberField
open scoped NumberField TensorProduct
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFormation CyclicCohomology
open AlgebraicNumberTheory LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
noncomputable section
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
local instance : MulDistribMulAction (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L) :=
  RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · full declaration
theorem rationalFixed_conjugate_action
    (sigma : Gal(SeparableClosure ℚ/ℚ)) (tau : L ≃ₐ[K] L)
    (h : ∀ y : L, numberFieldSeparableClosureEmbedding L (tau y) =
      sigma (numberFieldSeparableClosureEmbedding L y))
    (c : IdeleClassGroup L) :
    let E := numberFieldInRationalSeparableClosure L
    let e : L ≃ₐ[ℚ] E := (numberFieldSeparableClosureEmbedding L).equivFieldRange
    rationalIdeleClassRepresentation.ρ sigma
        (rationalIdeleClassEquivFixed E (Additive.ofMul (ideleClassCongr e c))).1 =
      (rationalIdeleClassEquivFixed E
        (Additive.ofMul (ideleClassCongr e
          (ideleClassCongr (tau.restrictScalars ℚ) c)))).1 := by
  dsimp only
  let E := numberFieldInRationalSeparableClosure L
  let e : L ≃ₐ[ℚ] E := (numberFieldSeparableClosureEmbedding L).equivFieldRange
  let eta : E ≃ₐ[ℚ] E := (e.symm.trans (tau.restrictScalars ℚ)).trans e
  have hse : ∀ x : E, (eta x).1 = sigma x.1 := by
    intro x
    obtain ⟨y, rfl⟩ := e.surjective x
    change numberFieldSeparableClosureEmbedding L (tau (e.symm (e y))) =
      sigma (numberFieldSeparableClosureEmbedding L y)
    rw [e.symm_apply_apply]
    exact h y
  have hn := rationalIdeleClassEquivFixed_ambientAlgEquiv sigma eta hse
    (ideleClassCongr e c)
  exact hn.trans (congrArg (fun d : IdeleClassGroup E =>
    (rationalIdeleClassEquivFixed E (Additive.ofMul d)).1)
      (ideleClassCongr_conjugate L e (tau.restrictScalars ℚ) c))
theorem

relativeIdeleClassEquivRationalFixed_action_core

L175 ↗
ClassFieldTower.Martinet.Shafarevich.relativeIdeleClassEquivRationalFixed_action_core
Source context 10 commands

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

open CategoryTheory NumberField
open scoped NumberField TensorProduct
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFormation CyclicCohomology
open AlgebraicNumberTheory LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
noncomputable section
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
local instance : MulDistribMulAction (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L) :=
  RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
omit [IsGalois K L] in
Lean source · statement
theorem relativeIdeleClassEquivRationalFixed_action_core
    (sigma : Gal(SeparableClosure ℚ/ℚ)) (tau : L ≃ₐ[K] L)
    (h : ∀ y : L, numberFieldSeparableClosureEmbedding L (tau y) =
      sigma (numberFieldSeparableClosureEmbedding L y))
    (c : RelativeIdeleGroup.ClassGroup K L) :
    rationalIdeleClassRepresentation.ρ sigma
        (relativeIdeleClassEquivRationalFixed K L (Additive.ofMul c)).1 =
      (relativeIdeleClassEquivRationalFixed K L
        (Additive.ofMul (tau • c))).1
theorem

relativeIdeleClassEquivRationalFixed_action

L199 ↗
ClassFieldTower.Martinet.Shafarevich.relativeIdeleClassEquivRationalFixed_action
Documentation

The fixed-coefficient equivalence respects restriction from the actual ambient Galois group to the finite extension quotient.

Source context 9 commands

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

open CategoryTheory NumberField
open scoped NumberField TensorProduct
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFormation CyclicCohomology
open AlgebraicNumberTheory LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
noncomputable section
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
local instance : MulDistribMulAction (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L) :=
  RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
Lean source · statement
theorem relativeIdeleClassEquivRationalFixed_action
    (sigma : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (c : RelativeIdeleGroup.ClassGroup K L) :
    rationalIdeleClassRepresentation.ρ sigma.1
        (relativeIdeleClassEquivRationalFixed K L (Additive.ofMul c)).1 =
      (relativeIdeleClassEquivRationalFixed K L
        (Additive.ofMul
          (numberFieldTowerExtensionQuotientEquivGaloisGroup K L
            ((numberFieldTowerFiniteGaloisSubextension K L).extensionQuotientMk sigma) • c))).1
def

relativeIdeleClassFixedRepresentationEquiv

L215 ↗
ClassFieldTower.Martinet.Shafarevich.relativeIdeleClassFixedRepresentationEquiv
Documentation

Coefficient equivalence with the representation descended to the finite abstract extension quotient.

Source context 9 commands

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

open CategoryTheory NumberField
open scoped NumberField TensorProduct
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFormation CyclicCohomology
open AlgebraicNumberTheory LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
noncomputable section
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
local instance : MulDistribMulAction (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L) :=
  RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
Lean source · statement
def relativeIdeleClassFixedRepresentationEquiv :
    Additive (RelativeIdeleGroup.ClassGroup K L) ≃+
      (extensionFixedRepresentation rationalIdeleClassRepresentation
        (numberFieldTowerFiniteAbstractField K L).field
        (numberFieldTowerFiniteGaloisSubextension K L).field
        (numberFieldTowerFiniteGaloisSubextension K L).below
        (numberFieldTowerFiniteGaloisSubextension K L).normal).V
theorem

relativeIdeleClassFixedRepresentationEquiv_action

L231 ↗
ClassFieldTower.Martinet.Shafarevich.relativeIdeleClassFixedRepresentationEquiv_action
Documentation

The coefficient equivalence is equivariant for the concrete identification of the abstract extension quotient with Gal(L/K).

Source context 9 commands

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

open CategoryTheory NumberField
open scoped NumberField TensorProduct
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFormation CyclicCohomology
open AlgebraicNumberTheory LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
noncomputable section
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
local instance : MulDistribMulAction (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L) :=
  RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
Lean source · statement
theorem relativeIdeleClassFixedRepresentationEquiv_action
    (q : (numberFieldTowerFiniteGaloisSubextension K L).extensionQuotient)
    (c : Additive (RelativeIdeleGroup.ClassGroup K L)) :
    (extensionFixedRepresentation rationalIdeleClassRepresentation
      (numberFieldTowerFiniteAbstractField K L).field
      (numberFieldTowerFiniteGaloisSubextension K L).field
      (numberFieldTowerFiniteGaloisSubextension K L).below
      (numberFieldTowerFiniteGaloisSubextension K L).normal).ρ q
        (relativeIdeleClassFixedRepresentationEquiv K L c) =
      relativeIdeleClassFixedRepresentationEquiv K L
        ((Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
          (RelativeIdeleGroup.ClassGroup K L)).ρ
          (numberFieldTowerExtensionQuotientEquivGaloisGroup K L q) c)
theorem

ideleClassH1_subsingleton_of_isPGroup

L251 ↗
ClassFieldTower.Martinet.Shafarevich.ideleClassH1_subsingleton_of_isPGroup
Documentation

The actual relative idele-class representation has vanishing H¹ for every finite Galois p-extension of number fields. The only arithmetic input is the existing rational idele-class class-field axiom.

Source context 9 commands

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

open CategoryTheory NumberField
open scoped NumberField TensorProduct
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFormation CyclicCohomology
open AlgebraicNumberTheory LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
noncomputable section
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
local instance : MulDistribMulAction (L ≃ₐ[K] L) (RelativeIdeleGroup.ClassGroup K L) :=
  RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction K L
Lean source · statement
theorem ideleClassH1_subsingleton_of_isPGroup
    {p : ℕ} [Fact p.Prime] (hP : IsPGroup p (L ≃ₐ[K] L)) :
    Subsingleton (groupCohomology.H1
      (Rep.ofMulDistribMulAction (L ≃ₐ[K] L)
        (RelativeIdeleGroup.ClassGroup K L)))

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