Module

DescendedCharacterAction.lean

Nyll.GaloisCohomology.Kummer.Concrete.DescendedCharacterAction

2 declarations indexed from sourceView source ↗

Module documentation

The action on a descended character

An invariant character of a finite normal intermediate field descends across a coprime degree. If the lower automorphism acts trivially on H¹, every lift to that intermediate field fixes this character. The proof constructs one ambient lift and uses its actual compatibility with both fields.

Imports5

Imported by3

theorem

invariant_of_semilinear_extension

L32 ↗

KummerTheory.invariant_of_semilinear_extension

Documentation

Restriction along the same ambient lift transfers invariance of an actual extension character to its character on the intermediate field.

Source context 3 commands

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

namespace KummerTheory
variable {K Ω : Type*} [Field K] [Field Ω]
  [Algebra K Ω] [IsAlgClosure K Ω]
  (E : IntermediateField K Ω) [FiniteDimensional K E]
attribute [local instance] closureOverIntermediate

Lean source · statement

theorem invariant_of_semilinear_extension
    {A : Type*} [CommGroup A] [TopologicalSpace A] [T1Space A]
    (f : Gal(AlgebraicClosure E/E) →ₜ* A) (ψ : Gal(Ω/K) →ₜ* A)
    (hψ : ∀ σ : E.fixingSubgroup, ψ (σ : Gal(Ω/K)) =
      f (absoluteGaloisClosureEquiv E Ω (fixingSubgroupContinuousEquiv E σ)))
    (τ : K ≃+* K) (υ : E ≃+* E) (a : Ω ≃+* Ω)
    (haK : ∀ x : K, a (algebraMap K Ω x) = algebraMap K Ω (τ x))
    (haE : ∀ x : E, a (algebraMap E Ω x) = algebraMap E Ω (υ x))
    (hψinv : ∀ ρ : Gal(Ω/K), ψ (semilinearGaloisConjugate τ a haK ρ) = ψ ρ)
    (σ : Gal(AlgebraicClosure E/E)) : f (absoluteGaloisConjugate υ σ) = f σ

theorem

absoluteCharacter_invariant_of_trivial_lowerH1Action

L64 ↗

KummerTheory.absoluteCharacter_invariant_of_trivial_lowerH1Action