SemilinearConjugation.lean

theorem semilinear_symm_algebraMap (τ : K ≃+* K) (e : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k)) (k : K) :
    e.symm (algebraMap K Ω k) = algebraMap K Ω (τ.symm k)

def semilinearGaloisConjugate (τ : K ≃+* K) (e : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (σ : Gal(Ω/K)) : Gal(Ω/K)

theorem semilinearGaloisConjugate_apply (τ : K ≃+* K) (e : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (σ : Gal(Ω/K)) (x : Ω) :
    semilinearGaloisConjugate τ e he σ x = e (σ (e.symm x))

theorem semilinear_refl_algebraMap (k : K) :
    RingEquiv.refl Ω (algebraMap K Ω k) = algebraMap K Ω (RingEquiv.refl K k)

theorem semilinearGaloisConjugate_refl (σ : Gal(Ω/K)) :
    semilinearGaloisConjugate (RingEquiv.refl K) (RingEquiv.refl Ω)
      (semilinear_refl_algebraMap (K := K) (Ω := Ω)) σ = σ

theorem semilinear_trans_algebraMap (τ υ : K ≃+* K) (e d : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (hd : ∀ k : K, d (algebraMap K Ω k) = algebraMap K Ω (υ k)) (k : K) :
    (e.trans d) (algebraMap K Ω k) = algebraMap K Ω ((τ.trans υ) k)

theorem semilinearGaloisConjugate_trans (τ υ : K ≃+* K) (e d : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (hd : ∀ k : K, d (algebraMap K Ω k) = algebraMap K Ω (υ k))
    (σ : Gal(Ω/K)) :
    semilinearGaloisConjugate (τ.trans υ) (e.trans d)
      (semilinear_trans_algebraMap τ υ e d he hd) σ =
        semilinearGaloisConjugate υ d hd (semilinearGaloisConjugate τ e he σ)

def semilinearGaloisConjugateEquiv (τ : K ≃+* K) (e : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k)) :
    Gal(Ω/K) ≃* Gal(Ω/K) where
  toFun := semilinearGaloisConjugate τ e he
  invFun := semilinearGaloisConjugate τ.symm e.symm
    (semilinear_symm_algebraMap τ e he)
  left_inv σ := by
    apply AlgEquiv.ext
    intro x
    simp only [semilinearGaloisConjugate_apply, RingEquiv.symm_symm,
      RingEquiv.symm_apply_apply]
  right_inv σ := by
    apply AlgEquiv.ext
    intro x
    simp only [semilinearGaloisConjugate_apply, RingEquiv.symm_symm,
      RingEquiv.apply_symm_apply]
  map_mul' σ ρ := by
    apply AlgEquiv.ext
    intro x
    simp only [semilinearGaloisConjugate_apply, AlgEquiv.mul_apply,
      RingEquiv.symm_apply_apply]

theorem semilinearGaloisConjugateEquiv_apply (τ : K ≃+* K) (e : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (σ : Gal(Ω/K)) :
    semilinearGaloisConjugateEquiv τ e he σ = semilinearGaloisConjugate τ e he σ

def semilinearGaloisExtensionDifference (τ : K ≃+* K) (e e' : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (he' : ∀ k : K, e' (algebraMap K Ω k) = algebraMap K Ω (τ k)) :
    Gal(Ω/K)

theorem semilinearGaloisExtensionDifference_apply (τ : K ≃+* K) (e e' : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (he' : ∀ k : K, e' (algebraMap K Ω k) = algebraMap K Ω (τ k)) (x : Ω) :
    semilinearGaloisExtensionDifference τ e e' he he' x = e' (e.symm x)

theorem semilinearGaloisExtensionDifference_inv_apply
    (τ : K ≃+* K) (e e' : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (he' : ∀ k : K, e' (algebraMap K Ω k) = algebraMap K Ω (τ k)) (x : Ω) :
    (semilinearGaloisExtensionDifference τ e e' he he')⁻¹ x = e (e'.symm x)

theorem semilinearGaloisConjugate_eq_inner (τ : K ≃+* K) (e e' : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (he' : ∀ k : K, e' (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (σ : Gal(Ω/K)) :
    semilinearGaloisConjugate τ e' he' σ =
      semilinearGaloisExtensionDifference τ e e' he he' *
        semilinearGaloisConjugate τ e he σ *
          (semilinearGaloisExtensionDifference τ e e' he he')⁻¹

theorem map_semilinearGaloisConjugate_eq {A : Type*} [CommGroup A]
    (f : Gal(Ω/K) →* A) (τ : K ≃+* K) (e e' : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (he' : ∀ k : K, e' (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (σ : Gal(Ω/K)) :
    f (semilinearGaloisConjugate τ e' he' σ) =
      f (semilinearGaloisConjugate τ e he σ)