Yamaguchi26AbfaithfulGalois.inverse_relativeH1Action_ne_one_of_moved_abelianModPower
A moved mod-prime abelianization class gives a nontrivial action on H¹. The inverse appears because the cohomology action uses inverse pullback.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups.Abelian ClassFieldTower.ProP
universe uLean source · statement
theorem inverse_relativeH1Action_ne_one_of_moved_abelianModPower
(K L : Type u) [Field K] [Field L] [Algebra K L] [CharZero L]
(p : ℕ) [Fact p.Prime] (τ : Gal(L/K))
(z : abelianModPower Gal(AlgebraicClosure L/L) p)
(hz : relativeGaloisAbelianModPowerTransform K L p τ z ≠ z) :
relativeGaloisH1Action (n := p) K L τ⁻¹ ≠ 1