AbsoluteContinuousCharacterAction.lean

def absoluteContinuousCharacterTransform (τ : RingAut K)
    (f : Gal(AlgebraicClosure K/K) →ₜ* A) : Gal(AlgebraicClosure K/K) →ₜ* A

theorem absoluteContinuousCharacterTransform_apply (τ : RingAut K)
    (f : Gal(AlgebraicClosure K/K) →ₜ* A) (σ : Gal(AlgebraicClosure K/K)) :
    absoluteContinuousCharacterTransform τ f σ =
      f (absoluteGaloisConjugate τ.symm σ)

theorem absoluteContinuousCharacterTransform_one
    (f : Gal(AlgebraicClosure K/K) →ₜ* A) :
    absoluteContinuousCharacterTransform 1 f = f

theorem absoluteContinuousCharacterTransform_mul (τ υ : RingAut K)
    (f : Gal(AlgebraicClosure K/K) →ₜ* A) :
    absoluteContinuousCharacterTransform (τ * υ) f =
      absoluteContinuousCharacterTransform τ (absoluteContinuousCharacterTransform υ f)

def absoluteContinuousCharacterAction :
    RingAut K →* MulAut (Gal(AlgebraicClosure K/K) →ₜ* A) where
  toFun τ :=
    { toFun := absoluteContinuousCharacterTransform τ
      invFun := absoluteContinuousCharacterTransform τ⁻¹
      left_inv f := by
        rw [← absoluteContinuousCharacterTransform_mul, inv_mul_cancel,
          absoluteContinuousCharacterTransform_one]
      right_inv f := by
        rw [← absoluteContinuousCharacterTransform_mul, mul_inv_cancel,
          absoluteContinuousCharacterTransform_one]
      map_mul' f g := by
        apply ContinuousMonoidHom.ext
        intro σ
        rfl }
  map_one' := by
    apply MulEquiv.ext
    intro f
    exact absoluteContinuousCharacterTransform_one f
  map_mul' τ υ := by
    apply MulEquiv.ext
    intro f
    exact absoluteContinuousCharacterTransform_mul τ υ f

theorem absoluteContinuousCharacterAction_apply (τ : RingAut K)
    (f : Gal(AlgebraicClosure K/K) →ₜ* A) :
    absoluteContinuousCharacterAction τ f = absoluteContinuousCharacterTransform τ f