Module

FiniteKummerCyclicCarryInflation.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.FiniteKummerCyclicCarryInflation

10 declarations indexed from sourceView source ↗

Module documentation

Inflation and naturality of finite cyclic carry cocycles

Generator-fixed coefficients in a representation define positive cyclic carry cocycles after restriction along a group homomorphism. Mapping coefficients commutes with inflation and the degree-two cohomology map; the unit representation and intermediate-field unit inclusion give the Kummer cases.

Imports2

Imported by2

abbrev

FiniteCyclicCarryCoefficient

L32 ↗

ClassFieldTower.Martinet.Shafarevich.FiniteCyclicCarryCoefficient

Documentation

Coefficients fixed by the selected generator, packaged in the exact module structure carried by a representation.

Source context 6 commands

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

open CategoryTheory
open RamificationTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
universe u

Lean source · statement

abbrev FiniteCyclicCarryCoefficient
    {R G : Type u} [CommRing R] [CommGroup G]
    (A : Rep R G) (g : G)

def

inflatedFiniteCyclicCarryTwoCocycleOfRep

L39 ↗

ClassFieldTower.Martinet.Shafarevich.inflatedFiniteCyclicCarryTwoCocycleOfRep

Documentation

The positive cyclic carry cocycle pulled back along a group homomorphism, with coefficients in an arbitrary target representation.

Source context 6 commands

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

open CategoryTheory
open RamificationTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
universe u

Lean source · statement

def inflatedFiniteCyclicCarryTwoCocycleOfRep
    {R G Q : Type u} [CommRing R] [CommGroup G] [Fintype G] [Group Q]
    (B : Rep R Q) (q : Q →* G)
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (b : B) (hb : ∀ x : Q, B.ρ x b = b) :
    groupCohomology.cocycles₂ B

theorem

inflatedFiniteCyclicCarryTwoCocycleOfRep_apply

L57 ↗

ClassFieldTower.Martinet.Shafarevich.inflatedFiniteCyclicCarryTwoCocycleOfRep_apply

Source context 6 commands

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

open CategoryTheory
open RamificationTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
universe u

Lean source · statement

theorem inflatedFiniteCyclicCarryTwoCocycleOfRep_apply
    {R G Q : Type u} [CommRing R] [CommGroup G] [Fintype G] [Group Q]
    (B : Rep R Q) (q : Q →* G)
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (b : B) (hb : ∀ x : Q, B.ρ x b = b)
    (x y : Q) :
    inflatedFiniteCyclicCarryTwoCocycleOfRep B q g hg b hb (x, y) =
      finiteCyclicCarry g hg (q x) (q y) • b

theorem

mapCocycles₂_finiteCyclicCarryTwoCocycle

L70 ↗

ClassFieldTower.Martinet.Shafarevich.mapCocycles₂_finiteCyclicCarryTwoCocycle

Documentation

Mapping a cyclic carry cocycle maps its fixed coefficient and otherwise leaves the pulled-back positive carry factor set unchanged.

Source context 6 commands

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

open CategoryTheory
open RamificationTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
universe u

Lean source · statement

theorem mapCocycles₂_finiteCyclicCarryTwoCocycle
    {R G Q : Type u} [CommRing R] [CommGroup G] [Fintype G] [Group Q]
    (A : Rep R G) (B : Rep R Q) (q : Q →* G)
    (f : Rep.res q A ⟶ B)
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : FiniteCyclicCarryCoefficient A g)
    (b : B) (hb : ∀ x : Q, B.ρ x b = b)
    (hab : f.hom a.1 = b) :
    groupCohomology.mapCocycles₂ q f
        (finiteCyclicCarryTwoCocycle A g hg a) =
      inflatedFiniteCyclicCarryTwoCocycleOfRep B q g hg b hb

theorem

finiteCyclicCarryCoefficient_map_fixed

L91 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicCarryCoefficient_map_fixed

Documentation

The image of a generator-fixed coefficient is fixed after restriction along the cyclic quotient.

Source context 6 commands

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

open CategoryTheory
open RamificationTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
universe u

Lean source · statement

theorem finiteCyclicCarryCoefficient_map_fixed
    {R G Q : Type u} [CommRing R] [CommGroup G] [Group Q]
    (A : Rep R G) (B : Rep R Q) (q : Q →* G)
    (f : Rep.res q A ⟶ B)
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : FiniteCyclicCarryCoefficient A g)
    (x : Q) :
    B.ρ x (f.hom a.1) = f.hom a.1

theorem

map_H2pi_finiteCyclicCarryTwoCocycle

L109 ↗

ClassFieldTower.Martinet.Shafarevich.map_H2pi_finiteCyclicCarryTwoCocycle

Documentation

Degree-two naturality for a cyclic carry factor set.

Source context 6 commands

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

open CategoryTheory
open RamificationTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
universe u

Lean source · statement

