chore: redefine AlgebraicClosure to make certain instance diagrams co…

…mmute (#6734)

A similar trick to the trick used in #4891 makes all the required type class diagrams commute.

I also added instances for `CharP` and `CharZero` and tests for the instance diagrams.



Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

@@ -297,28 +297,31 @@ instance toStepOfLE.directedSystem : DirectedSystem (Step k) fun i j h => toStep
 
 end AlgebraicClosure
 
-/-- The canonical algebraic closure of a field, the direct limit of adding roots to the field for
-each polynomial over the field. -/
-def AlgebraicClosure : Type u :=
+/-- Auxiliary construction for `AlgebraicClosure`. Although `AlgebraicClosureAux` does define
+the algebraic closure of a field, it is redefined at `AlgebraicClosure` in order to make sure
+certain instance diamonds commute by definition.
+-/
+def AlgebraicClosureAux [Field k] : Type u :=
   Ring.DirectLimit (AlgebraicClosure.Step k) fun i j h => AlgebraicClosure.toStepOfLE k i j h
-#align algebraic_closure AlgebraicClosure
+#align algebraic_closure AlgebraicClosureAux
 
-namespace AlgebraicClosure
+namespace AlgebraicClosureAux
 
-instance : Field (AlgebraicClosure k) :=
+open AlgebraicClosure
+
+/-- `AlgebraicClosureAux k` is a `Field` -/
+local instance field : Field (AlgebraicClosureAux k) :=
   Field.DirectLimit.field _ _
 
-instance : Inhabited (AlgebraicClosure k) :=
+instance : Inhabited (AlgebraicClosureAux k) :=
   ⟨37⟩
 
 /-- The canonical ring embedding from the `n`th step to the algebraic closure. -/
-def ofStep (n : ℕ) : Step k n →+* AlgebraicClosure k :=
+def ofStep (n : ℕ) : Step k n →+* AlgebraicClosureAux k :=
   Ring.DirectLimit.of _ _ _
-#align algebraic_closure.of_step AlgebraicClosure.ofStep
+#noalign algebraic_closure.of_step
 
-instance algebraOfStep (n) : Algebra (Step k n) (AlgebraicClosure k) :=
-  (ofStep k n).toAlgebra
-#align algebraic_closure.algebra_of_step AlgebraicClosure.algebraOfStep
+#noalign algebraic_closure.algebra_of_step
 
 theorem ofStep_succ (n : ℕ) : (ofStep k (n + 1)).comp (toStepSucc k n) = ofStep k n := by
   ext x
@@ -336,14 +339,14 @@ theorem ofStep_succ (n : ℕ) : (ofStep k (n + 1)).comp (toStepSucc k n) = ofSte
   -- RingHom.ext fun x =>
   --   show Ring.DirectLimit.of (Step k) (fun i j h => toStepOfLE k i j h) _ _ = _ by
   --     convert Ring.DirectLimit.of_f n.le_succ x; ext x; exact (Nat.leRecOn_succ' x).symm
-#align algebraic_closure.of_step_succ AlgebraicClosure.ofStep_succ
+#noalign algebraic_closure.of_step_succ
 
-theorem exists_ofStep (z : AlgebraicClosure k) : ∃ n x, ofStep k n x = z :=
+theorem exists_ofStep (z : AlgebraicClosureAux k) : ∃ n x, ofStep k n x = z :=
   Ring.DirectLimit.exists_of z
-#align algebraic_closure.exists_of_step AlgebraicClosure.exists_ofStep
+#noalign algebraic_closure.exists_of_step
 
-theorem exists_root {f : Polynomial (AlgebraicClosure k)} (hfm : f.Monic) (hfi : Irreducible f) :
-    ∃ x : AlgebraicClosure k, f.eval x = 0 := by
+theorem exists_root {f : Polynomial (AlgebraicClosureAux k)}
+    (hfm : f.Monic) (hfi : Irreducible f) : ∃ x : AlgebraicClosureAux k, f.eval x = 0 := by
   have : ∃ n p, Polynomial.map (ofStep k n) p = f := by
     convert Ring.DirectLimit.Polynomial.exists_of f
   obtain ⟨n, p, rfl⟩ := this
@@ -352,36 +355,19 @@ theorem exists_root {f : Polynomial (AlgebraicClosure k)} (hfm : f.Monic) (hfi :
   obtain ⟨x, hx⟩ := toStepSucc.exists_root k hfm this
   refine' ⟨ofStep k (n + 1) x, _⟩
   rw [← ofStep_succ k n, eval_map, ← hom_eval₂, hx, RingHom.map_zero]
-#align algebraic_closure.exists_root AlgebraicClosure.exists_root
+#noalign algebraic_closure.exists_root
 
-instance instIsAlgClosed : IsAlgClosed (AlgebraicClosure k) :=
+@[local instance] theorem instIsAlgClosed : IsAlgClosed (AlgebraicClosureAux k) :=
   IsAlgClosed.of_exists_root _ fun _ => exists_root k
-#align algebraic_closure.is_alg_closed AlgebraicClosure.instIsAlgClosed
 
-instance instAlgebra {R : Type*} [CommSemiring R] [alg : Algebra R k] :
-    Algebra R (AlgebraicClosure k) :=
-  ((ofStep k 0).comp (@algebraMap _ _ _ _ alg)).toAlgebra
+/-- `AlgebraicClosureAux k` is a `k`-`Algebra` -/
+local instance instAlgebra : Algebra k (AlgebraicClosureAux k) :=
+  (ofStep k 0).toAlgebra
 
-theorem algebraMap_def {R : Type*} [CommSemiring R] [alg : Algebra R k] :
-    algebraMap R (AlgebraicClosure k) = (ofStep k 0 : k →+* _).comp (@algebraMap _ _ _ _ alg) :=
-  rfl
-#align algebraic_closure.algebra_map_def AlgebraicClosure.algebraMap_def
-
-
-instance {R S : Type*} [CommSemiring R] [CommSemiring S] [Algebra R S] [Algebra S k] [Algebra R k]
-    [IsScalarTower R S k] : IsScalarTower R S (AlgebraicClosure k) := by
-  apply IsScalarTower.of_algebraMap_eq _
-  intro x
-  simp only [algebraMap_def]
-  rw [RingHom.comp_apply, RingHom.comp_apply]
-  exact RingHom.congr_arg _ (IsScalarTower.algebraMap_apply R S k x : _)
-  -- Porting Note: Original proof (without `by`) didn't work anymore, I think it couldn't figure
-  -- out `algebraMap_def`. Orignally:
-  -- IsScalarTower.of_algebraMap_eq fun x =>
-  --   RingHom.congr_arg _ (IsScalarTower.algebraMap_apply R S k x : _)
+#noalign algebraic_closure.algebra_map_def
 
 /-- Canonical algebra embedding from the `n`th step to the algebraic closure. -/
-def ofStepHom (n) : Step k n →ₐ[k] AlgebraicClosure k :=
+def ofStepHom (n) : Step k n →ₐ[k] AlgebraicClosureAux k :=
   { ofStep k n with
     commutes' := by
     --Porting Note: Originally `(fun x => Ring.DirectLimit.of_f n.zero_le x)`
@@ -391,15 +377,107 @@ def ofStepHom (n) : Step k n →ₐ[k] AlgebraicClosure k :=
           MonoidHom.coe_coe]
       convert @Ring.DirectLimit.of_f ℕ _ (Step k) _ (fun m n h => (toStepOfLE k m n h : _ → _))
           0 n n.zero_le x }
-#align algebraic_closure.of_step_hom AlgebraicClosure.ofStepHom
+#noalign algebraic_closure.of_step_hom
 
-theorem isAlgebraic : Algebra.IsAlgebraic k (AlgebraicClosure k) := fun z =>
+theorem isAlgebraic : Algebra.IsAlgebraic k (AlgebraicClosureAux k) := fun z =>
   isAlgebraic_iff_isIntegral.2 <|
     let ⟨n, x, hx⟩ := exists_ofStep k z
     hx ▸ map_isIntegral (ofStepHom k n) (Step.isIntegral k n x)
+
+@[local instance] theorem isAlgClosure : IsAlgClosure k (AlgebraicClosureAux k) :=
+  ⟨AlgebraicClosureAux.instIsAlgClosed k, isAlgebraic k⟩
+
+end AlgebraicClosureAux
+
+attribute [local instance] AlgebraicClosureAux.field AlgebraicClosureAux.instAlgebra
+  AlgebraicClosureAux.instIsAlgClosed
+
+/-- The canonical algebraic closure of a field, the direct limit of adding roots to the field for
+each polynomial over the field. -/
+def AlgebraicClosure : Type u :=
+  MvPolynomial (AlgebraicClosureAux k) k ⧸
+    RingHom.ker (MvPolynomial.aeval (R := k) id).toRingHom
+
+namespace AlgebraicClosure
+
+instance commRing : CommRing (AlgebraicClosure k) :=
+  Ideal.Quotient.commRing _
+
+instance inhabited : Inhabited (AlgebraicClosure k) :=
+  ⟨37⟩
+
+instance {S : Type*} [DistribSMul S k] [IsScalarTower S k k] : SMul S (AlgebraicClosure k) :=
+  Submodule.Quotient.instSMul' _
+
+instance instAlgebra {R : Type*} [CommSemiring R] [Algebra R k] : Algebra R (AlgebraicClosure k) :=
+  Ideal.Quotient.algebra _
+
+instance {R S : Type*} [CommSemiring R] [CommSemiring S] [Algebra R S] [Algebra S k] [Algebra R k]
+    [IsScalarTower R S k] : IsScalarTower R S (AlgebraicClosure k) :=
+  Ideal.Quotient.isScalarTower _ _ _
+
+/-- The equivalence between `AlgebraicClosure` and `AlgebraicClosureAux`, which we use to transfer
+properties of `AlgebraicClosureAux` to `AlgebraicClosure` -/
+def algEquivAlgebraicClosureAux :
+    AlgebraicClosure k ≃ₐ[k] AlgebraicClosureAux k := by
+  delta AlgebraicClosure
+  exact Ideal.quotientKerAlgEquivOfSurjective
+    (fun x => ⟨MvPolynomial.X x, by simp⟩)
+
+-- This instance is basically copied from the `Field` instance on `SplittingField`
+instance : Field (AlgebraicClosure k) :=
+  letI e := algEquivAlgebraicClosureAux k
+  { toCommRing := AlgebraicClosure.commRing k
+    ratCast := fun a => algebraMap k _ (a : k)
+    inv := fun a => e.symm (e a)⁻¹
+    qsmul := (· • ·)
+    qsmul_eq_mul' := fun a x =>
+      Quotient.inductionOn x (fun p => congr_arg Quotient.mk''
+        (by ext; simp [MvPolynomial.algebraMap_eq, Rat.smul_def]))
+    ratCast_mk := fun a b h1 h2 => by
+      apply_fun e
+      change e (algebraMap k _ _) = _
+      simp only [map_ratCast, map_natCast, map_mul, map_intCast, AlgEquiv.commutes,
+        AlgEquiv.apply_symm_apply]
+      apply Field.ratCast_mk
+    exists_pair_ne := ⟨e.symm 0, e.symm 1, fun w => zero_ne_one ((e.symm).injective w)⟩
+    mul_inv_cancel := fun a w => by
+      apply_fun e
+      simp_rw [map_mul, e.apply_symm_apply, map_one]
+      exact mul_inv_cancel ((AddEquivClass.map_ne_zero_iff e).mpr w)
+    inv_zero := by simp }
+
+instance isAlgClosed : IsAlgClosed (AlgebraicClosure k) :=
+  IsAlgClosed.of_ringEquiv _ _ (algEquivAlgebraicClosureAux k).symm.toRingEquiv
+#align algebraic_closure.is_alg_closed AlgebraicClosure.isAlgClosed
+
+instance : IsAlgClosure k (AlgebraicClosure k) := by
+  rw [isAlgClosure_iff]
+  refine ⟨inferInstance, (algEquivAlgebraicClosureAux k).symm.isAlgebraic <|
+    AlgebraicClosureAux.isAlgebraic _⟩
+
+theorem isAlgebraic : Algebra.IsAlgebraic k (AlgebraicClosure k) :=
+  IsAlgClosure.algebraic
 #align algebraic_closure.is_algebraic AlgebraicClosure.isAlgebraic
 
-instance : IsAlgClosure k (AlgebraicClosure k) :=
-  ⟨AlgebraicClosure.instIsAlgClosed k, isAlgebraic k⟩
+instance [CharZero k] : CharZero (AlgebraicClosure k) :=
+  charZero_of_injective_algebraMap (RingHom.injective (algebraMap k (AlgebraicClosure k)))
+
+instance {p : ℕ} [CharP k p] : CharP (AlgebraicClosure k) p :=
+  charP_of_injective_algebraMap (RingHom.injective (algebraMap k (AlgebraicClosure k))) p
+
+example : (AddCommMonoid.natModule : Module ℕ (AlgebraicClosure k)) =
+      @Algebra.toModule _ _ _ _ (AlgebraicClosure.instAlgebra k) :=
+  rfl
+
+example : (AddCommGroup.intModule _ : Module ℤ (AlgebraicClosure k)) =
+      @Algebra.toModule _ _ _ _ (AlgebraicClosure.instAlgebra k) :=
+  rfl
+
+example [CharZero k] : AlgebraicClosure.instAlgebra k = algebraRat :=
+  rfl
+
+example : algebraInt (AlgebraicClosure ℚ) = AlgebraicClosure.instAlgebra ℚ :=
+  rfl
 
 end AlgebraicClosure

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -139,6 +139,21 @@ theorem of_exists_root (H : ∀ p : k[X], p.Monic → Irreducible p → ∃ x, p
   exact degree_mul_leadingCoeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root this hx
 #align is_alg_closed.of_exists_root IsAlgClosed.of_exists_root
 
+theorem of_ringEquiv (k' : Type u) [Field k'] (e : k ≃+* k')
+    [IsAlgClosed k] : IsAlgClosed k' := by
+  apply IsAlgClosed.of_exists_root
+  intro p hmp hp
+  have hpe : degree (p.map e.symm.toRingHom) ≠ 0 := by
+    rw [degree_map]
+    exact ne_of_gt (degree_pos_of_irreducible hp)
+  rcases IsAlgClosed.exists_root (k := k) (p.map e.symm) hpe with ⟨x, hx⟩
+  use e x
+  rw [IsRoot] at hx
+  apply e.symm.injective
+  rw [map_zero, ← hx]
+  clear hx hpe hp hmp
+  induction p using Polynomial.induction_on <;> simp_all
+
 theorem degree_eq_one_of_irreducible [IsAlgClosed k] {p : k[X]} (hp : Irreducible p) :
     p.degree = 1 :=
   degree_eq_one_of_irreducible_of_splits hp (IsAlgClosed.splits_codomain _)