IsAdjoinRoot.lean

/-
Copyright (c) 2022 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen
-/
module

public import Mathlib.Algebra.Polynomial.AlgebraMap
public import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
public import Mathlib.RingTheory.PowerBasis
public import Mathlib.LinearAlgebra.Charpoly.Basic

/-!
# A predicate on adjoining roots of polynomial

This file defines a predicate `IsAdjoinRoot S f`, which states that the ring `S` can be
constructed by adjoining a specified root of the polynomial `f : R[X]` to `R`.
This predicate is useful when the same ring can be generated by adjoining the root of different
polynomials, and you want to vary which polynomial you're considering.

The results in this file are intended to mirror those in `Mathlib/RingTheory/AdjoinRoot.lean`,
in order to provide an easier way to translate results from one to the other.

## Motivation

`AdjoinRoot` presents one construction of a ring `R[α]`. However, it is possible to obtain
rings of this form in many ways, such as `NumberField.ringOfIntegers ℚ(√-5)`,
or `Algebra.adjoin R {α, α^2}`, or `IntermediateField.adjoin R {α, 2 - α}`,
or even if we want to view `ℂ` as adjoining a root of `X^2 + 1` to `ℝ`.

## Main definitions

The two main predicates in this file are:

* `IsAdjoinRoot S f`: `S` is generated by adjoining a specified root of `f : R[X]` to `R`
* `IsAdjoinRootMonic S f`: `S` is generated by adjoining a root of the monic polynomial
  `f : R[X]` to `R`

Using `IsAdjoinRoot` to map into `S`:

* `IsAdjoinRoot.map`: inclusion from `R[X]` to `S`
* `IsAdjoinRoot.root`: the specific root adjoined to `R` to give `S`

Using `IsAdjoinRoot` to map out of `S`:

* `IsAdjoinRoot.repr`: choose a non-unique representative in `R[X]`
* `IsAdjoinRoot.lift`, `IsAdjoinRoot.liftHom`: lift a morphism `R →+* T` to `S →+* T`
* `IsAdjoinRootMonic.modByMonicHom`: a unique representative in `R[X]` if `f` is monic

## Main results

* `AdjoinRoot.isAdjoinRoot` and `AdjoinRoot.isAdjoinRootMonic`:
  `AdjoinRoot` satisfies the conditions on `IsAdjoinRoot`(`Monic`)
* `IsAdjoinRootMonic.powerBasis`: the `root` generates a power basis on `S` over `R`
* `IsAdjoinRoot.algEquiv`: algebra isomorphism showing adjoining a root gives a unique ring
  up to isomorphism
* `IsAdjoinRoot.ofAlgEquiv`: transfer `IsAdjoinRoot` across an algebra isomorphism
* `IsAdjoinRootMonic.minpoly_eq`: the minimal polynomial of the adjoined root of `f` is equal to
  `f`, if `f` is irreducible and monic, and `R` is a GCD domain
-/

@[expose] public section

open Module Polynomial

noncomputable section

universe u v

-- This class doesn't really make sense on a predicate
/-- `IsAdjoinRoot S f` states that the ring `S` can be constructed by adjoining a specified root
of the polynomial `f : R[X]` to `R`.

Compare `PowerBasis R S`, which does not explicitly specify which polynomial we adjoin a root of
(in particular `f` does not need to be the minimal polynomial of the root we adjoin),
and `AdjoinRoot` which constructs a new type.

This is not a typeclass because the choice of root given `S` and `f` is not unique.
-/
structure IsAdjoinRoot {R : Type u} (S : Type v) [CommSemiring R] [Semiring S] [Algebra R S]
    (f : R[X]) : Type max u v where
  map : R[X] →ₐ[R] S
  map_surjective : Function.Surjective map
  ker_map : RingHom.ker map = Ideal.span {f}

-- This class doesn't really make sense on a predicate
/-- `IsAdjoinRootMonic S f` states that the ring `S` can be constructed by adjoining a specified
root of the monic polynomial `f : R[X]` to `R`.

As long as `f` is monic, there is a well-defined representation of elements of `S` as polynomials
in `R[X]` of degree lower than `deg f` (see `modByMonicHom` and `coeff`). In particular,
we have `IsAdjoinRootMonic.powerBasis`.

Bundling `Monic` into this structure is very useful when working with explicit `f`s such as
`X^2 - C a * X - C b` since it saves you carrying around the proofs of monicity.
-/
structure IsAdjoinRootMonic {R : Type u} (S : Type v) [CommSemiring R] [Semiring S] [Algebra R S]
    (f : R[X]) extends IsAdjoinRoot S f where
  monic : Monic f

