Module

FiniteExtensionAbsoluteH2Restriction.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.FiniteExtensionAbsoluteH2Restriction

4 declarations indexed from sourceView source ↗

Module documentation

Absolute H² restriction along actual finite-field embeddings

The existing finite-extension identification realizes the absolute Galois group of the top field as its open fixing subgroup in the bottom absolute Galois group. Transporting prime-to-index restriction along this actual continuous equivalence proves injectivity for the field-embedding map, including the named cyclotomic extension.

Imports2

Imported by2

theorem

finiteExtensionAbsoluteH2Restriction_injective

L36 ↗

ClassFieldTower.Martinet.Shafarevich.finiteExtensionAbsoluteH2Restriction_injective

Documentation

Restriction along a concrete embedded finite extension of degree prime to p is injective on continuous absolute H² with trivial coefficients.

Source context 8 commands

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

open CategoryTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP
open RamificationTheory.Field.absoluteGaloisGroup
universe u
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem finiteExtensionAbsoluteH2Restriction_injective
    (L : Type u) [Field L] [Algebra F L] [FiniteDimensional F L]
    (i : L →ₐ[F] AlgebraicClosure F)
    (hdegree : ¬ p ∣ Module.finrank F L) :
    Function.Injective (continuousCohomologyZModPMapLifted p
      (ofFiniteExtensionAbsoluteContinuous F i) 2).hom

instance

finiteExtensionCyclotomicFiniteDimensional

L65 ↗

ClassFieldTower.Martinet.Shafarevich.finiteExtensionCyclotomicFiniteDimensional

Source context 8 commands

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

open CategoryTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP
open RamificationTheory.Field.absoluteGaloisGroup
universe u
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

instance finiteExtensionCyclotomicFiniteDimensional :
    FiniteDimensional F (IdealRadicalCyclotomicBase F p Fact.out)

def

cyclotomicAbsoluteGaloisInclusion

L71 ↗

ClassFieldTower.Martinet.Shafarevich.cyclotomicAbsoluteGaloisInclusion

Documentation

The concrete continuous map from the absolute Galois group of the named cyclotomic field to that of the base field.

Source context 9 commands

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

open CategoryTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP
open RamificationTheory.Field.absoluteGaloisGroup
universe u
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finiteExtensionCyclotomicFiniteDimensional :
    FiniteDimensional F (IdealRadicalCyclotomicBase F p Fact.out) :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out

Lean source · statement

def cyclotomicAbsoluteGaloisInclusion :
    Field.absoluteGaloisGroup (IdealRadicalCyclotomicBase F p Fact.out) →ₜ*
      Field.absoluteGaloisGroup F

theorem

cyclotomicFieldAbsoluteH2Restriction_injective

L78 ↗

ClassFieldTower.Martinet.Shafarevich.cyclotomicFieldAbsoluteH2Restriction_injective

Documentation

The actual field-extension restriction, rather than only its subgroup-valued form, detects absolute degree-two vanishing.

Source context 9 commands

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

open CategoryTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.ProP
open RamificationTheory.Field.absoluteGaloisGroup
universe u
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finiteExtensionCyclotomicFiniteDimensional :
    FiniteDimensional F (IdealRadicalCyclotomicBase F p Fact.out) :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out

Lean source · statement

theorem cyclotomicFieldAbsoluteH2Restriction_injective :
    Function.Injective (continuousCohomologyZModPMapLifted p
      (cyclotomicAbsoluteGaloisInclusion F p) 2).hom

Module documentation

Absolute H² restriction along actual finite-field embeddings

Declarations

finiteExtensionAbsoluteH2Restriction_injective

finiteExtensionCyclotomicFiniteDimensional

cyclotomicAbsoluteGaloisInclusion

cyclotomicFieldAbsoluteH2Restriction_injective