NYLL
Module

CyclotomicAbsoluteH2Restriction.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.CyclotomicAbsoluteH2Restriction
6 declarations indexed from sourceView source ↗

Module documentation

Detecting absolute H² after adjoining the p-th roots of unity

The named cyclotomic base has degree strictly below p. Its fixing subgroup in the absolute Galois group is therefore open of index prime to p, and continuous degree-two restriction is injective by the proved transfer argument. This applies to the absolute Galois group, not to an open subgroup of the maximal unramified pro-p quotient.

Imports4
Imported by2

Declarations

instance

cyclotomicAbsoluteFiniteDimensional

L31 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicAbsoluteFiniteDimensional
Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance cyclotomicAbsoluteFiniteDimensional :
    FiniteDimensional F (IdealRadicalCyclotomicBase F p Fact.out)
theorem

idealRadicalCyclotomicBase_finrank_lt

L36 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicBase_finrank_lt
Documentation

The concrete named cyclotomic base has degree strictly less than p.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance cyclotomicAbsoluteFiniteDimensional :
    FiniteDimensional F (IdealRadicalCyclotomicBase F p Fact.out) :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
Lean source · statement
theorem idealRadicalCyclotomicBase_finrank_lt :
    Module.finrank F (IdealRadicalCyclotomicBase F p Fact.out) < p
def

idealRadicalCyclotomicOpenSubgroup

L48 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicOpenSubgroup
Documentation

The actual absolute-Galois subgroup fixing the named cyclotomic base.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance cyclotomicAbsoluteFiniteDimensional :
    FiniteDimensional F (IdealRadicalCyclotomicBase F p Fact.out) :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
Lean source · full declaration
def idealRadicalCyclotomicOpenSubgroup : OpenSubgroup (Field.absoluteGaloisGroup F) where
  toSubgroup := (IdealRadicalCyclotomicBase F p Fact.out).fixingSubgroup
  isOpen' := (IdealRadicalCyclotomicBase F p Fact.out).fixingSubgroup_isOpen
theorem

idealRadicalCyclotomicOpenSubgroup_index

L53 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicOpenSubgroup_index
Documentation

The index of the fixing subgroup is the actual cyclotomic field degree.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance cyclotomicAbsoluteFiniteDimensional :
    FiniteDimensional F (IdealRadicalCyclotomicBase F p Fact.out) :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
Lean source · statement
theorem idealRadicalCyclotomicOpenSubgroup_index :
    (idealRadicalCyclotomicOpenSubgroup F p).toSubgroup.index =
      Module.finrank F (IdealRadicalCyclotomicBase F p Fact.out)
theorem

idealRadicalCyclotomicOpenSubgroup_index_not_dvd

L61 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicOpenSubgroup_index_not_dvd
Documentation

The cyclotomic fixing subgroup has index prime to p.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance cyclotomicAbsoluteFiniteDimensional :
    FiniteDimensional F (IdealRadicalCyclotomicBase F p Fact.out) :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
Lean source · statement
theorem idealRadicalCyclotomicOpenSubgroup_index_not_dvd :
    ¬ p ∣ (idealRadicalCyclotomicOpenSubgroup F p).toSubgroup.index
theorem

cyclotomicAbsoluteH2Restriction_injective

L71 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicAbsoluteH2Restriction_injective
Documentation

Restriction of absolute trivial-coefficient H² to the cyclotomic fixing subgroup is injective. Thus an actual primitive after cyclotomic base change detects vanishing of the original absolute class.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance cyclotomicAbsoluteFiniteDimensional :
    FiniteDimensional F (IdealRadicalCyclotomicBase F p Fact.out) :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
Lean source · statement
theorem cyclotomicAbsoluteH2Restriction_injective :
    Function.Injective (ClassFieldTower.Cohomology.continuousCohomologyZModPMapLifted p
      (ClassFieldTower.Cohomology.subgroupInclusion
        (idealRadicalCyclotomicOpenSubgroup F p).toSubgroup) 2).hom

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