NYLL
Module

ArithmeticStageH2GoverningObstruction.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageH2GoverningObstruction
13 declarations indexed from sourceView source ↗

Module documentation

Arithmetic-stage central obstructions and the governing field

The kernel of a finite arithmetic-stage degree-two embedding problem is the lifted ZMod p coefficient. Consequently, an actual character of the cyclotomic ideal radical valued in that central kernel determines a unique automorphism of the ideal-radical governing field. The conversion is injective and detects a nontrivial obstruction character.

This file only performs that canonical algebraic conversion. It does not assert that an arbitrary degree-two class supplies such a radical character; constructing that character from local splittings and global reciprocity is the remaining arithmetic duality step.

Imports2
Imported by1

Declarations

instance

(anonymous instance)

L37 ↗
Source context 7 commands

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

open scoped NumberField IsMulCommutative Topology
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open KummerTheory ProCGroups ProCGroups.ProC
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out)
theorem

arithmeticStageH2Projection_right_eq_one

L42 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2Projection_right_eq_one
Source context 8 commands

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

open scoped NumberField IsMulCommutative Topology
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open KummerTheory ProCGroups ProCGroups.ProC
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
theorem arithmeticStageH2Projection_right_eq_one
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (x : (arithmeticStageH2Projection F p hpOdd U xU).ker) :
    x.1.right = 1
def

arithmeticStageH2ProjectionKernelEquivCoefficient

L59 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2ProjectionKernelEquivCoefficient
Documentation

The kernel of the arithmetic-stage projection is canonically the coefficient group of the chosen degree-two cocycle extension.

Source context 8 commands

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

open scoped NumberField IsMulCommutative Topology
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open KummerTheory ProCGroups ProCGroups.ProC
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · full declaration
def arithmeticStageH2ProjectionKernelEquivCoefficient
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2) :
    (arithmeticStageH2Projection F p hpOdd U xU).ker ≃*
      Multiplicative (FreeProPH2Cocycle.A p) where
  toFun x := x.1.left
  invFun a := ⟨⟨a, 1⟩, by
    change
      openNormalQuotientContinuousEquivArithmeticStageGalois F p hpOdd U 1 = 1
    exact map_one _⟩
  left_inv x := by
    apply Subtype.ext
    apply H2CocycleExtension.ext
    · rfl
    · exact (arithmeticStageH2Projection_right_eq_one F p hpOdd U xU x).symm
  right_inv _ := rfl
  map_mul' x y := by
    change x.1.left + y.1.left +
        FreeProPH2Cocycle.normalizedCocycle
          (degreeTwoCocycleRepresentative xU) x.1.right y.1.right =
      x.1.left + y.1.left
    rw [arithmeticStageH2Projection_right_eq_one F p hpOdd U xU x,
      arithmeticStageH2Projection_right_eq_one F p hpOdd U xU y,
      FreeProPH2Cocycle.normalizedCocycle_one_left]
    simp
abbrev

ArithmeticStageH2RadicalObstructionCharacter

L91 ↗
ClassFieldTower.Martinet.Shafarevich.ArithmeticStageH2RadicalObstructionCharacter
Documentation

A stage obstruction character is a radical character valued in the central coefficient kernel of the arithmetic-stage embedding problem.

Source context 8 commands

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

open scoped NumberField IsMulCommutative Topology
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open KummerTheory ProCGroups ProCGroups.ProC
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
abbrev ArithmeticStageH2RadicalObstructionCharacter
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
def

liftedCoefficientMulEquivZMod

L101 ↗
ClassFieldTower.Martinet.Shafarevich.liftedCoefficientMulEquivZMod
Source context 8 commands

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

open scoped NumberField IsMulCommutative Topology
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open KummerTheory ProCGroups ProCGroups.ProC
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
def liftedCoefficientMulEquivZMod :
    Multiplicative (FreeProPH2Cocycle.A p) ≃*
      Multiplicative (ZMod p)
theorem

governingFieldPrimitiveRootsNonempty

L107 ↗
ClassFieldTower.Martinet.Shafarevich.governingFieldPrimitiveRootsNonempty
Source context 8 commands

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

open scoped NumberField IsMulCommutative Topology
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open KummerTheory ProCGroups ProCGroups.ProC
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
theorem governingFieldPrimitiveRootsNonempty :
    (primitiveRoots p (IdealRadicalGoverningField F p Fact.out)).Nonempty
def

arithmeticStageH2RadicalObstructionCharacterZMod

L119 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2RadicalObstructionCharacterZMod
Documentation

Coefficient coordinates of a central-kernel-valued obstruction character.

