TargetAction.lean

def iteratedRadicalTargetAlgHom
    {A : Type u} {S : Type v} [CommRing A] [CommRing S] [Algebra A S] :
    {r : ℕ} → (n : Fin r → ℕ) → (a : Fin r → A) →
      (x : Fin r → S) →
      (∀ i, x i ^ n i = algebraMap A S (a i)) →
      iteratedRadical A r n a →ₐ[A] S
  | 0, _, _, _, _ => Algebra.ofId A S
  | r + 1, n, a, x, hx => by
      let T : CommAlgCat.{u} A :=
        iteratedRadical A r (Fin.init n) (Fin.init a)
      let f : T[X] :=
        X ^ n (Fin.last r) -
          C (algebraMap A T (a (Fin.last r)))
      let prefixMap : T →ₐ[A] S :=
        iteratedRadicalTargetAlgHom
          (Fin.init n) (Fin.init a) (Fin.init x)
          (fun i ↦ hx i.castSucc)
      have hroot : f.eval₂ prefixMap (x (Fin.last r)) = 0 := by
        simp only [f, eval₂_sub, eval₂_pow, eval₂_X, eval₂_C]
        rw [hx (Fin.last r)]
        exact sub_eq_zero.mpr (prefixMap.commutes _).symm
      exact AdjoinRoot.liftAlgHom f prefixMap (x (Fin.last r)) hroot

theorem iteratedRadicalTargetAlgHom_apply_root
    {A : Type u} {S : Type v} [CommRing A] [CommRing S] [Algebra A S]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (x : Fin r → S)
    (hx : ∀ i, x i ^ n i = algebraMap A S (a i))
    (i : Fin r) :
    iteratedRadicalTargetAlgHom n a x hx
        (iteratedRadicalRoot A n a i) = x i

theorem iteratedRadicalTargetAlgHom_injective
    {A : Type u} {S : Type v}
    [CommRing A] [Nontrivial A] [CommRing S] [Algebra A S]
    [FaithfulSMul A S]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    [IsDomain (iteratedRadical A r n a)]
    (x : Fin r → S)
    (hx : ∀ i, x i ^ n i = algebraMap A S (a i)) :
    Function.Injective (iteratedRadicalTargetAlgHom n a x hx)