theorem map_H2pi_finiteCyclicCarryTwoCocycle
    {R G Q : Type u} [CommRing R] [CommGroup G] [Fintype G] [Group Q]
    (A : Rep R G) (B : Rep R Q) (q : Q →* G)
    (f : Rep.res q A ⟶ B)
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : FiniteCyclicCarryCoefficient A g)
    (b : B) (hb : ∀ x : Q, B.ρ x b = b)
    (hab : f.hom a.1 = b) :
    groupCohomology.map q f 2
        (groupCohomology.H2π A (finiteCyclicCarryTwoCocycle A g hg a)) =
      groupCohomology.H2π B
        (inflatedFiniteCyclicCarryTwoCocycleOfRep B q g hg b hb)

theorem

inflatedFiniteCyclicCarryTwoCocycleOfRep_units_eq

L133 ↗

ClassFieldTower.Martinet.Shafarevich.inflatedFiniteCyclicCarryTwoCocycleOfRep_units_eq

Documentation

The arbitrary-representation pullback specializes definitionally to the unit-representation carry cocycle used by the Kummer factor-set bridge.

Source context 6 commands

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

open CategoryTheory
open RamificationTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
universe u

Lean source · statement

theorem inflatedFiniteCyclicCarryTwoCocycleOfRep_units_eq
    (K M : Type) [Field K] [Field M] [Algebra K M]
    {G : Type} [CommGroup G] [Fintype G]
    (q : Gal(M/K) →* G)
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (b : Rep.ofAlgebraAutOnUnits K M)
    (hb : ∀ x : Gal(M / K),
      (Rep.ofAlgebraAutOnUnits K M).ρ x b = b) :
    inflatedFiniteCyclicCarryTwoCocycleOfRep
        (Rep.ofAlgebraAutOnUnits K M) q g hg b hb =
      inflatedFiniteCyclicCarryTwoCocycle K M q g hg b hb

theorem

map_H2pi_finiteCyclicCarryTwoCocycle_units

L155 ↗

ClassFieldTower.Martinet.Shafarevich.map_H2pi_finiteCyclicCarryTwoCocycle_units

Documentation

Unit-coefficient specialization of cyclic carry naturality.

Source context 6 commands

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

open CategoryTheory
open RamificationTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
universe u

Lean source · statement

theorem map_H2pi_finiteCyclicCarryTwoCocycle_units
    (K M : Type) [Field K] [Field M] [Algebra K M]
    {G : Type} [CommGroup G] [Fintype G]
    (A : Rep ℤ G) (q : Gal(M/K) →* G)
    (f : Rep.res q A ⟶ Rep.ofAlgebraAutOnUnits K M)
    (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (a : FiniteCyclicCarryCoefficient A g)
    (b : Rep.ofAlgebraAutOnUnits K M)
    (hb : ∀ x : Gal(M / K),
      (Rep.ofAlgebraAutOnUnits K M).ρ x b = b)
    (hab : f.hom a.1 = b) :
    groupCohomology.map q f 2
        (groupCohomology.H2π A (finiteCyclicCarryTwoCocycle A g hg a)) =
      groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K M)
        (inflatedFiniteCyclicCarryTwoCocycle K M q g hg b hb)

theorem

intermediateFieldUnitsRepHom_apply

L180 ↗

ClassFieldTower.Martinet.Shafarevich.intermediateFieldUnitsRepHom_apply

Source context 8 commands

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

open CategoryTheory
open RamificationTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
universe u
section IntermediateFields
variable {K Omega : Type u} [Field K] [Field Omega] [Algebra K Omega]

Lean source · statement

theorem intermediateFieldUnitsRepHom_apply
    (E F : IntermediateField K Omega) (hEF : E ≤ F)
    [Normal K E] (x : Additive Eˣ) :
    (intermediateFieldUnitsRepHom E F hEF).hom x =
      Additive.ofMul
        (Units.map (IntermediateField.inclusion hEF).toRingHom.toMonoidHom
          (Additive.toMul x))

theorem

intermediateFieldUnitsRepHom_baseUnit

L191 ↗

ClassFieldTower.Martinet.Shafarevich.intermediateFieldUnitsRepHom_baseUnit

Documentation

Intermediate-field unit inclusion carries a base-field unit to the same base-field unit in the larger intermediate field.

Source context 8 commands

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

open CategoryTheory
open RamificationTheory
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
universe u
section IntermediateFields
variable {K Omega : Type u} [Field K] [Field Omega] [Algebra K Omega]

Lean source · statement

theorem intermediateFieldUnitsRepHom_baseUnit
    (E F : IntermediateField K Omega) (hEF : E ≤ F)
    [Normal K E] (a : Kˣ) :
    (intermediateFieldUnitsRepHom E F hEF).hom
        (Additive.ofMul (Units.map (algebraMap K E).toMonoidHom a)) =
      Additive.ofMul (Units.map (algebraMap K F).toMonoidHom a)

Module documentation

Inflation and naturality of finite cyclic carry cocycles

Declarations