import Mathlib
import Definitions.Def_PDivisibleGroup_Dimension

set_option autoImplicit false

noncomputable section

open scoped TensorProduct
open Coalgebra Bialgebra WithConv

universe u v w

namespace PDivisibleGroup.Hopf

section BaseChange

variable (R : Type u) [CommRing R] (S : Type w) [CommRing S] [Algebra R S]
  (A : Type v) [CommRing A] [Bialgebra R A]

theorem nsmulAlgHom_baseChange_tmul (n : ℕ) (s : S) (a : A) :
    nsmulAlgHom S (S ⊗[R] A) n (s ⊗ₜ[R] a) = s ⊗ₜ[R] nsmulAlgHom R A n a := by
  induction n generalizing s a with
  | zero =>
    rw [nsmulAlgHom_zero_apply, nsmulAlgHom_zero_apply, TensorProduct.counit_tmul,
      CommSemiring.counit_apply, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self,
      RingHom.id_apply, Algebra.algebraMap_eq_smul_one]
    rw [TensorProduct.smul_tmul]
  | succ n ih =>
    rw [nsmulAlgHom_succ, nsmulAlgHom_succ]
    change (toConv (nsmulAlgHom S (S ⊗[R] A) n) * toConv (AlgHom.id S (S ⊗[R] A))) (s ⊗ₜ[R] a) =
      s ⊗ₜ[R] (toConv (nsmulAlgHom R A n) * toConv (AlgHom.id R A)) a
    rw [AlgHom.convMul_apply, AlgHom.convMul_apply, TensorProduct.comul_tmul,
      CommSemiring.comul_apply]
    obtain ⟨ι, t, f, g, hrep⟩ :=
      (⟨_, _, _, _, (Coalgebra.Repr.arbitrary R a).eq⟩ :
        ∃ (ι : Type v) (t : Finset ι) (f g : ι → A), ∑ i ∈ t, f i ⊗ₜ[R] g i = comul (R := R) a)
    rw [← hrep, TensorProduct.tmul_sum, map_sum, map_sum, map_sum, TensorProduct.tmul_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_tmul, Algebra.TensorProduct.lift_tmul,
      Algebra.TensorProduct.lift_tmul]
    change nsmulAlgHom S (S ⊗[R] A) n ((1 : S) ⊗ₜ[R] f i) * (s ⊗ₜ[R] g i) =
      s ⊗ₜ[R] (nsmulAlgHom R A n (f i) * g i)
    rw [ih, Algebra.TensorProduct.tmul_mul_tmul, one_mul]

theorem nsmulAlgHom_baseChange (n : ℕ) :
    nsmulAlgHom S (S ⊗[R] A) n =
      Algebra.TensorProduct.map (AlgHom.id S S) (nsmulAlgHom R A n) := by
  ext a
  change nsmulAlgHom S (S ⊗[R] A) n ((1 : S) ⊗ₜ[R] a) = (1 : S) ⊗ₜ[R] nsmulAlgHom R A n a
  exact nsmulAlgHom_baseChange_tmul R S A n 1 a

theorem counit_baseChange_eq (x : S ⊗[R] A) :
    counit (R := S) x =
      Algebra.TensorProduct.rid R S S
        (Algebra.TensorProduct.map (AlgHom.id S S) (counitAlgHom R A) x) := by
  induction x using TensorProduct.induction_on with
  | zero => simp only [map_zero]
  | tmul s a =>
    rw [TensorProduct.counit_tmul, CommSemiring.counit_apply, Algebra.TensorProduct.map_tmul,
      Algebra.TensorProduct.rid_tmul]
    rfl
  | add x y hx hy => rw [map_add, hx, hy, map_add, map_add]

