import Mathlib
import Definitions.Def_HopfAlgebra_HopfKerHopf

set_option autoImplicit false
set_option linter.unusedSectionVars false

open scoped TensorProduct
open Coalgebra WithConv

universe u v w x

namespace HopfAlgebra

class IsHopfTower (k : Type u) (A : Type v) (C : Type w) [CommRing k] [CommRing A] [CommRing C]
    [HopfAlgebra k A] [HopfAlgebra k C] [Algebra A C] [IsScalarTower k A C] : Prop where
  comul_algebraMap : ∀ a : A, comul (R := k) (algebraMap A C a) =
    Algebra.TensorProduct.map (IsScalarTower.toAlgHom k A C) (IsScalarTower.toAlgHom k A C)
      (comul (R := k) a)
  counit_algebraMap : ∀ a : A, counit (R := k) (algebraMap A C a) = counit (R := k) a

namespace IsHopfTower

variable (k : Type u) (A : Type v) (C : Type w) [CommRing k] [CommRing A] [CommRing C]
    [HopfAlgebra k A] [HopfAlgebra k C] [Algebra A C] [IsScalarTower k A C]

instance refl : IsHopfTower k C C where
  comul_algebraMap c := by
    rw [Algebra.algebraMap_self, RingHom.id_apply]
    conv_lhs => rw [← (ℛ k c).eq]
    rw [← (ℛ k c).eq, map_sum]
    simp
  counit_algebraMap c := by simp

variable [IsHopfTower k A C]

noncomputable def toBialgHom : A →ₐc[k] C :=
  BialgHom.ofAlgHom (IsScalarTower.toAlgHom k A C)
    (by ext a; simpa using IsHopfTower.counit_algebraMap (k := k) (A := A) (C := C) a)
    (by ext a; simpa using (IsHopfTower.comul_algebraMap (k := k) (A := A) (C := C) a).symm)

@[simp] theorem toBialgHom_apply (a : A) : toBialgHom k A C a = algebraMap A C a := rfl

theorem coe_toBialgHom : ((toBialgHom k A C : A →ₐc[k] C) : A →ₐ[k] C) =
    IsScalarTower.toAlgHom k A C := rfl

theorem algebraMap_antipode (a : A) :
    algebraMap A C (antipode k a) = antipode k (algebraMap A C a) :=
  HopfKerHopf.map_antipode (toBialgHom k A C) a

noncomputable def reprMap {a : A} {ι : Type*} (𝓡 : Coalgebra.Repr k a ι) :
    Coalgebra.Repr k (algebraMap A C a) ι where
  index := 𝓡.index
  left i := algebraMap A C (𝓡.left i)
  right i := algebraMap A C (𝓡.right i)
  eq := by
    rw [IsHopfTower.comul_algebraMap (k := k), ← 𝓡.eq, map_sum]
    simp

@[simp] theorem reprMap_index {a : A} {ι : Type*} (𝓡 : Coalgebra.Repr k a ι) : (reprMap k A C 𝓡).index = 𝓡.index := rfl
@[simp] theorem reprMap_left {a : A} {ι : Type*} (𝓡 : Coalgebra.Repr k a ι) (i : ι) :
    (reprMap k A C 𝓡).left i = algebraMap A C (𝓡.left i) := rfl
@[simp] theorem reprMap_right {a : A} {ι : Type*} (𝓡 : Coalgebra.Repr k a ι) (i : ι) :
    (reprMap k A C 𝓡).right i = algebraMap A C (𝓡.right i) := rfl

theorem sum_tmul_algebraMap_eq {a : A} {ι : Type*} (𝓡 : Coalgebra.Repr k a ι) :
    ∑ i ∈ 𝓡.index, algebraMap A C (𝓡.left i) ⊗ₜ[k] algebraMap A C (𝓡.right i) =
      comul (R := k) (algebraMap A C a) :=
  (reprMap k A C 𝓡).eq

variable {k A C} in
omit [IsHopfTower k A C] in

theorem trans (B : Type*) [CommRing B] [HopfAlgebra k B] [Algebra A B] [Algebra B C]
    [IsScalarTower k A B] [IsScalarTower k B C] [IsScalarTower A B C]
    [IsHopfTower k A B] [IsHopfTower k B C] : IsHopfTower k A C where
  comul_algebraMap a := by
    rw [IsScalarTower.algebraMap_apply A B C, IsHopfTower.comul_algebraMap (k := k),
      IsHopfTower.comul_algebraMap (k := k), ← (ℛ k a).eq]
    simp [← IsScalarTower.algebraMap_apply]
  counit_algebraMap a := by
    rw [IsScalarTower.algebraMap_apply A B C, IsHopfTower.counit_algebraMap (k := k),
      IsHopfTower.counit_algebraMap (k := k)]

end IsHopfTower

section augIdeal

variable (k : Type u) (A : Type v) [CommRing k] [CommRing A] [HopfAlgebra k A]

def augIdeal : Ideal A := RingHom.ker (Bialgebra.counitAlgHom k A)

variable {A} in
@[simp] theorem mem_augIdeal {a : A} : a ∈ augIdeal k A ↔ counit (R := k) a = 0 := Iff.rfl

variable {A} in
theorem sub_algebraMap_counit_mem_augIdeal (a : A) :
    a - algebraMap k A (counit (R := k) a) ∈ augIdeal k A := by
  simp [mem_augIdeal, Bialgebra.counit_algebraMap]

theorem augIdeal_ne_top [Nontrivial k] : augIdeal k A ≠ ⊤ := by
  rw [Ne, Ideal.eq_top_iff_one, mem_augIdeal, Bialgebra.counit_one]
  exact one_ne_zero

theorem sum_counit_right_smul {a : A} {ι : Type*} (𝓡 : Coalgebra.Repr k a ι) :
    ∑ i ∈ 𝓡.index, counit (R := k) (𝓡.right i) • 𝓡.left i = a := by
  simpa only [map_sum, TensorProduct.lift.tmul, LinearMap.flip_apply, LinearMap.lsmul_apply, one_smul]
    using congr(TensorProduct.lift (LinearMap.lsmul k A).flip $(sum_tmul_counit_eq (R := k) 𝓡))

end augIdeal

structure IsHopfSubalgebra (k : Type u) {H : Type v} [CommRing k] [CommRing H] [HopfAlgebra k H]
    (K : Subalgebra k H) : Prop where
  comul_mem : ∀ x ∈ K, comul (R := k) x ∈
    Submodule.span k {t : H ⊗[k] H | ∃ a ∈ K, ∃ b ∈ K, t = a ⊗ₜ[k] b}
  antipode_mem : ∀ x ∈ K, antipode k x ∈ K

namespace IsHopfSubalgebra

variable {k : Type u} {H : Type v} [CommRing k] [CommRing H] [HopfAlgebra k H]
variable {K : Subalgebra k H}

noncomputable def ι₂A (K : Subalgebra k H) : ↥K ⊗[k] ↥K →ₐ[k] H ⊗[k] H :=
  Algebra.TensorProduct.map K.val K.val

