The character action with trivial coefficients gives the additive action on H¹. Restriction along relative Galois automorphisms gives the action for an extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ClassFieldTower.ProP
variable {K : Type*} [Field K] (n : ℕ)instance discreteZModTopology : TopologicalSpace (ZMod n)Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ClassFieldTower.ProP
variable {K : Type*} [Field K] (n : ℕ)
local instance discreteZModTopology : TopologicalSpace (ZMod n) := ⊥instance discreteZMod : DiscreteTopology (ZMod n)Pullback of continuous degree-one classes by inverse Galois conjugation.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ClassFieldTower.ProP
variable {K : Type*} [Field K] (n : ℕ)
local instance discreteZModTopology : TopologicalSpace (ZMod n) := ⊥
local instance discreteZMod : DiscreteTopology (ZMod n) := discreteTopology_bot _def absoluteH1Transform (τ : RingAut K)
(c : ContinuousH1ZMod (p := n) (G := Field.absoluteGaloisGroup K)) :
ContinuousH1ZMod (p := n) (G := Field.absoluteGaloisGroup K)Evaluation of the degree-one transform on an absolute Galois element.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ClassFieldTower.ProP
variable {K : Type*} [Field K] (n : ℕ)
local instance discreteZModTopology : TopologicalSpace (ZMod n) := ⊥
local instance discreteZMod : DiscreteTopology (ZMod n) := discreteTopology_bot _theorem absoluteH1Transform_apply (τ : RingAut K)
(c : ContinuousH1ZMod (p := n) (G := Field.absoluteGaloisGroup K))
(σ : Gal(AlgebraicClosure K/K)) :
absoluteH1Transform n τ c (Additive.ofMul (σ : Field.absoluteGaloisGroup K)) =
c (Additive.ofMul
(absoluteGaloisConjugate τ.symm σ : Field.absoluteGaloisGroup K))The identity automorphism fixes every continuous degree-one class.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ClassFieldTower.ProP
variable {K : Type*} [Field K] (n : ℕ)
local instance discreteZModTopology : TopologicalSpace (ZMod n) := ⊥
local instance discreteZMod : DiscreteTopology (ZMod n) := discreteTopology_bot _theorem absoluteH1Transform_one
(c : ContinuousH1ZMod (p := n) (G := Field.absoluteGaloisGroup K)) :
absoluteH1Transform n 1 c = cDegree-one transforms satisfy the left action law.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ClassFieldTower.ProP
variable {K : Type*} [Field K] (n : ℕ)
local instance discreteZModTopology : TopologicalSpace (ZMod n) := ⊥
local instance discreteZMod : DiscreteTopology (ZMod n) := discreteTopology_bot _theorem absoluteH1Transform_mul (τ υ : RingAut K)
(c : ContinuousH1ZMod (p := n) (G := Field.absoluteGaloisGroup K)) :
absoluteH1Transform n (τ * υ) c =
absoluteH1Transform n τ (absoluteH1Transform n υ c)Automorphisms of the field act additively on its continuous degree-one classes.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ClassFieldTower.ProP
variable {K : Type*} [Field K] (n : ℕ)
local instance discreteZModTopology : TopologicalSpace (ZMod n) := ⊥
local instance discreteZMod : DiscreteTopology (ZMod n) := discreteTopology_bot _def absoluteH1Action :
RingAut K →* Multiplicative
(AddAut (ContinuousH1ZMod (p := n) (G := Field.absoluteGaloisGroup K))) where
toFun τ :=
Multiplicative.ofAdd
{ toFun := absoluteH1Transform n τ
invFun := absoluteH1Transform n τ⁻¹
left_inv c := by
rw [← absoluteH1Transform_mul, inv_mul_cancel, absoluteH1Transform_one]
right_inv c := by
rw [← absoluteH1Transform_mul, mul_inv_cancel, absoluteH1Transform_one]
map_add' c d := by
apply ContinuousAddMonoidHom.ext
intro σ
rfl }
map_one' := by
apply AddEquiv.ext
intro c
exact absoluteH1Transform_one n c
map_mul' τ υ := by
apply AddEquiv.ext
intro c
exact absoluteH1Transform_mul n τ υ cThe relative Galois group acts on the continuous absolute H¹ of the extension.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ClassFieldTower.ProP
variable {K : Type*} [Field K] (n : ℕ)
local instance discreteZModTopology : TopologicalSpace (ZMod n) := ⊥
local instance discreteZMod : DiscreteTopology (ZMod n) := discreteTopology_bot _
variable (K) (L : Type*) [Field L] [Algebra K L]def relativeGaloisH1Action :
Gal(L/K) →* Multiplicative
(AddAut (ContinuousH1ZMod (p := n) (G := Field.absoluteGaloisGroup L)))The relative action is pullback by inverse conjugation in the closure.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace KummerTheory
open ClassFieldTower.ProP
variable {K : Type*} [Field K] (n : ℕ)
local instance discreteZModTopology : TopologicalSpace (ZMod n) := ⊥
local instance discreteZMod : DiscreteTopology (ZMod n) := discreteTopology_bot _
variable (K) (L : Type*) [Field L] [Algebra K L]theorem relativeGaloisH1Action_apply (τ : Gal(L/K))
(c : ContinuousH1ZMod (p := n) (G := Field.absoluteGaloisGroup L))
(σ : Gal(AlgebraicClosure L/L)) :
(relativeGaloisH1Action (n := n) K L τ).toAdd c
(Additive.ofMul (σ : Field.absoluteGaloisGroup L)) =
c (Additive.ofMul
(absoluteGaloisConjugate τ.toRingEquiv.symm σ : Field.absoluteGaloisGroup L))