theorem augIdeal_baseChange :
    augIdeal S (S ⊗[R] A) =
      (augIdeal R A).map (Algebra.TensorProduct.includeRight : A →ₐ[R] S ⊗[R] A) := by
  have hsurj : Function.Surjective (counitAlgHom R A) := fun r =>
    ⟨algebraMap R A r, by rw [Bialgebra.counitAlgHom_apply, counit_algebraMap]⟩
  have hker := Algebra.TensorProduct.lTensor_ker (A := S) (counitAlgHom R A) hsurj
  change RingHom.ker (counitAlgHom S (S ⊗[R] A)) = (RingHom.ker (counitAlgHom R A)).map _
  rw [← hker]
  ext x
  rw [RingHom.mem_ker, RingHom.mem_ker, Bialgebra.counitAlgHom_apply, counit_baseChange_eq]
  have hmaps : Algebra.TensorProduct.map (AlgHom.id S S) (counitAlgHom R A) x =
      Algebra.TensorProduct.map (AlgHom.id R S) (counitAlgHom R A) x := by
    induction x using TensorProduct.induction_on with
    | zero => simp only [map_zero]
    | tmul s a => rfl
    | add x y hx hy => rw [map_add, map_add, hx, hy]
  rw [← hmaps]
  exact (Algebra.TensorProduct.rid R S S).map_eq_zero_iff

theorem torsionIdeal_baseChange (n : ℕ) :
    torsionIdeal S (S ⊗[R] A) n =
      (torsionIdeal R A n).map (Algebra.TensorProduct.includeRight : A →ₐ[R] S ⊗[R] A) := by
  rw [torsionIdeal, torsionIdeal, augIdeal_baseChange]
  change ((augIdeal R A).map (Algebra.TensorProduct.includeRight : A →ₐ[R] S ⊗[R] A).toRingHom).map
      (nsmulAlgHom S (S ⊗[R] A) n).toRingHom =
    ((augIdeal R A).map (nsmulAlgHom R A n).toRingHom).map
      (Algebra.TensorProduct.includeRight : A →ₐ[R] S ⊗[R] A).toRingHom
  rw [Ideal.map_map, Ideal.map_map]
  congr 1
  refine RingHom.ext fun a => ?_
  change nsmulAlgHom S (S ⊗[R] A) n ((1 : S) ⊗ₜ[R] a) = (1 : S) ⊗ₜ[R] nsmulAlgHom R A n a
  exact nsmulAlgHom_baseChange_tmul R S A n 1 a

end BaseChange

end PDivisibleGroup.Hopf

namespace PDivisibleGroup

variable {R : Type} [CommRing R] {p h : ℕ} (G : PDivisibleGroup R p h)
  (S : Type) [CommRing S] [Algebra R S]

theorem ker_map_transition (v : ℕ) :
    RingHom.ker (Bialgebra.TensorProduct.map (BialgHom.id S S) (G.transition v)) =
      (RingHom.ker (G.transition v)).map
        (Algebra.TensorProduct.includeRight : G.level (v + 1) →ₐ[R] S ⊗[R] G.level (v + 1)) := by
  have hker : RingHom.ker (Algebra.TensorProduct.map (AlgHom.id R S) (G.transitionAlgHom v)) =
      (RingHom.ker (G.transition v)).map
        (Algebra.TensorProduct.includeRight : G.level (v + 1) →ₐ[R] S ⊗[R] G.level (v + 1)) :=
    Algebra.TensorProduct.lTensor_ker (A := S) (G.transitionAlgHom v) (G.transition_surjective v)
  rw [← hker]
  ext x
  rw [RingHom.mem_ker, RingHom.mem_ker]
  have hmaps : Bialgebra.TensorProduct.map (BialgHom.id S S) (G.transition v) x =
      Algebra.TensorProduct.map (AlgHom.id R S) (G.transitionAlgHom v) x := by
    induction x using TensorProduct.induction_on with
    | zero => simp only [map_zero]
    | tmul s a => rfl
    | add x y hx hy => rw [map_add, map_add, hx, hy]
  rw [hmaps]

variable [Nontrivial S]