noncomputable def ι₂ (K : Subalgebra k H) : ↥K ⊗[k] ↥K →ₗ[k] H ⊗[k] H := (ι₂A K).toLinearMap

theorem ι₂_eq_map : ι₂ K = TensorProduct.map K.val.toLinearMap K.val.toLinearMap :=
  TensorProduct.ext' fun _ _ => rfl

@[simp] theorem ι₂_tmul (s t : ↥K) : ι₂ K (s ⊗ₜ[k] t) = (s : H) ⊗ₜ[k] (t : H) := rfl

theorem ι₂_mul (x y : ↥K ⊗[k] ↥K) : ι₂ K (x * y) = ι₂ K x * ι₂ K y := map_mul (ι₂A K) x y

theorem ι₂_one : ι₂ K 1 = 1 := map_one (ι₂A K)

theorem range_ι₂ : LinearMap.range (ι₂ K) =
    Submodule.span k {t : H ⊗[k] H | ∃ a ∈ K, ∃ b ∈ K, t = a ⊗ₜ[k] b} := by
  rw [ι₂_eq_map, TensorProduct.range_map, Submodule.map₂_eq_span_image2]
  congr 1
  ext t
  simp only [Set.mem_image2, SetLike.mem_coe, LinearMap.mem_range, AlgHom.toLinearMap_apply,
    Subalgebra.coe_val, Subtype.exists, exists_prop, TensorProduct.mk_apply, Set.mem_setOf_eq]
  constructor
  · rintro ⟨a, ⟨a', ha', rfl⟩, b, ⟨b', hb', rfl⟩, rfl⟩
    exact ⟨a', ha', b', hb', rfl⟩
  · rintro ⟨a, ha, b, hb, rfl⟩
    exact ⟨a, ⟨a, ha, rfl⟩, b, ⟨b, hb, rfl⟩, rfl⟩

variable [Module.Flat k H] [Module.Flat k ↥K]

theorem ι₂_injective : Function.Injective (ι₂ K) := by
  have h1 : Function.Injective (K.val.toLinearMap.lTensor ↥K) :=
    Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective
  have h2 : Function.Injective (K.val.toLinearMap.rTensor H) :=
    Module.Flat.rTensor_preserves_injective_linearMap _ Subtype.val_injective
  rw [ι₂_eq_map, ← LinearMap.rTensor_comp_lTensor]
  exact h2.comp h1

noncomputable def ι₃ (K : Subalgebra k H) : ↥K ⊗[k] (↥K ⊗[k] ↥K) →ₗ[k] H ⊗[k] (H ⊗[k] H) :=
  TensorProduct.map K.val.toLinearMap (ι₂ K)

@[simp] theorem ι₃_tmul (s : ↥K) (z : ↥K ⊗[k] ↥K) : ι₃ K (s ⊗ₜ[k] z) = (s : H) ⊗ₜ[k] ι₂ K z := rfl

theorem ι₃_injective : Function.Injective (ι₃ K) := by
  have h1 : Function.Injective ((ι₂ K).lTensor ↥K) :=
    Module.Flat.lTensor_preserves_injective_linearMap _ ι₂_injective
  have h2 : Function.Injective (K.val.toLinearMap.rTensor (H ⊗[k] H)) :=
    Module.Flat.rTensor_preserves_injective_linearMap _ Subtype.val_injective
  rw [ι₃, ← LinearMap.rTensor_comp_lTensor]
  exact h2.comp h1

variable (hK : IsHopfSubalgebra k K)
include hK

theorem comul_coe_mem_range (s : ↥K) : comul (R := k) (s : H) ∈ LinearMap.range (ι₂ K) := by
  rw [range_ι₂]; exact hK.comul_mem s s.2

noncomputable def comulK : ↥K →ₗ[k] ↥K ⊗[k] ↥K :=
  (LinearEquiv.ofInjective (ι₂ K) ι₂_injective).symm.toLinearMap
    ∘ₗ ((comul (R := k) (A := H)) ∘ₗ K.val.toLinearMap).codRestrict (LinearMap.range (ι₂ K))
        hK.comul_coe_mem_range

@[simp] theorem ι₂_comulK (s : ↥K) : ι₂ K (hK.comulK s) = comul (R := k) (s : H) := by
  simp only [comulK, LinearMap.comp_apply, LinearEquiv.coe_coe, LinearEquiv.ofInjective_symm_apply,
    LinearMap.codRestrict_apply, AlgHom.toLinearMap_apply, Subalgebra.coe_val]

omit hK in

noncomputable def counitK (K : Subalgebra k H) : ↥K →ₗ[k] k := counit ∘ₗ K.val.toLinearMap

omit [Module.Flat k H] [Module.Flat k ↥K] hK in
@[simp] theorem counitK_apply (s : ↥K) : counitK K s = counit (R := k) (s : H) := rfl

omit [Module.Flat k H] [Module.Flat k ↥K] hK in
theorem rTensor_counitK (z : ↥K ⊗[k] ↥K) :
    K.val.toLinearMap.lTensor k ((counitK K).rTensor ↥K z)
      = (counit (R := k) (A := H)).rTensor H (ι₂ K z) := by
  induction z with
  | zero => simp
  | add x y hx hy => simp only [map_add, hx, hy]
  | tmul x y => simp

omit [Module.Flat k H] [Module.Flat k ↥K] hK in
theorem lTensor_counitK (z : ↥K ⊗[k] ↥K) :
    K.val.toLinearMap.rTensor k ((counitK K).lTensor ↥K z)
      = (counit (R := k) (A := H)).lTensor H (ι₂ K z) := by
  induction z with
  | zero => simp
  | add x y hx hy => simp only [map_add, hx, hy]
  | tmul x y => simp

theorem ι₃_lTensor_comulK (z : ↥K ⊗[k] ↥K) :
    ι₃ K (hK.comulK.lTensor ↥K z) = (comul (R := k) (A := H)).lTensor H (ι₂ K z) := by
  induction z with
  | zero => simp only [LinearMap.map_zero]
  | add x y hx hy => simp only [map_add, hx, hy]
  | tmul x y => simp

theorem ι₃_assoc_rTensor_comulK (z : ↥K ⊗[k] ↥K) :
    ι₃ K ((TensorProduct.assoc k _ _ _).toLinearMap (hK.comulK.rTensor ↥K z))
      = (TensorProduct.assoc k H H H).toLinearMap ((comul (R := k) (A := H)).rTensor H (ι₂ K z)) := by
  induction z with
  | zero => simp only [LinearMap.map_zero]
  | add x y hx hy => simp only [map_add, hx, hy]
  | tmul x y =>
      simp only [LinearMap.rTensor_tmul, ι₂_tmul]
      rw [← hK.ι₂_comulK x]
      induction hK.comulK x with
      | zero => simp only [LinearMap.map_zero, TensorProduct.zero_tmul]
      | add c d hc hd => simp only [TensorProduct.add_tmul, map_add, hc, hd]
      | tmul c d => simp [LinearEquiv.coe_coe]