section Ring

variable {R : Type u} {S : Type v} [CommRing R] [Ring S] {f : R[X]} [Algebra R S]

namespace IsAdjoinRoot

variable (h : IsAdjoinRoot S f)

/-- `(h : IsAdjoinRoot S f).root` is the root of `f` that can be adjoined to generate `S`. -/
def root : S := h.map X

theorem algebraMap_apply (x : R) :
    algebraMap R S x = h.map (Polynomial.C x) := AlgHom.algebraMap_eq_apply h.map rfl

theorem mem_ker_map {p} : p ∈ RingHom.ker h.map ↔ f ∣ p := by
  rw [h.ker_map, Ideal.mem_span_singleton]

@[simp]
theorem map_eq_zero_iff {p} : h.map p = 0 ↔ f ∣ p := by simpa using h.mem_ker_map

@[simp]
theorem map_X : h.map X = h.root := rfl

@[simp]
theorem map_self : h.map f = 0 := by simp

@[simp]
theorem aeval_root_eq_map : aeval h.root = h.map := by ext; simp

theorem aeval_root_self : aeval h.root f = 0 := by simp

theorem adjoin_root_eq_top : Algebra.adjoin R {h.root} = ⊤ := by
  rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top, aeval_root_eq_map]
  exact h.map_surjective

/-- Extensionality of the `IsAdjoinRoot` structure itself. See `IsAdjoinRootMonic.ext_elem`
for extensionality of the ring elements. -/
theorem ext_map (h' : IsAdjoinRoot S f) (eq : ∀ x, h.map x = h'.map x) : h = h' := by
  cases h; cases h'; congr
  exact AlgHom.ext eq

/-- Extensionality of the `IsAdjoinRoot` structure itself. See `IsAdjoinRootMonic.ext_elem`
for extensionality of the ring elements. -/
@[ext]
theorem ext (h' : IsAdjoinRoot S f) (eq : h.root = h'.root) : h = h' :=
  h.ext_map h' (fun x => by rw [← h.aeval_root_eq_map, ← h'.aeval_root_eq_map, eq])

/-- Choose an arbitrary representative so that `h.map (h.repr x) = x`.

If `f` is monic, use `IsAdjoinRootMonic.modByMonicHom` for a unique choice of representative.
-/
def repr (x : S) : R[X] := (h.map_surjective x).choose

@[simp]
theorem map_repr (x : S) : h.map (h.repr x) = x := (h.map_surjective x).choose_spec

/-- `repr` preserves zero, up to multiples of `f` -/
theorem repr_zero_mem_span : h.repr 0 ∈ Ideal.span ({f} : Set R[X]) := by simp [← h.ker_map]

/-- `repr` preserves addition, up to multiples of `f` -/
theorem repr_add_sub_repr_add_repr_mem_span (x y : S) :
    h.repr (x + y) - (h.repr x + h.repr y) ∈ Ideal.span ({f} : Set R[X]) := by simp [← h.ker_map]

section Equiv

variable {T : Type*} [Ring T] [Algebra R T]

/-- Algebra isomorphism with `R[X]/(f)`. -/
def adjoinRootAlgEquiv : AdjoinRoot f ≃ₐ[R] S :=
  (Ideal.quotientEquivAlgOfEq R h.ker_map.symm).trans <|
    Ideal.quotientKerAlgEquivOfSurjective h.map_surjective

@[simp]
theorem adjoinRootAlgEquiv_apply_mk (g : R[X]) :
    h.adjoinRootAlgEquiv (AdjoinRoot.mk f g) = h.map g := rfl

theorem adjoinRootAlgEquiv_apply_eq_map (a : AdjoinRoot f) :
    h.adjoinRootAlgEquiv a = h.map (AdjoinRoot.mk_surjective a).choose := by
  rw (occs := [1]) [← (AdjoinRoot.mk_surjective a).choose_spec, adjoinRootAlgEquiv_apply_mk]

theorem adjoinRootAlgEquiv_symm_apply_eq_mk (a : S) :
    h.adjoinRootAlgEquiv.symm a = AdjoinRoot.mk f (h.repr a) := by
  rw (occs := [1]) [AlgEquiv.symm_apply_eq, ← h.map_repr a, adjoinRootAlgEquiv_apply_mk]

@[simp]
theorem adjoinRootAlgEquiv_apply_root : h.adjoinRootAlgEquiv (AdjoinRoot.root f) = h.root := rfl

@[simp]
theorem adjoinRootAlgEquiv_symm_apply_root : h.adjoinRootAlgEquiv.symm h.root = AdjoinRoot.root f :=
  (AlgEquiv.symm_apply_eq h.adjoinRootAlgEquiv).mpr rfl

