ClassFieldTower.Martinet.Shafarevich.finiteKummerCup_H2pi_eq_map_finiteCyclicCarry
Arbitrary-pair cyclic descent: once the common Kummer stage acts on a chosen root by chi, and its cyclic quotient coordinate is -psi, the coefficient-changed cup class is the pullback of the quotient's positive carry class.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory
open ClassFieldTower.ProP
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.CohomologyLean source · statement
theorem finiteKummerCup_H2pi_eq_map_finiteCyclicCarry
(K M : Type) [Field K] [Field M] [Algebra K M]
(p : ℕ+)
{G : Type} [CommGroup G] [Fintype G]
(hmu : (primitiveRoots (p : ℕ) K).Nonempty)
(chi psi : ContinuousH1ZMod
(p := (p : ℕ)) (G := Gal(M/K)))
(q : Gal(M/K) →* G)
(g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
(hcard : Nat.card G = (p : ℕ))
(hcoord : ∀ sigma : Gal(M / K),
(finiteCyclicGeneratorCoordinate g hg (q sigma)).val =
(-psi (Additive.ofMul sigma)).val)
(A : Rep ℤ G)
(f : Rep.res q A ⟶ Rep.ofAlgebraAutOnUnits K M)
(c : FiniteCyclicCarryCoefficient A g)
(alpha a : Rep.ofAlgebraAutOnUnits K M)
(halpha : ∀ sigma : Gal(M / K),
(Rep.ofAlgebraAutOnUnits K M).ρ sigma alpha =
(finiteKummerCoefficientRepHom K M p hmu).hom
(ULift.up (chi (Additive.ofMul sigma))) + alpha)
(hpow : (p : ℕ) • alpha = a)
(ha : ∀ sigma : Gal(M / K),
(Rep.ofAlgebraAutOnUnits K M).ρ sigma a = a)
(hca : f.hom c.1 = a) :
groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K M)
(finiteKummerCupCoefficientTwoCocycle K M p hmu chi psi) =
groupCohomology.map q f 2
(groupCohomology.H2π A
(finiteCyclicCarryTwoCocycle A g hg c))