@[reducible] noncomputable def coalgebra : Coalgebra k ↥K where
  comul := hK.comulK
  counit := counitK K
  coassoc := by
    ext s
    apply ι₃_injective
    rw [LinearMap.comp_apply, LinearMap.comp_apply, LinearMap.comp_apply,
      ι₃_assoc_rTensor_comulK, ι₃_lTensor_comulK, ι₂_comulK]
    exact LinearMap.congr_fun (Coalgebra.coassoc (R := k) (A := H)) (s : H)
  rTensor_counit_comp_comul := by
    ext s
    have hinj : Function.Injective (K.val.toLinearMap.lTensor k) :=
      Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective
    apply hinj
    simp only [LinearMap.comp_apply, TensorProduct.mk_apply, LinearMap.lTensor_tmul]
    rw [rTensor_counitK, ι₂_comulK, Coalgebra.rTensor_counit_comul]; rfl
  lTensor_counit_comp_comul := by
    ext s
    have hinj : Function.Injective (K.val.toLinearMap.rTensor k) :=
      Module.Flat.rTensor_preserves_injective_linearMap _ Subtype.val_injective
    apply hinj
    simp only [LinearMap.comp_apply, LinearMap.flip_apply, TensorProduct.mk_apply, LinearMap.rTensor_tmul]
    rw [lTensor_counitK, ι₂_comulK, Coalgebra.lTensor_counit_comul]; rfl

theorem comul_def (s : ↥K) : (letI := hK.coalgebra; comul (R := k) s) = hK.comulK s := rfl

theorem counit_coe (s : ↥K) : (letI := hK.coalgebra; counit (R := k) s) = counit (R := k) (s : H) := rfl

theorem ι₂_comul (s : ↥K) : ι₂ K (letI := hK.coalgebra; comul (R := k) s) = comul (R := k) (s : H) :=
  hK.ι₂_comulK s

theorem map_val_val_comul (s : ↥K) :
    TensorProduct.map K.val.toLinearMap K.val.toLinearMap (letI := hK.coalgebra; comul (R := k) s) =
      comul (R := k) (s : H) := by
  rw [← ι₂_eq_map, ι₂_comul]

@[reducible] noncomputable def bialgebra : Bialgebra k ↥K :=
  letI := hK.coalgebra
  { counit_one := by rw [counit_coe]; simp
    mul_compr₂_counit := by
      ext a b
      exact (Bialgebra.counit_mul (R := k) (a : H) (b : H) : _)
    comul_one := by
      apply ι₂_injective
      rw [ι₂_comul, ι₂_one]; simp
    mul_compr₂_comul := by
      ext a b
      apply ι₂_injective
      change ι₂ K (comul (R := k) (a * b)) = ι₂ K (comul (R := k) a * comul (R := k) b)
      rw [ι₂_mul, ι₂_comul, ι₂_comul, ι₂_comul, Subalgebra.coe_mul, Bialgebra.comul_mul] }

noncomputable def antipodeK : ↥K →ₗ[k] ↥K where
  toFun s := ⟨antipode k (s : H), hK.antipode_mem s s.2⟩
  map_add' s t := by ext; simp
  map_smul' r s := by ext; simp

@[simp] theorem coe_antipodeK (s : ↥K) : ((hK.antipodeK s : ↥K) : H) = antipode k (s : H) := rfl