variable (h' : IsAdjoinRoot T f)

/-- Adjoining a root gives a unique algebra up to isomorphism.

This is the converse of `IsAdjoinRoot.ofAlgEquiv`: this turns an `IsAdjoinRoot` into an
`AlgEquiv`, and `IsAdjoinRoot.ofAlgEquiv` turns an `AlgEquiv` into an `IsAdjoinRoot`.
-/
def algEquiv : S ≃ₐ[R] T := h.adjoinRootAlgEquiv.symm.trans h'.adjoinRootAlgEquiv

theorem algEquiv_def : h.algEquiv h' = h.adjoinRootAlgEquiv.symm.trans h'.adjoinRootAlgEquiv := rfl

@[simp]
theorem algEquiv_root : h.algEquiv h' h.root = h'.root := by simp [algEquiv_def]

@[simp]
theorem algEquiv_map : AlgHom.comp (h.algEquiv h') h.map = h'.map := by
  ext; simp

@[simp]
theorem algEquiv_apply_map (z : R[X]) : h.algEquiv h' (h.map z) = h'.map z := by
  rw [← h.algEquiv_map h']; simp [-algEquiv_map]

@[simp] theorem algEquiv_self : h.algEquiv h = AlgEquiv.refl := by ext; simp [algEquiv_def]

@[simp] theorem algEquiv_symm : (h.algEquiv h').symm = h'.algEquiv h := rfl

@[simp]
theorem algEquiv_algEquiv {U : Type*} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f) (x) :
    (h'.algEquiv h'') (h.algEquiv h' x) = h.algEquiv h'' x := by simp [algEquiv_def]

@[simp]
theorem algEquiv_trans {U : Type*} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f) :
    (h.algEquiv h').trans (h'.algEquiv h'') = h.algEquiv h'' := by ext; simp

/-- Transfer `IsAdjoinRoot` across an algebra isomorphism.

This is the converse of `IsAdjoinRoot.algEquiv`: this turns an `AlgEquiv` into an `IsAdjoinRoot`,
and `IsAdjoinRoot.algEquiv` turns an `IsAdjoinRoot` into an `AlgEquiv`.
-/
@[simps! map_apply]
def ofAlgEquiv (e : S ≃ₐ[R] T) : IsAdjoinRoot T f where
  map := (e : S →ₐ[R] T).comp h.map
  map_surjective := e.surjective.comp h.map_surjective
  ker_map := by ext; simp [Ideal.mem_span_singleton]

@[simp] theorem ofAlgEquiv_root (e : S ≃ₐ[R] T) : (h.ofAlgEquiv e).root = e h.root := rfl

@[simp]
theorem algEquiv_ofAlgEquiv {U : Type*} [Ring U] [Algebra R U] (e : T ≃ₐ[R] U) :
    h.algEquiv (h'.ofAlgEquiv e) = (h.algEquiv h').trans e := by
  ext a
  simp [algEquiv_def, AlgEquiv.trans_apply, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply]

@[simp]
theorem ofAlgEquiv_algEquiv {U : Type*} [Ring U] [Algebra R U] (h'' : IsAdjoinRoot U f)
    (e : S ≃ₐ[R] T) : (h.ofAlgEquiv e).algEquiv h'' = e.symm.trans (h.algEquiv h'') := by
  ext a
  simp_rw [algEquiv_def, AlgEquiv.trans_apply, EmbeddingLike.apply_eq_iff_eq,
           AlgEquiv.symm_apply_eq, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply,
           ← adjoinRootAlgEquiv_apply_eq_map, AlgEquiv.apply_symm_apply]

end Equiv

section lift

variable {T : Type*} [CommRing T] {i : R →+* T} {x : T}

section
variable (hx : f.eval₂ i x = 0)
include hx

/-- Auxiliary lemma for `IsAdjoinRoot.lift` -/
theorem eval₂_repr_eq_eval₂_of_map_eq (z : S) (w : R[X])
    (hzw : h.map w = z) : (h.repr z).eval₂ i x = w.eval₂ i x := by
  rw [eq_comm, ← sub_eq_zero, ← h.map_repr z, ← map_sub, h.map_eq_zero_iff] at hzw
  obtain ⟨y, hy⟩ := hzw
  rw [← sub_eq_zero, ← eval₂_sub, hy, eval₂_mul, hx, zero_mul]

variable (i x)

-- To match `AdjoinRoot.lift`
/-- Lift a ring homomorphism `R →+* T` to `S →+* T` by specifying a root `x` of `f` in `T`,
where `S` is given by adjoining a root of `f` to `R`. -/
def lift (hx : f.eval₂ i x = 0) : S →+* T where
  toFun z := (h.repr z).eval₂ i x
  map_zero' := by simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ (map_zero _)]
  map_add' z w := by simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ (h.repr z + h.repr w)]
  map_one' := by simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ (map_one _)]
  map_mul' z w := by simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ (h.repr z * h.repr w)]

variable {i x}

@[simp]
theorem lift_map (z : R[X]) : h.lift i x hx (h.map z) = z.eval₂ i x := by
  simp [lift, h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ rfl]

@[simp]
theorem lift_root : h.lift i x hx h.root = x := by
  rw [← h.map_X, lift_map, eval₂_X]

@[simp]
theorem lift_algebraMap (a : R) : h.lift i x hx (algebraMap R S a) = i a := by
  simp [h.algebraMap_apply]

/-- Auxiliary lemma for `apply_eq_lift` -/
theorem apply_eq_lift (g : S →+* T) (hmap : ∀ a, g (algebraMap R S a) = i a)
    (hroot : g h.root = x) (a : S) : g a = h.lift i x hx a := by
  rw [← h.map_repr a, Polynomial.as_sum_range_C_mul_X_pow (h.repr a)]
  simp [← h.algebraMap_apply, *]

/-- Unicity of `lift`: a map that agrees on `R` and `h.root` agrees with `lift` everywhere. -/
theorem eq_lift (g : S →+* T) (hmap : ∀ a, g (algebraMap R S a) = i a) (hroot : g h.root = x) :
    g = h.lift i x hx := RingHom.ext (h.apply_eq_lift hx g hmap hroot)

end

variable [Algebra R T] (hx' : aeval x f = 0)

variable (x) in
-- To match `AdjoinRoot.liftHom`
/-- Lift the algebra map `R → T` to `S →ₐ[R] T` by specifying a root `x` of `f` in `T`,
where `S` is given by adjoining a root of `f` to `R`. -/
def liftHom : S →ₐ[R] T :=
  { h.lift (algebraMap R T) x hx' with commutes' a := h.lift_algebraMap hx' a }

@[simp]
theorem coe_liftHom : (h.liftHom x hx' : S →+* T) = h.lift (algebraMap R T) x hx' := rfl

theorem lift_algebraMap_apply (z : S) : h.lift (algebraMap R T) x hx' z = h.liftHom x hx' z := rfl

@[simp]
theorem liftHom_map (z : R[X]) : h.liftHom x hx' (h.map z) = aeval x z := by
  rw [← lift_algebraMap_apply, lift_map, aeval_def]

@[simp]
theorem liftHom_root : h.liftHom x hx' h.root = x := by rw [← lift_algebraMap_apply, lift_root]

/-- Unicity of `liftHom`: a map that agrees on `h.root` agrees with `liftHom` everywhere. -/
theorem eq_liftHom (g : S →ₐ[R] T) (hroot : g h.root = x) : g = h.liftHom x hx' :=
  AlgHom.ext (h.apply_eq_lift hx' g g.commutes hroot)

end lift

theorem isAlgebraic_root (hf : f ≠ 0) : IsAlgebraic R h.root := ⟨f, by simp [hf]⟩

end IsAdjoinRoot

namespace AdjoinRoot

variable (f)

/-- `AdjoinRoot f` is indeed given by adjoining a root of `f`. -/
protected def isAdjoinRoot : IsAdjoinRoot (AdjoinRoot f) f where
  map := AdjoinRoot.mkₐ f
  map_surjective := Ideal.Quotient.mkₐ_surjective _ _
  ker_map := by ext; simp [Ideal.mem_span_singleton]

/-- `AdjoinRoot f` is indeed given by adjoining a root of `f`. If `f` is monic this is more
powerful than `AdjoinRoot.isAdjoinRoot`. -/
protected def isAdjoinRootMonic (hf : Monic f) : IsAdjoinRootMonic (AdjoinRoot f) f where
  __ := AdjoinRoot.isAdjoinRoot f
  monic := hf

@[simp]
theorem isAdjoinRootMonic_toAdjoinRoot (hf : Monic f) :
    (AdjoinRoot.isAdjoinRootMonic f hf).toIsAdjoinRoot = AdjoinRoot.isAdjoinRoot f := rfl

theorem isAdjoinRoot_map_eq_mkₐ : (AdjoinRoot.isAdjoinRoot f).map = AdjoinRoot.mkₐ f := rfl

@[simp]
theorem isAdjoinRoot_root_eq_root : (AdjoinRoot.isAdjoinRoot f).root = AdjoinRoot.root f := by
  simp [AdjoinRoot.isAdjoinRoot, IsAdjoinRoot.root]

end AdjoinRoot

/-- If `S` is `R`-isomorphic to `R[X]/(f)`, then `S` is given by adjoining a root of `f`. -/
abbrev IsAdjoinRoot.ofAdjoinRootEquiv (e : AdjoinRoot f ≃ₐ[R] S) : IsAdjoinRoot S f :=
  ofAlgEquiv (AdjoinRoot.isAdjoinRoot f) e

namespace IsAdjoinRootMonic

variable (h : IsAdjoinRootMonic S f)

open IsAdjoinRoot

theorem map_modByMonic (g : R[X]) : h.map (g %ₘ f) = h.map g := by
  rw [← RingHom.sub_mem_ker_iff, mem_ker_map, modByMonic_eq_sub_mul_div, sub_right_comm,
    sub_self, zero_sub, dvd_neg]
  exact ⟨_, rfl⟩

theorem modByMonic_repr_map (g : R[X]) : h.repr (h.map g) %ₘ f = g %ₘ f :=
  modByMonic_eq_of_dvd_sub h.monic <| by rw [← h.mem_ker_map, RingHom.sub_mem_ker_iff, map_repr]

/-- `IsAdjoinRoot.modByMonicHom` sends the equivalence class of `f` mod `g` to `f %ₘ g`. -/
def modByMonicHom : S →ₗ[R] R[X] where
  toFun x := h.repr x %ₘ f
  map_add' x y := by
    conv_lhs =>
      rw [← h.map_repr x, ← h.map_repr y, ← map_add, h.modByMonic_repr_map, add_modByMonic]
  map_smul' c x := by
    rw [RingHom.id_apply, ← h.map_repr x, Algebra.smul_def, h.algebraMap_apply, ← map_mul,
        h.modByMonic_repr_map, ← smul_eq_C_mul, smul_modByMonic, h.map_repr]

@[simp]
theorem modByMonicHom_map (g : R[X]) : h.modByMonicHom (h.map g) = g %ₘ f :=
  h.modByMonic_repr_map g

@[simp]
theorem map_modByMonicHom (x : S) : h.map (h.modByMonicHom x) = x := by
  simp [modByMonicHom, map_modByMonic, map_repr]

@[simp]
theorem modByMonicHom_root_pow {n : ℕ} (hdeg : n < natDegree f) :
    h.modByMonicHom (h.root ^ n) = X ^ n := by
  nontriviality R
  rw [← h.map_X, ← map_pow, modByMonicHom_map, modByMonic_eq_self_iff h.monic, degree_X_pow]
  contrapose! hdeg
  simpa [natDegree_le_iff_degree_le] using hdeg

@[simp]
theorem modByMonicHom_root (hdeg : 1 < natDegree f) : h.modByMonicHom h.root = X := by
  simpa using modByMonicHom_root_pow h hdeg

/-- The basis on `S` generated by powers of `h.root`.

Auxiliary definition for `IsAdjoinRootMonic.powerBasis`. -/
def basis : Basis (Fin (natDegree f)) R S where
  repr.toFun x := (h.modByMonicHom x).toFinsupp.coeff.comapDomain _ Fin.val_injective.injOn
  repr.invFun g := h.map <| ofFinsupp <| .ofCoeff <| g.mapDomain Fin.val
  repr.left_inv x := by
    nontriviality R using Algebra.subsingleton R S
    simp only [AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff]
    rw [Finsupp.mapDomain_comapDomain, Polynomial.eta, h.map_modByMonicHom x]
    · exact Fin.val_injective
    intro i hi
    refine Set.mem_range.mpr ⟨⟨i, ?_⟩, rfl⟩
    contrapose! hi
    simp only [Polynomial.toFinsupp_apply, Classical.not_not, Finsupp.mem_support_iff, Ne,
      modByMonicHom, LinearMap.coe_mk, Finset.mem_coe]
    obtain rfl | hf := eq_or_ne f 1
    · simp
    · exact coeff_eq_zero_of_natDegree_lt <| (natDegree_modByMonic_lt _ h.monic hf).trans_le hi
  repr.right_inv g := by
    nontriviality R
    ext i
    simp only [AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff, h.modByMonicHom_map,
      Finsupp.comapDomain_apply, Polynomial.toFinsupp_apply]
    rw [(Polynomial.modByMonic_eq_self_iff h.monic).mpr, Polynomial.coeff]
    · rw [Finsupp.mapDomain_apply Fin.val_injective]
    rw [degree_eq_natDegree h.monic.ne_zero, degree_lt_iff_coeff_zero]
    intro m hm
    rw [Polynomial.coeff]
    rw [Finsupp.mapDomain_notin_range]
    rw [Set.mem_range, not_exists]
    rintro i rfl
    exact i.prop.not_ge hm
  repr.map_add' := by simp [Finsupp.comapDomain_add_of_injective Fin.val_injective]
  repr.map_smul' := by simp [Finsupp.comapDomain_smul_of_injective Fin.val_injective]

@[simp]
theorem basis_apply (i) : h.basis i = h.root ^ (i : ℕ) :=
  Basis.apply_eq_iff.mpr <| by
    simp [AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff, IsAdjoinRootMonic.basis]

include h in
theorem deg_pos [Nontrivial S] : 0 < natDegree f := by
  rcases h.basis.index_nonempty with ⟨⟨i, hi⟩⟩
  exact Nat.zero_lt_of_lt hi

include h in
theorem deg_ne_zero [Nontrivial S] : natDegree f ≠ 0 := h.deg_pos.ne'

/-- If `f` is monic, the powers of `h.root` form a basis. -/
@[simps! gen dim basis]
def powerBasis : PowerBasis R S where
  gen := h.root
  dim := natDegree f
  basis := h.basis
  basis_eq_pow := h.basis_apply

@[simp]
theorem basis_repr (x : S) (i : Fin (natDegree f)) :
    h.basis.repr x i = (h.modByMonicHom x).coeff (i : ℕ) := by
  simp [IsAdjoinRootMonic.basis, AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff, toFinsupp_apply]

theorem basis_one (hdeg : 1 < natDegree f) : h.basis ⟨1, hdeg⟩ = h.root := by
  rw [h.basis_apply, Fin.val_mk, pow_one]

include h in
theorem finite : Module.Finite R S := (powerBasis h).finite

include h in
theorem finrank [StrongRankCondition R] : Module.finrank R S = f.natDegree :=
  (powerBasis h).finrank

/--
See `finrank_quotient_span_eq_natDegree` for a more general version over a field.
-/
theorem _root_.finrank_quotient_span_eq_natDegree' [StrongRankCondition R] (hf : f.Monic) :
    Module.finrank R (R[X] ⧸ Ideal.span {f}) = f.natDegree :=
  (AdjoinRoot.isAdjoinRootMonic _ hf).finrank

/-- `IsAdjoinRootMonic.liftPolyₗ` lifts a linear map on polynomials to a linear map on `S`. -/
@[simps!]
def liftPolyₗ {T : Type*} [AddCommGroup T] [Module R T] (g : R[X] →ₗ[R] T) : S →ₗ[R] T :=
  g.comp h.modByMonicHom

/-- `IsAdjoinRootMonic.coeff h x i` is the `i`th coefficient of the representative of `x : S`.
-/
def coeff : S →ₗ[R] ℕ → R :=
  h.liftPolyₗ
    { toFun := Polynomial.coeff
      map_add' p q := funext (Polynomial.coeff_add p q)
      map_smul' c p := funext (Polynomial.coeff_smul c p) }

theorem coeff_apply_lt (z : S) (i : ℕ) (hi : i < natDegree f) :
    h.coeff z i = h.basis.repr z ⟨i, hi⟩ := by
  simp [coeff]

theorem coeff_apply_coe (z : S) (i : Fin (natDegree f)) : h.coeff z i = h.basis.repr z i :=
  h.coeff_apply_lt z i i.prop

theorem coeff_apply_le (z : S) (i : ℕ) (hi : natDegree f ≤ i) : h.coeff z i = 0 := by
  simp only [coeff, liftPolyₗ_apply, LinearMap.coe_mk, AddHom.coe_mk]
  nontriviality R
  exact
    Polynomial.coeff_eq_zero_of_degree_lt
      ((degree_modByMonic_lt _ h.monic).trans_le (Polynomial.degree_le_of_natDegree_le hi))

theorem coeff_apply (z : S) (i : ℕ) :
    h.coeff z i = if hi : i < natDegree f then h.basis.repr z ⟨i, hi⟩ else 0 := by
  split_ifs with hi
  · exact h.coeff_apply_lt z i hi
  · exact h.coeff_apply_le z i (le_of_not_gt hi)

theorem coeff_root_pow {n} (hn : n < natDegree f) : h.coeff (h.root ^ n) = Pi.single n 1 := by
  ext i
  rw [coeff_apply]
  split_ifs with hi
  · calc
      h.basis.repr (h.root ^ n) ⟨i, _⟩ = h.basis.repr (h.basis ⟨n, hn⟩) ⟨i, hi⟩ := by
        rw [h.basis_apply, Fin.val_mk]
      _ = Pi.single (M := fun _ => R) ((⟨n, hn⟩ : Fin _) : ℕ) (1 : (fun _ => R) n)
        ↑(⟨i, _⟩ : Fin _) := by
        rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]
      _ = Pi.single (M := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_mk]
  · rw [Pi.single_eq_of_ne]
    rintro rfl
    simp [hi] at hn

theorem coeff_one [Nontrivial S] : h.coeff 1 = Pi.single 0 1 := by
  rw [← h.coeff_root_pow h.deg_pos, pow_zero]

theorem coeff_root (hdeg : 1 < natDegree f) : h.coeff h.root = Pi.single 1 1 := by
  rw [← h.coeff_root_pow hdeg, pow_one]

theorem coeff_algebraMap [Nontrivial S] (x : R) : h.coeff (algebraMap R S x) = Pi.single 0 x := by
  ext i
  rw [Algebra.algebraMap_eq_smul_one, map_smul, coeff_one, Pi.smul_apply, smul_eq_mul]
  refine (Pi.apply_single (fun _ y => x * y) ?_ 0 1 i).trans (by simp)
  simp

theorem ext_elem ⦃x y : S⦄ (hxy : ∀ i < natDegree f, h.coeff x i = h.coeff y i) : x = y :=
  EquivLike.injective h.basis.equivFun <|
    funext fun i => by
      rw [Basis.equivFun_apply, ← h.coeff_apply_coe, Basis.equivFun_apply, ← h.coeff_apply_coe,
        hxy i i.prop]

theorem ext_elem_iff {x y : S} : x = y ↔ ∀ i < natDegree f, h.coeff x i = h.coeff y i :=
  ⟨fun hxy _ _=> hxy ▸ rfl, fun hxy => h.ext_elem hxy⟩

theorem coeff_injective : Function.Injective h.coeff := fun _ _ hxy =>
  h.ext_elem fun _ _ => hxy ▸ rfl

theorem isIntegral_root : IsIntegral R h.root := ⟨f, h.monic, h.aeval_root_self⟩

end IsAdjoinRootMonic

end Ring

section CommRing

variable {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {f : R[X]}

namespace IsAdjoinRoot

variable (h : IsAdjoinRoot S f)

section lift

@[simp]
theorem lift_self_apply (x : S) : h.lift (algebraMap R S) h.root h.aeval_root_self x = x := by
  rw [← h.map_repr x, lift_map, ← aeval_def, h.aeval_root_eq_map]

theorem lift_self : h.lift (algebraMap R S) h.root h.aeval_root_self = RingHom.id S :=
  RingHom.ext h.lift_self_apply

end lift

section mkOfAdjoinEqTop

variable [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyClosed R]
    {α : S} (hα : IsIntegral R α) (hα₂ : Algebra.adjoin R {α} = ⊤)

/-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
@[simps]
def mkOfAdjoinEqTop : IsAdjoinRoot S (minpoly R α) where
  map := aeval α
  map_surjective := by
    rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← Algebra.adjoin_singleton_eq_range_aeval,
      hα₂, Algebra.coe_top]
  ker_map := by
    ext
    simpa [Ideal.mem_span_singleton] using minpoly.isIntegrallyClosed_dvd_iff hα _

/-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
abbrev _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop : IsAdjoinRootMonic S (minpoly R α) where
  __ := IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂
  monic := minpoly.monic hα

@[simp]
theorem mkOfAdjoinEqTop_root : (IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂).root = α := by
  simp [IsAdjoinRoot.root]

end mkOfAdjoinEqTop

section Equiv

variable {T : Type*} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type*} [CommRing U]

@[simp]
theorem lift_algEquiv (i : R →+* U) (x hx z) :
    h'.lift i x hx (h.algEquiv h' z) = h.lift i x hx z := by rw [← h.map_repr z]; simp [-map_repr]

@[simp]
theorem liftHom_algEquiv [Algebra R U] (x : U) (hx z) :
    h'.liftHom x hx (h.algEquiv h' z) = h.liftHom x hx z := h.lift_algEquiv h' _ _ hx _

end Equiv

end IsAdjoinRoot

namespace IsAdjoinRootMonic

variable (h : IsAdjoinRootMonic S f)

theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyClosed R]
  (hirr : Irreducible f) : minpoly R h.root = f :=
  let ⟨q, hq⟩ := minpoly.isIntegrallyClosed_dvd h.isIntegral_root h.aeval_root_self
  symm <|
    eq_of_monic_of_associated h.monic (minpoly.monic h.isIntegral_root) <| by
      convert
        Associated.mul_left (minpoly R h.root) <|
          associated_one_iff_isUnit.2 <|
            (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
      rw [mul_one]

/-- If `α` generates `S` as an algebra and `S` is free and finite,
then `S` is given by adjoining a root of `minpoly R α`.
Does not require that `R` is an integral domain, unlike `mkOfAdjoinEqTop`. -/
@[simps]
def mkOfAdjoinEqTop'
    [Module.Finite R S] [Module.Free R S]
    {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
    IsAdjoinRootMonic S (minpoly R α) where
  __ : IsAdjoinRoot S (minpoly R α) :=
    let f := minpoly R α
    have hf := minpoly.monic (Algebra.IsIntegral.isIntegral (R := R) α)
    let φ : AdjoinRoot f →ₐ[R] S :=
      AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α (minpoly.aeval R α)
    IsAdjoinRoot.ofAdjoinRootEquiv <| AlgEquiv.ofBijective φ <| by
      have hφ : Function.Surjective φ := by
        rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
        intro s; obtain ⟨p, hp⟩ := hα s
        exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
      haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
      by_cases h : Nontrivial R
      · letI e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S <|
          le_antisymm (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le α)
          (LinearMap.finrank_le_finrank_of_surjective (f := φ.toLinearMap) hφ)
        exact OrzechProperty.bijective_of_surjective_of_injective
          e.toLinearMap φ e.injective hφ
      · apply not_nontrivial_iff_subsingleton.mp at h
        haveI := Module.subsingleton R (AdjoinRoot f)
        exact ⟨Function.injective_of_subsingleton φ, hφ⟩
  map := aeval α
  monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)

@[simp]
theorem mkOfAdjoinEqTop'_root
    [Module.Finite R S] [Module.Free R S]
    {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
      (mkOfAdjoinEqTop' hα).root = α := by
  simp [IsAdjoinRoot.root]

end IsAdjoinRootMonic

section Algebra

open AdjoinRoot IsAdjoinRoot minpoly PowerBasis IsAdjoinRootMonic Algebra

theorem Algebra.adjoin.powerBasis'_minpoly_gen [IsDomain R] [IsDomain S] [IsTorsionFree R S]
    [IsIntegrallyClosed R] {x : S} (hx' : IsIntegral R x) :
    minpoly R x = minpoly R (Algebra.adjoin.powerBasis' hx').gen := by
  have := isDomain_of_prime (prime_of_isIntegrallyClosed hx')
  have :=
    noZeroSMulDivisors_of_prime_of_degree_ne_zero (prime_of_isIntegrallyClosed hx')
      (degree_pos hx').ne'
  rw [← minpolyGen_eq, adjoin.powerBasis', minpolyGen_map, minpolyGen_eq,
    AdjoinRoot.powerBasis'_gen, ← isAdjoinRoot_root_eq_root _,
    ← isAdjoinRootMonic_toAdjoinRoot _ (monic hx'),
    minpoly_eq (AdjoinRoot.isAdjoinRootMonic _ (monic hx')) (irreducible hx')]

end Algebra

end CommRing

section Field

open scoped IntermediateField

variable {F E : Type*} [Field F] [Field E] [Algebra F E] {f : F[X]}

namespace IsAdjoinRoot

theorem primitive_element_root (h : IsAdjoinRoot E f) : F⟮h.root⟯ = ⊤ :=
  IntermediateField.adjoin_eq_top_of_algebra F {h.root} (adjoin_root_eq_top h)

/-- If `α` is primitive in `E/f`, then `E` is given by adjoining a root of `minpoly F α`. -/
abbrev mkOfPrimitiveElement {α : E} (hα : IsIntegral F α) (hα₂ : F⟮α⟯ = ⊤) :
    IsAdjoinRoot E (minpoly F α) :=
  mkOfAdjoinEqTop hα (Algebra.adjoin_eq_top_of_primitive_element hα.isAlgebraic hα₂)

/-- If `α` is primitive in `E/f`, then `E` is given by adjoining a root of `minpoly F α`. -/
abbrev _root_.IsAdjoinRootMonic.mkOfPrimitiveElement
    {α : E} (hα : IsIntegral F α) (hα₂ : F⟮α⟯ = ⊤) : IsAdjoinRootMonic E (minpoly F α) where
  __ := IsAdjoinRoot.mkOfPrimitiveElement hα hα₂
  monic := minpoly.monic hα

end IsAdjoinRoot

end Field