def baseChange : PDivisibleGroup S p h where
  level v := S ⊗[R] G.level v
  transition v := Bialgebra.TensorProduct.map (BialgHom.id S S) (G.transition v)
  transition_surjective v :=
    Algebra.TensorProduct.map_surjective (AlgHom.id S S) (G.transitionAlgHom v)
      Function.surjective_id (G.transition_surjective v)
  finrank_level v := by
    haveI : Nontrivial R := (algebraMap R S).domain_nontrivial
    rw [Module.finrank_baseChange, G.finrank_level]
  ker_transition v := by
    rw [ker_map_transition, G.ker_transition, Hopf.torsionIdeal_baseChange]

@[simp] theorem baseChange_level (v : ℕ) : (G.baseChange S).level v = (S ⊗[R] G.level v) := rfl

theorem baseChange_transition (v : ℕ) :
    (G.baseChange S).transition v = Bialgebra.TensorProduct.map (BialgHom.id S S) (G.transition v) :=
  rfl

@[simp] theorem baseChange_transition_tmul (v : ℕ) (s : S) (a : G.level (v + 1)) :
    (G.baseChange S).transition v (s ⊗ₜ[R] a) = s ⊗ₜ[R] G.transition v a := rfl

theorem augIdeal_baseChange (v : ℕ) :
    Hopf.augIdeal S ((G.baseChange S).level v) =
      (Hopf.augIdeal R (G.level v)).map
        (Algebra.TensorProduct.includeRight : G.level v →ₐ[R] S ⊗[R] G.level v) :=
  Hopf.augIdeal_baseChange R S (G.level v)

omit [Nontrivial S] in
theorem augIdeal_le_comap_includeRight (v : ℕ) :
    G.augIdeal v ≤ (Hopf.augIdeal S (S ⊗[R] G.level v)).comap
      (Algebra.TensorProduct.includeRight : G.level v →ₐ[R] S ⊗[R] G.level v) := by
  rw [Hopf.augIdeal_baseChange R S (G.level v)]
  exact Ideal.le_comap_map

theorem baseChange_cotangent_eq (v : ℕ) :
    (G.baseChange S).Cotangent v = (Hopf.augIdeal S (S ⊗[R] G.level v)).Cotangent := rfl

omit [Nontrivial S] in

def cotangentToBaseChange (v : ℕ) :
    G.Cotangent v →ₗ[R] (Hopf.augIdeal S (S ⊗[R] G.level v)).Cotangent :=
  Ideal.mapCotangent (G.augIdeal v) (Hopf.augIdeal S (S ⊗[R] G.level v))
    (Algebra.TensorProduct.includeRight : G.level v →ₐ[R] S ⊗[R] G.level v)
    (G.augIdeal_le_comap_includeRight S v)

omit [Nontrivial S] in
@[simp] theorem cotangentToBaseChange_toCotangent (v : ℕ) (x : G.augIdeal v) :
    G.cotangentToBaseChange S v ((G.augIdeal v).toCotangent x) =
      (Hopf.augIdeal S (S ⊗[R] G.level v)).toCotangent
        ⟨(1 : S) ⊗ₜ[R] (x : G.level v), G.augIdeal_le_comap_includeRight S v x.2⟩ := rfl

omit [Nontrivial S] in

def cotangentBaseChange (v : ℕ) :
    S ⊗[R] G.Cotangent v →ₗ[S] (Hopf.augIdeal S (S ⊗[R] G.level v)).Cotangent :=
  (G.cotangentToBaseChange S v).liftBaseChange S

omit [Nontrivial S] in
@[simp] theorem cotangentBaseChange_tmul (v : ℕ) (s : S) (y : G.Cotangent v) :
    G.cotangentBaseChange S v (s ⊗ₜ[R] y) = s • G.cotangentToBaseChange S v y := by
  rw [cotangentBaseChange, LinearMap.liftBaseChange_tmul]

end PDivisibleGroup

end