theorem val_mul'_rTensor_antipodeK (z : ↥K ⊗[k] ↥K) :
    ((LinearMap.mul' k ↥K (hK.antipodeK.rTensor _ z) : ↥K) : H)
      = LinearMap.mul' k H ((antipode k (A := H)).rTensor H (ι₂ K z)) := by
  induction z with
  | zero => simp
  | add x y hx hy => simp only [map_add, Subalgebra.coe_add, hx, hy]
  | tmul x y => simp

theorem val_mul'_lTensor_antipodeK (z : ↥K ⊗[k] ↥K) :
    ((LinearMap.mul' k ↥K (hK.antipodeK.lTensor _ z) : ↥K) : H)
      = LinearMap.mul' k H ((antipode k (A := H)).lTensor H (ι₂ K z)) := by
  induction z with
  | zero => simp
  | add x y hx hy => simp only [map_add, Subalgebra.coe_add, hx, hy]
  | tmul x y => simp

@[reducible] noncomputable def hopfAlgebra : HopfAlgebra k ↥K :=
  letI := hK.bialgebra
  { antipode := hK.antipodeK
    mul_antipode_rTensor_comul := by
      ext s
      simp only [LinearMap.comp_apply, Algebra.linearMap_apply, Subalgebra.coe_algebraMap]
      rw [val_mul'_rTensor_antipodeK, ι₂_comul, mul_antipode_rTensor_comul_apply, counit_coe]
    mul_antipode_lTensor_comul := by
      ext s
      simp only [LinearMap.comp_apply, Algebra.linearMap_apply, Subalgebra.coe_algebraMap]
      rw [val_mul'_lTensor_antipodeK, ι₂_comul, mul_antipode_lTensor_comul_apply, counit_coe] }

theorem coe_antipode (s : ↥K) :
    ((letI := hK.hopfAlgebra; antipode k s : ↥K) : H) = antipode k (s : H) := rfl

theorem isHopfTower : letI := hK.hopfAlgebra; IsHopfTower k ↥K H := by
  letI := hK.hopfAlgebra
  refine ⟨fun s => ?_, fun s => rfl⟩
  change comul (R := k) (s : H) = _
  rw [← hK.map_val_val_comul s]
  rfl

end IsHopfSubalgebra

namespace HopfTower

section AntipodeAlgHom
variable (k : Type u) (C : Type v) [CommRing k] [CommRing C] [HopfAlgebra k C]

noncomputable def antipodeAlgHom : C →ₐ[k] C :=
  AlgHom.ofLinearMap (antipode k) antipode_one fun a b => by rw [antipode_mul, mul_comm]
@[simp] theorem antipodeAlgHom_apply (x : C) : antipodeAlgHom k C x = antipode k x := rfl

variable {k C}
variable {L : Type w} [CommRing L] [Algebra k L]

theorem convMul_comp_antipodeAlgHom (φ : C →ₐ[k] L) :
    toConv φ * toConv (φ.comp (antipodeAlgHom k C)) = 1 := by
  refine WithConv.ext (AlgHom.ext fun x => ?_)
  change (toConv φ * toConv (φ.comp (antipodeAlgHom k C))) x = (1 : WithConv (C →ₐ[k] L)) x
  rw [AlgHom.convMul_apply, AlgHom.convOne_apply, ofConv_toConv, ofConv_toConv]
  have h : ∀ z : C ⊗[k] C, Algebra.TensorProduct.lift φ (φ.comp (antipodeAlgHom k C))
      (fun _ _ => .all _ _) z = φ (LinearMap.mul' k C ((antipode k).lTensor C z)) := by
    intro z
    induction z with
    | zero => simp
    | tmul x y => simp [LinearMap.lTensor_tmul]
    | add x y hx hy => simp [map_add, hx, hy]
  rw [h, mul_antipode_lTensor_comul_apply, AlgHom.commutes]

theorem comp_antipodeAlgHom_convMul (φ : C →ₐ[k] L) :
    toConv (φ.comp (antipodeAlgHom k C)) * toConv φ = 1 := by
  refine WithConv.ext (AlgHom.ext fun x => ?_)
  change (toConv (φ.comp (antipodeAlgHom k C)) * toConv φ) x = (1 : WithConv (C →ₐ[k] L)) x
  rw [AlgHom.convMul_apply, AlgHom.convOne_apply, ofConv_toConv, ofConv_toConv]
  have h : ∀ z : C ⊗[k] C, Algebra.TensorProduct.lift (φ.comp (antipodeAlgHom k C)) φ
      (fun _ _ => .all _ _) z = φ (LinearMap.mul' k C ((antipode k).rTensor C z)) := by
    intro z
    induction z with
    | zero => simp
    | tmul x y => simp [LinearMap.rTensor_tmul]
    | add x y hx hy => simp [map_add, hx, hy]
  rw [h, mul_antipode_rTensor_comul_apply, AlgHom.commutes]

end AntipodeAlgHom

section Galois

variable (k : Type u) (A : Type v) (B : Type w) (C : Type x)
  [CommRing k] [CommRing A] [CommRing B] [CommRing C]
  [HopfAlgebra k A] [HopfAlgebra k B] [HopfAlgebra k C]
  [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
  [IsScalarTower k A B] [IsScalarTower k B C] [IsScalarTower k A C]
  [IsHopfTower k A B] [IsHopfTower k B C] [IsHopfTower k A C]

def augIdealMap : Ideal B := (augIdeal k A).map (algebraMap A B)

theorem algebraMap_mem_augIdealMap {a : A} (ha : counit (R := k) a = 0) :
    algebraMap A B a ∈ augIdealMap k A B :=
  Ideal.mem_map_of_mem _ ((mem_augIdeal k).2 ha)

theorem mkₐ_algebraMap (a : A) :
    Ideal.Quotient.mkₐ k (augIdealMap k A B) (algebraMap A B a) =
      counit (R := k) a • (1 : B ⧸ augIdealMap k A B) := by
  rw [Algebra.smul_def, mul_one, Ideal.Quotient.mkₐ_eq_mk, ← Ideal.Quotient.mk_algebraMap,
    Ideal.Quotient.eq, IsScalarTower.algebraMap_apply k A B, ← map_sub]
  exact Ideal.mem_map_of_mem _ (sub_algebraMap_counit_mem_augIdeal k a)

noncomputable def fwdAux : B →ₐ[k] C ⊗[k] (B ⧸ augIdealMap k A B) :=
  (Algebra.TensorProduct.map (IsScalarTower.toAlgHom k B C)
      (Ideal.Quotient.mkₐ k (augIdealMap k A B))).comp (Bialgebra.comulAlgHom k B)

theorem fwdAux_apply {b : B} {ι : Type*} (𝓡 : Coalgebra.Repr k b ι) :
    fwdAux k A B C b = ∑ i ∈ 𝓡.index,
      algebraMap B C (𝓡.left i) ⊗ₜ[k] Ideal.Quotient.mk (augIdealMap k A B) (𝓡.right i) := by
  simp only [fwdAux, AlgHom.comp_apply, Bialgebra.comulAlgHom_apply, ← 𝓡.eq, map_sum,
    Algebra.TensorProduct.map_tmul]
  rfl

theorem fwdAux_algebraMap_eq_sum {a : A} {ι : Type*} (𝓡 : Coalgebra.Repr k a ι) :
    fwdAux k A B C (algebraMap A B a) = ∑ i ∈ 𝓡.index,
      algebraMap A C (𝓡.left i) ⊗ₜ[k]
        Ideal.Quotient.mkₐ k (augIdealMap k A B) (algebraMap A B (𝓡.right i)) := by
  rw [fwdAux_apply k A B C (IsHopfTower.reprMap k A B 𝓡)]
  simp only [IsHopfTower.reprMap_index, IsHopfTower.reprMap_left, IsHopfTower.reprMap_right,
    ← IsScalarTower.algebraMap_apply]
  rfl

theorem fwdAux_algebraMap (a : A) :
    fwdAux k A B C (algebraMap A B a) = algebraMap A C a ⊗ₜ[k] 1 := by
  rw [fwdAux_algebraMap_eq_sum k A B C (ℛ k a)]
  simp only [mkₐ_algebraMap, TensorProduct.tmul_smul]
  have h : ∀ i, counit (R := k) ((ℛ k a).right i) • algebraMap A C ((ℛ k a).left i) ⊗ₜ[k]
      (1 : B ⧸ augIdealMap k A B) =
      (IsScalarTower.toAlgHom k A C (counit (R := k) ((ℛ k a).right i) • (ℛ k a).left i)) ⊗ₜ[k] 1 :=
    fun i => by rw [TensorProduct.smul_tmul', map_smul]; rfl
  simp_rw [h]
  rw [← TensorProduct.sum_tmul, ← map_sum, sum_counit_right_smul k A (ℛ k a)]
  rfl

noncomputable def fwdB : B →ₐ[A] C ⊗[k] (B ⧸ augIdealMap k A B) :=
  { fwdAux k A B C with
    commutes' := fun a => by
      change fwdAux k A B C (algebraMap A B a) = _
      rw [fwdAux_algebraMap, IsScalarTower.algebraMap_apply A C (C ⊗[k] (B ⧸ augIdealMap k A B)),
        Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply] }

@[simp] theorem fwdB_apply (b : B) : fwdB k A B C b = fwdAux k A B C b := rfl

noncomputable def galoisFwd : C ⊗[A] B →ₐ[C] C ⊗[k] (B ⧸ augIdealMap k A B) :=
  Algebra.TensorProduct.lift (Algebra.ofId C _) (fwdB k A B C) fun _ _ => .all _ _

@[simp] theorem galoisFwd_tmul (c : C) (b : B) :
    galoisFwd k A B C (c ⊗ₜ[A] b) = (c ⊗ₜ[k] (1 : B ⧸ augIdealMap k A B)) * fwdAux k A B C b := by
  simp [galoisFwd, Algebra.ofId_apply, Algebra.TensorProduct.algebraMap_apply]

noncomputable def invAux : B →ₐ[k] C ⊗[A] B :=
  (Algebra.TensorProduct.lift
      ((Algebra.TensorProduct.includeLeft (S := C) (R := A) (A := C) (B := B)).restrictScalars k)
      ((Algebra.TensorProduct.includeRight (R := A) (A := C) (B := B)).restrictScalars k)
      (fun _ _ => .all _ _)).comp
    ((Algebra.TensorProduct.map ((antipodeAlgHom k C).comp (IsScalarTower.toAlgHom k B C))
        (AlgHom.id k B)).comp (Bialgebra.comulAlgHom k B))

theorem invAux_apply {b : B} {ι : Type*} (𝓡 : Coalgebra.Repr k b ι) :
    invAux k A B C b = ∑ i ∈ 𝓡.index, antipode k (algebraMap B C (𝓡.left i)) ⊗ₜ[A] 𝓡.right i := by
  simp only [invAux, AlgHom.comp_apply, Bialgebra.comulAlgHom_apply, ← 𝓡.eq, map_sum,
    Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.lift_tmul]
  refine Finset.sum_congr rfl fun i _ => ?_
  simp [Algebra.TensorProduct.tmul_mul_tmul]

omit [HopfAlgebra k B] [IsScalarTower k A B] [IsScalarTower k B C] [IsHopfTower k A B]
  [IsHopfTower k B C] [IsHopfTower k A C] in

theorem tmul_algebraMap (c : C) (a : A) :
    c ⊗ₜ[A] algebraMap A B a = (algebraMap A C a * c) ⊗ₜ[A] (1 : B) := by
  rw [Algebra.algebraMap_eq_smul_one, ← TensorProduct.smul_tmul, Algebra.smul_def]

theorem invAux_algebraMap_eq_sum {a : A} {ι : Type*} (𝓡 : Coalgebra.Repr k a ι) :
    invAux k A B C (algebraMap A B a) =
      ∑ i ∈ 𝓡.index, antipode k (algebraMap A C (𝓡.left i)) ⊗ₜ[A] algebraMap A B (𝓡.right i) := by
  rw [invAux_apply k A B C (IsHopfTower.reprMap k A B 𝓡)]
  simp only [IsHopfTower.reprMap_index, IsHopfTower.reprMap_left, IsHopfTower.reprMap_right,
    ← IsScalarTower.algebraMap_apply]

theorem invAux_algebraMap_of_counit_eq_zero {a : A} (ha : counit (R := k) a = 0) :
    invAux k A B C (algebraMap A B a) = 0 := by
  rw [invAux_algebraMap_eq_sum k A B C (ℛ k a)]
  have h : ∀ i ∈ (ℛ k a).index,
      antipode k (algebraMap A C ((ℛ k a).left i)) ⊗ₜ[A] algebraMap A B ((ℛ k a).right i) =
        (antipode k (algebraMap A C ((ℛ k a).left i)) * algebraMap A C ((ℛ k a).right i)) ⊗ₜ[A]
          (1 : B) := fun i _ => by
    rw [tmul_algebraMap, mul_comm]
  refine (Finset.sum_congr rfl h).trans ?_
  rw [← TensorProduct.sum_tmul]
  have h2 : ∑ i ∈ (ℛ k a).index,
      antipode k (algebraMap A C ((ℛ k a).left i)) * algebraMap A C ((ℛ k a).right i) =
        algebraMap k C (counit (R := k) (algebraMap A C a)) :=
    sum_antipode_mul_eq_algebraMap_counit (IsHopfTower.reprMap k A C (ℛ k a))
  rw [h2, IsHopfTower.counit_algebraMap, ha, map_zero, TensorProduct.zero_tmul]

theorem augIdealMap_le_ker_invAux :
    augIdealMap k A B ≤ RingHom.ker (invAux k A B C) := by
  rw [augIdealMap, Ideal.map_le_iff_le_comap]
  intro a ha
  exact invAux_algebraMap_of_counit_eq_zero k A B C ((mem_augIdeal k).1 ha)

noncomputable def invQuot : (B ⧸ augIdealMap k A B) →ₐ[k] C ⊗[A] B :=
  Ideal.Quotient.liftₐ (augIdealMap k A B) (invAux k A B C)
    fun _ hb => augIdealMap_le_ker_invAux k A B C hb

@[simp] theorem invQuot_mk (b : B) :
    invQuot k A B C (Ideal.Quotient.mk (augIdealMap k A B) b) = invAux k A B C b := rfl

noncomputable def galoisInv : C ⊗[k] (B ⧸ augIdealMap k A B) →ₐ[C] C ⊗[A] B :=
  Algebra.TensorProduct.lift (Algebra.ofId C _) (invQuot k A B C) fun _ _ => .all _ _

@[simp] theorem galoisInv_tmul (c : C) (q : B ⧸ augIdealMap k A B) :
    galoisInv k A B C (c ⊗ₜ[k] q) = (c ⊗ₜ[A] (1 : B)) * invQuot k A B C q := by
  simp [galoisInv, Algebra.ofId_apply, Algebra.TensorProduct.algebraMap_apply]

noncomputable def θ₁ : B ⊗[k] (B ⊗[k] B) →ₗ[k] C ⊗[A] B :=
  (Algebra.TensorProduct.lift
      ((Algebra.TensorProduct.includeLeft (S := C) (R := A) (A := C) (B := B)).restrictScalars k)
      (Algebra.TensorProduct.lift
        ((Algebra.TensorProduct.includeLeft (S := C) (R := A) (A := C) (B := B)).restrictScalars k)
        ((Algebra.TensorProduct.includeRight (R := A) (A := C) (B := B)).restrictScalars k)
        (fun _ _ => .all _ _))
      (fun _ _ => .all _ _)).toLinearMap ∘ₗ
    TensorProduct.map (IsScalarTower.toAlgHom k B C).toLinearMap
      (TensorProduct.map ((antipodeAlgHom k C).comp (IsScalarTower.toAlgHom k B C)).toLinearMap
        LinearMap.id)

@[simp] theorem θ₁_tmul (u v w : B) :
    θ₁ k A B C (u ⊗ₜ[k] (v ⊗ₜ[k] w)) =
      (algebraMap B C u * antipode k (algebraMap B C v)) ⊗ₜ[A] w := by
  simp [θ₁, Algebra.TensorProduct.tmul_mul_tmul]

noncomputable def θ₂ : B ⊗[k] (B ⊗[k] B) →ₗ[k] C ⊗[k] (B ⧸ augIdealMap k A B) :=
  (Algebra.TensorProduct.lift
      (Algebra.TensorProduct.includeLeft (R := k) (A := C) (B := B ⧸ augIdealMap k A B))
      (Algebra.TensorProduct.lift
        (Algebra.TensorProduct.includeLeft (R := k) (A := C) (B := B ⧸ augIdealMap k A B))
        (Algebra.TensorProduct.includeRight (R := k) (A := C) (B := B ⧸ augIdealMap k A B))
        (fun _ _ => .all _ _))
      (fun _ _ => .all _ _)).toLinearMap ∘ₗ
    TensorProduct.map ((antipodeAlgHom k C).comp (IsScalarTower.toAlgHom k B C)).toLinearMap
      (TensorProduct.map (IsScalarTower.toAlgHom k B C).toLinearMap
        (Ideal.Quotient.mkₐ k (augIdealMap k A B)).toLinearMap)

@[simp] theorem θ₂_tmul (u v w : B) :
    θ₂ k A B C (u ⊗ₜ[k] (v ⊗ₜ[k] w)) =
      (antipode k (algebraMap B C u) * algebraMap B C v) ⊗ₜ[k]
        Ideal.Quotient.mk (augIdealMap k A B) w := by
  simp [θ₂, Algebra.TensorProduct.tmul_mul_tmul]

theorem galoisInv_fwdAux (b : B) : galoisInv k A B C (fwdAux k A B C b) = 1 ⊗ₜ[A] b := by
  let 𝓡 := ℛ k b
  let a₁ : (i : _) → Coalgebra.Repr k (𝓡.left i) (_ × _) := fun i => ℛ k (𝓡.left i)
  let a₂ : (i : _) → Coalgebra.Repr k (𝓡.right i) (_ × _) := fun i => ℛ k (𝓡.right i)
  have key := congr(θ₁ k A B C $(sum_tmul_tmul_eq 𝓡 a₁ a₂))
  simp only [map_sum, θ₁_tmul] at key

  have lhs : galoisInv k A B C (fwdAux k A B C b) = ∑ i ∈ 𝓡.index, ∑ j ∈ (a₂ i).index,
      (algebraMap B C (𝓡.left i) * antipode k (algebraMap B C ((a₂ i).left j))) ⊗ₜ[A]
        (a₂ i).right j := by
    rw [fwdAux_apply k A B C 𝓡, map_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [galoisInv_tmul, invQuot_mk, invAux_apply k A B C (a₂ i), Finset.mul_sum]
    refine Finset.sum_congr rfl fun j _ => ?_
    rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul]
  have rhs : ∑ i ∈ 𝓡.index, ∑ j ∈ (a₁ i).index,
      (algebraMap B C ((a₁ i).left j) * antipode k (algebraMap B C ((a₁ i).right j))) ⊗ₜ[A]
        𝓡.right i = 1 ⊗ₜ[A] b := by
    have h : ∀ i ∈ 𝓡.index, ∑ j ∈ (a₁ i).index,
        (algebraMap B C ((a₁ i).left j) * antipode k (algebraMap B C ((a₁ i).right j))) ⊗ₜ[A]
          𝓡.right i = (1 : C) ⊗ₜ[A] (counit (R := k) (𝓡.left i) • 𝓡.right i) := fun i _ => by
      have h2 : ∑ j ∈ (a₁ i).index,
          algebraMap B C ((a₁ i).left j) * antipode k (algebraMap B C ((a₁ i).right j)) =
            algebraMap k C (counit (R := k) (algebraMap B C (𝓡.left i))) :=
        sum_mul_antipode_eq_algebraMap_counit (IsHopfTower.reprMap k B C (a₁ i))
      rw [← TensorProduct.sum_tmul, h2, IsHopfTower.counit_algebraMap,
        Algebra.algebraMap_eq_smul_one, ← TensorProduct.smul_tmul]
    rw [Finset.sum_congr rfl h, ← TensorProduct.tmul_sum, sum_counit_smul]
  rw [lhs, ← key, rhs]

theorem galoisFwd_invAux (b : B) :
    galoisFwd k A B C (invAux k A B C b) = 1 ⊗ₜ[k] Ideal.Quotient.mk (augIdealMap k A B) b := by
  let 𝓡 := ℛ k b
  let a₁ : (i : _) → Coalgebra.Repr k (𝓡.left i) (_ × _) := fun i => ℛ k (𝓡.left i)
  let a₂ : (i : _) → Coalgebra.Repr k (𝓡.right i) (_ × _) := fun i => ℛ k (𝓡.right i)
  have key := congr(θ₂ k A B C $(sum_tmul_tmul_eq 𝓡 a₁ a₂))
  simp only [map_sum, θ₂_tmul] at key
  have lhs : galoisFwd k A B C (invAux k A B C b) = ∑ i ∈ 𝓡.index, ∑ j ∈ (a₂ i).index,
      (antipode k (algebraMap B C (𝓡.left i)) * algebraMap B C ((a₂ i).left j)) ⊗ₜ[k]
        Ideal.Quotient.mk (augIdealMap k A B) ((a₂ i).right j) := by
    rw [invAux_apply k A B C 𝓡, map_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [galoisFwd_tmul, fwdAux_apply k A B C (a₂ i), Finset.mul_sum]
    refine Finset.sum_congr rfl fun j _ => ?_
    rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul]
  have rhs : ∑ i ∈ 𝓡.index, ∑ j ∈ (a₁ i).index,
      (antipode k (algebraMap B C ((a₁ i).left j)) * algebraMap B C ((a₁ i).right j)) ⊗ₜ[k]
        Ideal.Quotient.mk (augIdealMap k A B) (𝓡.right i) =
      1 ⊗ₜ[k] Ideal.Quotient.mk (augIdealMap k A B) b := by
    have h : ∀ i ∈ 𝓡.index, ∑ j ∈ (a₁ i).index,
        (antipode k (algebraMap B C ((a₁ i).left j)) * algebraMap B C ((a₁ i).right j)) ⊗ₜ[k]
          Ideal.Quotient.mk (augIdealMap k A B) (𝓡.right i) =
        (1 : C) ⊗ₜ[k] Ideal.Quotient.mk (augIdealMap k A B) (counit (R := k) (𝓡.left i) • 𝓡.right i) :=
      fun i _ => by
      have h2 : ∑ j ∈ (a₁ i).index,
          antipode k (algebraMap B C ((a₁ i).left j)) * algebraMap B C ((a₁ i).right j) =
            algebraMap k C (counit (R := k) (algebraMap B C (𝓡.left i))) :=
        sum_antipode_mul_eq_algebraMap_counit (IsHopfTower.reprMap k B C (a₁ i))
      rw [← TensorProduct.sum_tmul, h2, IsHopfTower.counit_algebraMap,
        Algebra.algebraMap_eq_smul_one, TensorProduct.smul_tmul, ← Ideal.Quotient.mkₐ_eq_mk k,
        map_smul]
    rw [Finset.sum_congr rfl h, ← TensorProduct.tmul_sum, ← map_sum, sum_counit_smul]
  rw [lhs, ← key, rhs]

theorem galoisInv_comp_galoisFwd :
    (galoisInv k A B C).comp (galoisFwd k A B C) = AlgHom.id C (C ⊗[A] B) := by
  refine Algebra.TensorProduct.ext (Subsingleton.elim _ _) ?_
  ext b
  simp only [AlgHom.coe_comp, AlgHom.coe_restrictScalars', Function.comp_apply,
    Algebra.TensorProduct.includeRight_apply, AlgHom.coe_id, id_eq, galoisFwd_tmul]
  rw [← Algebra.TensorProduct.one_def, one_mul, galoisInv_fwdAux]

theorem galoisFwd_comp_galoisInv :
    (galoisFwd k A B C).comp (galoisInv k A B C) = AlgHom.id C _ := by
  refine Algebra.TensorProduct.ext (Subsingleton.elim _ _) ?_
  refine Ideal.Quotient.algHom_ext k ?_
  ext b
  simp only [AlgHom.coe_comp, AlgHom.coe_restrictScalars', Function.comp_apply,
    Ideal.Quotient.mkₐ_eq_mk, Algebra.TensorProduct.includeRight_apply, AlgHom.coe_id, id_eq,
    galoisInv_tmul, invQuot_mk]
  rw [← Algebra.TensorProduct.one_def, one_mul, galoisFwd_invAux]

noncomputable def galoisEquiv : C ⊗[A] B ≃ₐ[C] C ⊗[k] (B ⧸ augIdealMap k A B) :=
  AlgEquiv.ofAlgHom (galoisFwd k A B C) (galoisInv k A B C) (galoisFwd_comp_galoisInv k A B C)
    (galoisInv_comp_galoisFwd k A B C)

theorem galoisEquiv_apply (z : C ⊗[A] B) : galoisEquiv k A B C z = galoisFwd k A B C z := rfl

theorem galoisEquiv_symm_apply (z : C ⊗[k] (B ⧸ augIdealMap k A B)) :
    (galoisEquiv k A B C).symm z = galoisInv k A B C z := rfl

theorem galoisEquiv_tmul (c : C) (b : B) :
    galoisEquiv k A B C (c ⊗ₜ[A] b) = (c ⊗ₜ[k] (1 : B ⧸ augIdealMap k A B)) * fwdAux k A B C b :=
  galoisFwd_tmul k A B C c b

theorem galoisEquiv_one_tmul (b : B) : galoisEquiv k A B C (1 ⊗ₜ[A] b) = fwdAux k A B C b := by
  rw [galoisEquiv_tmul, ← Algebra.TensorProduct.one_def, one_mul]

end Galois

section Naturality

universe y

variable (k : Type u) (A : Type v) (B : Type w) (B' : Type y) (C : Type x)
  [CommRing k] [CommRing A] [CommRing B] [CommRing B'] [CommRing C]
  [HopfAlgebra k A] [HopfAlgebra k B] [HopfAlgebra k B'] [HopfAlgebra k C]
  [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C]
  [Algebra A B'] [Algebra B' C] [IsScalarTower A B' C]
  [Algebra B B'] [IsScalarTower A B B'] [IsScalarTower B B' C]
  [IsScalarTower k A B] [IsScalarTower k B C] [IsScalarTower k A C]
  [IsScalarTower k A B'] [IsScalarTower k B' C] [IsScalarTower k B B']
  [IsHopfTower k A B] [IsHopfTower k B C] [IsHopfTower k A C]
  [IsHopfTower k A B'] [IsHopfTower k B' C] [IsHopfTower k B B']

omit [HopfAlgebra k B] [HopfAlgebra k B'] [Algebra B C] [IsScalarTower A B C] [Algebra B' C]
  [IsScalarTower A B' C] [IsScalarTower B B' C] [IsScalarTower k A B] [IsScalarTower k B C]
  [IsScalarTower k A B'] [IsScalarTower k B' C] [IsScalarTower k B B'] [IsHopfTower k A B]
  [IsHopfTower k B C] [IsHopfTower k A B'] [IsHopfTower k B' C] [IsHopfTower k B B']
  [HopfAlgebra k C] [Algebra A C] [IsScalarTower k A C] [IsHopfTower k A C] in
theorem augIdealMap_le_comap :
    augIdealMap k A B ≤ (augIdealMap k A B').comap (algebraMap B B') := by
  rw [augIdealMap, augIdealMap, Ideal.map_le_iff_le_comap, Ideal.comap_comap,
    ← IsScalarTower.algebraMap_eq]
  exact Ideal.le_comap_map

noncomputable def quotientMap : (B ⧸ augIdealMap k A B) →ₐ[k] (B' ⧸ augIdealMap k A B') :=
  Ideal.quotientMapₐ (augIdealMap k A B') (IsScalarTower.toAlgHom k B B')
    (augIdealMap_le_comap k A B B')

@[simp] theorem quotientMap_mk (b : B) :
    quotientMap k A B B' (Ideal.Quotient.mk (augIdealMap k A B) b) =
      Ideal.Quotient.mk (augIdealMap k A B') (algebraMap B B' b) := rfl

theorem fwdAux_algebraMap' (b : B) :
    fwdAux k A B' C (algebraMap B B' b) =
      Algebra.TensorProduct.map (AlgHom.id C C) (quotientMap k A B B') (fwdAux k A B C b) := by
  rw [fwdAux_apply k A B' C (IsHopfTower.reprMap k B B' (ℛ k b)), fwdAux_apply k A B C (ℛ k b),
    map_sum]
  simp only [IsHopfTower.reprMap_index, IsHopfTower.reprMap_left, IsHopfTower.reprMap_right,
    ← IsScalarTower.algebraMap_apply, Algebra.TensorProduct.map_tmul, AlgHom.coe_id, id_eq,
    quotientMap_mk]

theorem galoisEquiv_naturality (z : C ⊗[A] B) :
    galoisEquiv k A B' C
        (Algebra.TensorProduct.map (AlgHom.id C C) (IsScalarTower.toAlgHom A B B') z) =
      Algebra.TensorProduct.map (AlgHom.id C C) (quotientMap k A B B') (galoisEquiv k A B C z) := by
  suffices h : ((galoisEquiv k A B' C : _ ≃ₐ[C] _) : _ →ₐ[C] _).comp
      (Algebra.TensorProduct.map (AlgHom.id C C) (IsScalarTower.toAlgHom A B B')) =
      (Algebra.TensorProduct.map (AlgHom.id C C) (quotientMap k A B B')).comp
        (galoisEquiv k A B C : _ →ₐ[C] _) from congr($h z)
  refine Algebra.TensorProduct.ext (Subsingleton.elim _ _) ?_
  ext b
  simp only [AlgHom.coe_comp, AlgHom.coe_restrictScalars', Function.comp_apply,
    Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.map_tmul,
    map_one, IsScalarTower.coe_toAlgHom']
  change galoisEquiv k A B' C (1 ⊗ₜ[A] algebraMap B B' b) =
    Algebra.TensorProduct.map (AlgHom.id C C) (quotientMap k A B B') (galoisEquiv k A B C (1 ⊗ₜ[A] b))
  rw [galoisEquiv_one_tmul, galoisEquiv_one_tmul, fwdAux_algebraMap']

end Naturality

section Translate

variable (k : Type u) (C : Type v) [CommRing k] [CommRing C] [HopfAlgebra k C]

noncomputable def translate (φ : C →ₐ[k] k) : C →ₐ[k] C :=
  ((Algebra.TensorProduct.rid k k C).toAlgHom.comp
    (Algebra.TensorProduct.map (AlgHom.id k C) φ)).comp (Bialgebra.comulAlgHom k C)

variable {k C}

theorem translate_apply {x : C} (φ : C →ₐ[k] k) {ι : Type*} (𝓡 : Coalgebra.Repr k x ι) :
    translate k C φ x = ∑ i ∈ 𝓡.index, φ (𝓡.right i) • 𝓡.left i := by
  simp only [translate, AlgHom.comp_apply, Bialgebra.comulAlgHom_apply, ← 𝓡.eq, map_sum,
    Algebra.TensorProduct.map_tmul, AlgHom.coe_id, id_eq]
  refine Finset.sum_congr rfl fun i _ => ?_
  change Algebra.TensorProduct.rid k k C (𝓡.left i ⊗ₜ[k] φ (𝓡.right i)) = _
  rw [Algebra.TensorProduct.rid_tmul]

theorem counit_translate (φ : C →ₐ[k] k) (x : C) :
    counit (R := k) (translate k C φ x) = φ x := by
  rw [translate_apply φ (ℛ k x), map_sum]
  simp only [map_smul, smul_eq_mul, mul_comm (φ _)]
  have h := congr(TensorProduct.lid k k (TensorProduct.map LinearMap.id φ.toLinearMap
    $(sum_counit_tmul_eq (R := k) (ℛ k x))))
  simp only [map_sum, TensorProduct.map_tmul, LinearMap.id_coe, id_eq, AlgHom.toLinearMap_apply,
    TensorProduct.lid_tmul, smul_eq_mul, one_mul] at h
  exact h

theorem translate_one : translate k C (Bialgebra.counitAlgHom k C) = AlgHom.id k C := by
  ext x
  rw [translate_apply _ (ℛ k x)]
  simpa using sum_counit_right_smul k C (ℛ k x)

theorem convMul_apply' (φ ψ : C →ₐ[k] k) {x : C} {ι : Type*} (𝓡 : Coalgebra.Repr k x ι) :
    ofConv (toConv φ * toConv ψ) x = ∑ i ∈ 𝓡.index, φ (𝓡.left i) * ψ (𝓡.right i) := by
  rw [show ofConv (toConv φ * toConv ψ) x = (toConv φ * toConv ψ) x from rfl,
    AlgHom.convMul_apply, ofConv_toConv, ofConv_toConv, ← 𝓡.eq, map_sum]
  simp [Algebra.TensorProduct.lift_tmul]

theorem translate_translate (φ ψ : C →ₐ[k] k) (x : C) :
    translate k C φ (translate k C ψ x) = translate k C (ofConv (toConv φ * toConv ψ)) x := by
  let 𝓡 := ℛ k x
  let a₁ : (i : _) → Coalgebra.Repr k (𝓡.left i) (_ × _) := fun i => ℛ k (𝓡.left i)
  let a₂ : (i : _) → Coalgebra.Repr k (𝓡.right i) (_ × _) := fun i => ℛ k (𝓡.right i)

  let β : C ⊗[k] C →ₗ[k] k := LinearMap.mul' k k ∘ₗ TensorProduct.map φ.toLinearMap ψ.toLinearMap
  let θ : C ⊗[k] (C ⊗[k] C) →ₗ[k] C :=
    TensorProduct.lift ((LinearMap.lcomp k C β) ∘ₗ (LinearMap.lsmul k C).flip)
  have hθ : ∀ u v w : C, θ (u ⊗ₜ[k] (v ⊗ₜ[k] w)) = (φ v * ψ w) • u := fun u v w => by
    simp [θ, β]
  have key := congr(θ $(sum_tmul_tmul_eq 𝓡 a₁ a₂))
  simp only [map_sum, hθ] at key
  have lhs : translate k C φ (translate k C ψ x) =
      ∑ i ∈ 𝓡.index, ∑ j ∈ (a₁ i).index, (φ ((a₁ i).right j) * ψ (𝓡.right i)) • (a₁ i).left j := by
    rw [translate_apply ψ 𝓡, map_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [map_smul, translate_apply φ (a₁ i), Finset.smul_sum]
    refine Finset.sum_congr rfl fun j _ => ?_
    rw [smul_smul, mul_comm]
  have rhs : translate k C (ofConv (toConv φ * toConv ψ)) x =
      ∑ i ∈ 𝓡.index, ∑ j ∈ (a₂ i).index, (φ ((a₂ i).left j) * ψ ((a₂ i).right j)) • 𝓡.left i := by
    rw [translate_apply _ 𝓡]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [convMul_apply' φ ψ (a₂ i), Finset.sum_smul]
  rw [lhs, key, ← rhs]

theorem translate_comp_translate_antipode (φ : C →ₐ[k] k) :
    (translate k C φ).comp (translate k C (φ.comp (antipodeAlgHom k C))) = AlgHom.id k C := by
  ext x
  rw [AlgHom.comp_apply, translate_translate, convMul_comp_antipodeAlgHom]
  exact congr($(translate_one (k := k) (C := C)) x)

theorem translate_antipode_comp_translate (φ : C →ₐ[k] k) :
    (translate k C (φ.comp (antipodeAlgHom k C))).comp (translate k C φ) = AlgHom.id k C := by
  ext x
  rw [AlgHom.comp_apply, translate_translate, comp_antipodeAlgHom_convMul]
  exact congr($(translate_one (k := k) (C := C)) x)

variable (k C) in

noncomputable def translateEquiv (φ : C →ₐ[k] k) : C ≃ₐ[k] C :=
  AlgEquiv.ofAlgHom (translate k C φ) (translate k C (φ.comp (antipodeAlgHom k C)))
    (translate_comp_translate_antipode φ) (translate_antipode_comp_translate φ)

@[simp] theorem translateEquiv_apply (φ : C →ₐ[k] k) (x : C) :
    translateEquiv k C φ x = translate k C φ x := rfl

theorem comap_translate_augIdeal (φ : C →ₐ[k] k) :
    (RingHom.ker (Bialgebra.counitAlgHom k C)).comap (translate k C φ) = RingHom.ker φ := by
  ext x
  simp only [Ideal.mem_comap, RingHom.mem_ker, Bialgebra.counitAlgHom_apply, counit_translate]

theorem comp_translate (u φ : C →ₐ[k] k) :
    u.comp (translate k C φ) = ofConv (toConv u * toConv φ) := by
  ext x
  rw [AlgHom.comp_apply, translate_apply φ (ℛ k x), convMul_apply' u φ (ℛ k x), map_sum]
  simp [mul_comm]

end Translate

section TranslateTower

variable (k : Type u) (A : Type v) (C : Type w) [CommRing k] [CommRing A] [CommRing C]
    [HopfAlgebra k A] [HopfAlgebra k C] [Algebra A C] [IsScalarTower k A C]

theorem translate_algebraMap
    (hcomul : ∀ a : A, comul (R := k) (algebraMap A C a) =
      Algebra.TensorProduct.map (IsScalarTower.toAlgHom k A C) (IsScalarTower.toAlgHom k A C)
        (comul (R := k) a))
    (φ : C →ₐ[k] k) (a : A) :
    translate k C φ (algebraMap A C a) =
      algebraMap A C (translate k A (φ.comp (IsScalarTower.toAlgHom k A C)) a) := by
  let 𝓡 : Coalgebra.Repr k (algebraMap A C a) (A × A) :=
    { index := (ℛ k a).index
      left := fun i => algebraMap A C ((ℛ k a).left i)
      right := fun i => algebraMap A C ((ℛ k a).right i)
      eq := by rw [hcomul, ← (ℛ k a).eq, map_sum]; simp }
  rw [translate_apply φ 𝓡, translate_apply _ (ℛ k a), map_sum]
  refine Finset.sum_congr rfl fun i _ => ?_
  simp only [𝓡, Algebra.smul_def, map_mul, AlgHom.comp_apply, IsScalarTower.coe_toAlgHom',
    ← IsScalarTower.algebraMap_apply]

end TranslateTower

end HopfTower

end HopfAlgebra