SeparableAbsoluteKummerNaturality.lean

theorem separableKummer_naturality
    (n : ℕ+) [NeZero ((n : ℕ) : K)]
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (τ : K ≃+* K) (a : Kˣ) (σ : Gal(SeparableClosure K/K)) :
    ((separableKummerContinuousNthRootsCharacterEquiv K n hmu
        ((Units.map τ.toMonoidHom a : Kˣ) :
          Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)
        (semilinearGaloisConjugate τ (separableClosureEquivOfEquiv τ)
          (separableClosureEquivOfEquiv_algebraMap τ) σ) :
      DiscreteNthRootsSubgroup (SeparableClosure K) (n : ℕ)) :
        (SeparableClosure K)ˣ) =
      Units.map (separableClosureEquivOfEquiv τ).toMonoidHom
        ((separableKummerContinuousNthRootsCharacterEquiv K n hmu
            (a : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) σ :
          DiscreteNthRootsSubgroup (SeparableClosure K) (n : ℕ)) :
            (SeparableClosure K)ˣ)

theorem separableAbsoluteKummerContinuousZModCharacterEquiv_naturality_of_pow_roots
    (n : ℕ+) [NeZero ((n : ℕ) : K)]
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (τ : K ≃+* K) (m : ℕ)
    (hτ : ∀ ξ : K, ξ ^ (n : ℕ) = 1 → τ ξ = ξ ^ m)
    (a : Kˣ) (σ : Field.absoluteGaloisGroup K) :
    separableAbsoluteKummerContinuousZModCharacterEquiv K n hmu
        ((Units.map τ.toMonoidHom a : Kˣ) :
          Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)
        (absoluteGaloisConjugate τ σ) =
      separableAbsoluteKummerContinuousZModCharacterEquiv K n hmu
        (a : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) σ ^ m

theorem separableAbsoluteKummerContinuousZModCharacterEquiv_naturality_of_fixes_roots
    (n : ℕ+) [NeZero ((n : ℕ) : K)]
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (τ : K ≃+* K)
    (hτ : ∀ ξ : K, ξ ^ (n : ℕ) = 1 → τ ξ = ξ)
    (a : Kˣ) (σ : Field.absoluteGaloisGroup K) :
    separableAbsoluteKummerContinuousZModCharacterEquiv K n hmu
        ((Units.map τ.toMonoidHom a : Kˣ) :
          Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)
        (absoluteGaloisConjugate τ σ) =
      separableAbsoluteKummerContinuousZModCharacterEquiv K n hmu
        (a : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) σ