NYLL
Module

AbsoluteH1TrivialCharacter.lean

Nyll.GaloisCohomology.Kummer.Concrete.AbsoluteH1TrivialCharacter
2 declarations indexed from sourceView source ↗

Module documentation

Trivial H¹ actions fix continuous characters

Triviality of the relative action on H¹ gives invariance under forward conjugation by applying the inverse automorphism's action. The constructed closure comparison then gives invariance under any actual semilinear lift.

Imports6
Imported by2

Declarations

theorem

absoluteCharacter_conjugation_invariant_of_relativeH1Action_eq_one

L30 ↗
KummerTheory.absoluteCharacter_conjugation_invariant_of_relativeH1Action_eq_one
Documentation

A trivial relative H¹ action fixes every continuous cyclic character under forward absolute Galois conjugation.

Source context 3 commands

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

namespace KummerTheory
open ClassFieldTower.ProP
variable {K L : Type*} [Field K] [Field L] [Algebra K L] {n : ℕ}
Lean source · statement
theorem absoluteCharacter_conjugation_invariant_of_relativeH1Action_eq_one
    (τ : Gal(L/K)) (hτ : relativeGaloisH1Action (n := n) K L τ = 1)
    (f : Gal(AlgebraicClosure L/L) →ₜ* Multiplicative (ZMod n))
    (σ : Gal(AlgebraicClosure L/L)) :
    f (absoluteGaloisConjugate τ.toRingEquiv σ) = f σ
theorem

semilinearCharacter_invariant_of_relativeH1Action_eq_one

L52 ↗
KummerTheory.semilinearCharacter_invariant_of_relativeH1Action_eq_one
Documentation

Triviality of the relative H¹ action also fixes continuous cyclic characters on any actual algebraic closure, for every semilinear lift.

Source context 4 commands

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

namespace KummerTheory
open ClassFieldTower.ProP
variable {K L : Type*} [Field K] [Field L] [Algebra K L] {n : ℕ}
variable {Ω : Type*} [Field Ω] [Algebra L Ω] [IsAlgClosure L Ω]
Lean source · statement
theorem semilinearCharacter_invariant_of_relativeH1Action_eq_one
    (τ : Gal(L/K)) (hτ : relativeGaloisH1Action (n := n) K L τ = 1)
    (a : Ω ≃+* Ω)
    (ha : ∀ l : L, a (algebraMap L Ω l) = algebraMap L Ω (τ l))
    (ψ : Gal(Ω/L) →ₜ* Multiplicative (ZMod n)) (σ : Gal(Ω/L)) :
    ψ (semilinearGaloisConjugate τ.toRingEquiv a ha σ) = ψ σ

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.