Source context 8 commands

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

open scoped NumberField IsMulCommutative Topology
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open KummerTheory ProCGroups ProCGroups.ProC
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
def arithmeticStageH2RadicalObstructionCharacterZMod
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (chi : ArithmeticStageH2RadicalObstructionCharacter F p hpOdd U xU) :
    IdealRadicalCyclotomicRestrictedQuotient F p →*
      Multiplicative (ZMod p)
theorem

arithmeticStageH2RadicalObstructionCharacterZMod_apply

L134 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2RadicalObstructionCharacterZMod_apply
Source context 8 commands

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

open scoped NumberField IsMulCommutative Topology
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open KummerTheory ProCGroups ProCGroups.ProC
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
theorem arithmeticStageH2RadicalObstructionCharacterZMod_apply
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (chi : ArithmeticStageH2RadicalObstructionCharacter F p hpOdd U xU)
    (q : IdealRadicalCyclotomicRestrictedQuotient F p) :
    arithmeticStageH2RadicalObstructionCharacterZMod
        F p hpOdd U xU chi q =
      liftedCoefficientMulEquivZMod p
        (arithmeticStageH2ProjectionKernelEquivCoefficient
          F p hpOdd U xU (chi q))
def

arithmeticStageH2ObstructionGoverningAutomorphism

L152 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2ObstructionGoverningAutomorphism
Documentation

A kernel-valued obstruction character determines the unique governing automorphism with the same Kummer character.

Source context 8 commands

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

open scoped NumberField IsMulCommutative Topology
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open KummerTheory ProCGroups ProCGroups.ProC
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
def arithmeticStageH2ObstructionGoverningAutomorphism
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (chi : ArithmeticStageH2RadicalObstructionCharacter F p hpOdd U xU) :
    IdealRadicalGoverningGalois F p
theorem

idealRadicalGoverningFieldPairingZMod_obstructionGoverning_apply

L179 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningFieldPairingZMod_obstructionGoverning_apply
Documentation

The governing automorphism has exactly the coefficient character with which the stage obstruction started.

Source context 8 commands

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

open scoped NumberField IsMulCommutative Topology
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open KummerTheory ProCGroups ProCGroups.ProC
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
theorem idealRadicalGoverningFieldPairingZMod_obstructionGoverning_apply
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    (chi : ArithmeticStageH2RadicalObstructionCharacter F p hpOdd U xU)
    (q : IdealRadicalCyclotomicRestrictedQuotient F p) :
    idealRadicalGoverningFieldPairingZMod F p
        (arithmeticStageH2ObstructionGoverningAutomorphism
          F p hpOdd U xU chi) q =
      arithmeticStageH2RadicalObstructionCharacterZMod
        F p hpOdd U xU chi q
theorem

arithmeticStageH2ObstructionGoverningAutomorphism_injective

L217 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2ObstructionGoverningAutomorphism_injective
Documentation

Passing from a central-kernel obstruction character to its governing automorphism loses no information.

Source context 8 commands

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

open scoped NumberField IsMulCommutative Topology
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open KummerTheory ProCGroups ProCGroups.ProC
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
theorem arithmeticStageH2ObstructionGoverningAutomorphism_injective
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2) :
    Function.Injective
      (arithmeticStageH2ObstructionGoverningAutomorphism F p hpOdd U xU)
theorem

arithmeticStageH2ObstructionGoverningAutomorphism_one

L238 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2ObstructionGoverningAutomorphism_one
Source context 8 commands

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

open scoped NumberField IsMulCommutative Topology
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open KummerTheory ProCGroups ProCGroups.ProC
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
theorem arithmeticStageH2ObstructionGoverningAutomorphism_one
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2) :
    arithmeticStageH2ObstructionGoverningAutomorphism F p hpOdd U xU 1 = 1
theorem

arithmeticStageH2ObstructionGoverningAutomorphism_ne_one

L256 ↗
ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2ObstructionGoverningAutomorphism_ne_one
Documentation

A nontrivial central-kernel obstruction character produces a nontrivial governing automorphism.

Source context 8 commands

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

open scoped NumberField IsMulCommutative Topology
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open KummerTheory ProCGroups ProCGroups.ProC
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
theorem arithmeticStageH2ObstructionGoverningAutomorphism_ne_one
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup
      (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (xU : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
        (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
    {chi : ArithmeticStageH2RadicalObstructionCharacter F p hpOdd U xU}
    (hchi : chi ≠ 1) :
    arithmeticStageH2ObstructionGoverningAutomorphism
      F p hpOdd U xU chi ≠ 1

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