refactor: Turn Algebra.IsAlgebraic and Algebra.IsIntegral into classes (#12761)

As [discussed on Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Typeclass.20for.20algebraic.20extension.20of.20fields.3F), this PR replaces the current definition of `Algebra.IsAlgebraic` and `Algebra.IsIntegral` with classes.

The following main changes are required:
 * Since a class must be a structure, we can't identify `Algebra.IsAlgebraic R A` with `∀ (x : A), IsAlgebraic R x`. Either use the projection `.isAlgebraic`, or use the new definition `Algebra.IsAlgebraic.isAlgebraic` which leaves the proof implicit. Idem for integral.
 * Turn `Algebra.IsAlgebraic` and `Algebra.IsIntegral` arguments into instance implicits; turn theorems with those as the conclusion into instances.
 * `Algebra.IsAlgebraic` is now `protected`, like `Algebra.IsIntegral`.

The spelling `Algebra.IsAlgebraic.isAlgebraic x` and `Algebra.IsIntegral.isIntegral x` to prove an element `x` is algebraic/integral is kind of ugly, do you have better suggestions?

Author: Vierkantor

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -721,9 +721,9 @@ theorem comap_singleton_isClosed_of_surjective (f : R →+* S) (hf : Function.Su
 theorem comap_singleton_isClosed_of_isIntegral (f : R →+* S) (hf : f.IsIntegral)
     (x : PrimeSpectrum S) (hx : IsClosed ({x} : Set (PrimeSpectrum S))) :
     IsClosed ({comap f x} : Set (PrimeSpectrum R)) :=
+  have := (isClosed_singleton_iff_isMaximal x).1 hx
   (isClosed_singleton_iff_isMaximal _).2
-    (Ideal.isMaximal_comap_of_isIntegral_of_isMaximal' f hf x.asIdeal <|
-      (isClosed_singleton_iff_isMaximal x).1 hx)
+    (Ideal.isMaximal_comap_of_isIntegral_of_isMaximal' f hf x.asIdeal)
 #align prime_spectrum.comap_singleton_is_closed_of_is_integral PrimeSpectrum.comap_singleton_isClosed_of_isIntegral
 
 theorem image_comap_zeroLocus_eq_zeroLocus_comap (hf : Surjective f) (I : Ideal S) :

Mathlib/FieldTheory/Adjoin.lean

@@ -631,7 +631,7 @@ theorem adjoin_algebraic_toSubalgebra {S : Set E} (hS : ∀ x ∈ S, IsAlgebraic
   simp only [isAlgebraic_iff_isIntegral] at hS
   have : Algebra.IsIntegral F (Algebra.adjoin F S) := by
     rwa [← le_integralClosure_iff_isIntegral, Algebra.adjoin_le_iff]
-  have := isField_of_isIntegral_of_isField' this (Field.toIsField F)
+  have : IsField (Algebra.adjoin F S) := isField_of_isIntegral_of_isField' (Field.toIsField F)
   rw [← ((Algebra.adjoin F S).toIntermediateField' this).eq_adjoin_of_eq_algebra_adjoin F S] <;> rfl
 #align intermediate_field.adjoin_algebraic_to_subalgebra IntermediateField.adjoin_algebraic_toSubalgebra
 
@@ -675,38 +675,39 @@ theorem le_sup_toSubalgebra : E1.toSubalgebra ⊔ E2.toSubalgebra ≤ (E1 ⊔ E2
   sup_le (show E1 ≤ E1 ⊔ E2 from le_sup_left) (show E2 ≤ E1 ⊔ E2 from le_sup_right)
 #align intermediate_field.le_sup_to_subalgebra IntermediateField.le_sup_toSubalgebra
 
-theorem sup_toSubalgebra_of_isAlgebraic_right (halg : Algebra.IsAlgebraic K E2) :
+theorem sup_toSubalgebra_of_isAlgebraic_right [Algebra.IsAlgebraic K E2] :
     (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra := by
   have : (adjoin E1 (E2 : Set L)).toSubalgebra = _ := adjoin_algebraic_toSubalgebra fun x h ↦
-    IsAlgebraic.tower_top E1 (isAlgebraic_iff.1 (halg ⟨x, h⟩))
+    IsAlgebraic.tower_top E1 (isAlgebraic_iff.1
+      (Algebra.IsAlgebraic.isAlgebraic (⟨x, h⟩ : E2)))
   apply_fun Subalgebra.restrictScalars K at this
   erw [← restrictScalars_toSubalgebra, restrictScalars_adjoin,
     Algebra.restrictScalars_adjoin] at this
   exact this
 
-theorem sup_toSubalgebra_of_isAlgebraic_left (halg : Algebra.IsAlgebraic K E1) :
+theorem sup_toSubalgebra_of_isAlgebraic_left [Algebra.IsAlgebraic K E1] :
     (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra := by
-  have := sup_toSubalgebra_of_isAlgebraic_right E2 E1 halg
+  have := sup_toSubalgebra_of_isAlgebraic_right E2 E1
   rwa [sup_comm (a := E1), sup_comm (a := E1.toSubalgebra)]
 
 /-- The compositum of two intermediate fields is equal to the compositum of them
 as subalgebras, if one of them is algebraic over the base field. -/
 theorem sup_toSubalgebra_of_isAlgebraic
     (halg : Algebra.IsAlgebraic K E1 ∨ Algebra.IsAlgebraic K E2) :
     (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra :=
-  halg.elim (sup_toSubalgebra_of_isAlgebraic_left E1 E2)
-    (sup_toSubalgebra_of_isAlgebraic_right E1 E2)
+  halg.elim (fun _ ↦ sup_toSubalgebra_of_isAlgebraic_left E1 E2)
+    (fun _ ↦ sup_toSubalgebra_of_isAlgebraic_right E1 E2)
 
 theorem sup_toSubalgebra_of_left [FiniteDimensional K E1] :
     (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra :=
-  sup_toSubalgebra_of_isAlgebraic_left E1 E2 (Algebra.IsAlgebraic.of_finite K _)
+  sup_toSubalgebra_of_isAlgebraic_left E1 E2
 #align intermediate_field.sup_to_subalgebra IntermediateField.sup_toSubalgebra_of_left
 
 @[deprecated] alias sup_toSubalgebra := sup_toSubalgebra_of_left
 
 theorem sup_toSubalgebra_of_right [FiniteDimensional K E2] :
     (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra :=
-  sup_toSubalgebra_of_isAlgebraic_right E1 E2 (Algebra.IsAlgebraic.of_finite K _)
+  sup_toSubalgebra_of_isAlgebraic_right E1 E2
 
 instance finiteDimensional_sup [FiniteDimensional K E1] [FiniteDimensional K E2] :
     FiniteDimensional K (E1 ⊔ E2 : IntermediateField K L) := by
@@ -804,15 +805,16 @@ theorem adjoin_toSubalgebra_of_isAlgebraic (L : IntermediateField F K)
   erw [← restrictScalars_toSubalgebra, restrictScalars_adjoin_of_algEquiv i' hi,
     Algebra.restrictScalars_adjoin_of_algEquiv i' hi, restrictScalars_adjoin,
     Algebra.restrictScalars_adjoin]
-  exact E'.sup_toSubalgebra_of_isAlgebraic L (halg.imp i'.isAlgebraic id)
+  exact E'.sup_toSubalgebra_of_isAlgebraic L (halg.imp
+    (fun (_ : Algebra.IsAlgebraic F E) ↦ i'.isAlgebraic) id)
 
 theorem adjoin_toSubalgebra_of_isAlgebraic_left (L : IntermediateField F K)
-    (halg : Algebra.IsAlgebraic F E) :
+    [halg : Algebra.IsAlgebraic F E] :
     (adjoin E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K) :=
   adjoin_toSubalgebra_of_isAlgebraic E L (Or.inl halg)
 
 theorem adjoin_toSubalgebra_of_isAlgebraic_right (L : IntermediateField F K)
-    (halg : Algebra.IsAlgebraic F L) :
+    [halg : Algebra.IsAlgebraic F L] :
     (adjoin E (L : Set K)).toSubalgebra = Algebra.adjoin E (L : Set K) :=
   adjoin_toSubalgebra_of_isAlgebraic E L (Or.inr halg)
 
@@ -829,12 +831,12 @@ theorem adjoin_rank_le_of_isAlgebraic (L : IntermediateField F K)
   rwa [(Subalgebra.equivOfEq _ _ h).symm.toLinearEquiv.rank_eq] at this
 
 theorem adjoin_rank_le_of_isAlgebraic_left (L : IntermediateField F K)
-    (halg : Algebra.IsAlgebraic F E) :
+    [halg : Algebra.IsAlgebraic F E] :
     Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L :=
   adjoin_rank_le_of_isAlgebraic E L (Or.inl halg)
 
 theorem adjoin_rank_le_of_isAlgebraic_right (L : IntermediateField F K)
-    (halg : Algebra.IsAlgebraic F L) :
+    [halg : Algebra.IsAlgebraic F L] :
     Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L :=
   adjoin_rank_le_of_isAlgebraic E L (Or.inr halg)
 
@@ -905,7 +907,7 @@ theorem exists_finset_of_mem_supr'' {ι : Type*} {f : ι → IntermediateField F
     (subset_adjoin F (rootSet (minpoly F x1) E) _)
   · rw [IntermediateField.minpoly_eq, Subtype.coe_mk]
   · rw [mem_rootSet_of_ne, minpoly.aeval]
-    exact minpoly.ne_zero (isIntegral_iff.mp (h i ⟨x1, hx1⟩).isIntegral)
+    exact minpoly.ne_zero (isIntegral_iff.mp (Algebra.IsIntegral.isIntegral (⟨x1, hx1⟩ : f i)))
 #align intermediate_field.exists_finset_of_mem_supr'' IntermediateField.exists_finset_of_mem_supr''
 
 theorem exists_finset_of_mem_adjoin {S : Set E} {x : E} (hx : x ∈ adjoin F S) :
@@ -1192,7 +1194,7 @@ variable {F} in
 /-- If `E / F` is an infinite algebraic extension, then there exists an intermediate field
 `L / F` with arbitrarily large finite extension degree. -/
 theorem exists_lt_finrank_of_infinite_dimensional
-    (halg : Algebra.IsAlgebraic F E) (hnfd : ¬ FiniteDimensional F E) (n : ℕ) :
+    [Algebra.IsAlgebraic F E] (hnfd : ¬ FiniteDimensional F E) (n : ℕ) :
     ∃ L : IntermediateField F E, FiniteDimensional F L ∧ n < finrank F L := by
   induction' n with n ih
   · exact ⟨⊥, Subalgebra.finite_bot, finrank_pos⟩
@@ -1202,7 +1204,7 @@ theorem exists_lt_finrank_of_infinite_dimensional
     rw [show L = ⊤ from eq_top_iff.2 fun x _ ↦ hnfd x] at fin
     exact topEquiv.toLinearEquiv.finiteDimensional
   let L' := L ⊔ F⟮x⟯
-  haveI := adjoin.finiteDimensional (halg x).isIntegral
+  haveI := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) x)
   refine ⟨L', inferInstance, by_contra fun h ↦ ?_⟩
   have h1 : L = L' := eq_of_le_of_finrank_le le_sup_left ((not_lt.1 h).trans hn)
   have h2 : F⟮x⟯ ≤ L' := le_sup_right
@@ -1224,12 +1226,13 @@ theorem _root_.minpoly.degree_le (x : L) [FiniteDimensional K L] :
 theorem isAlgebraic_iSup {ι : Type*} {t : ι → IntermediateField K L}
     (h : ∀ i, Algebra.IsAlgebraic K (t i)) :
     Algebra.IsAlgebraic K (⨆ i, t i : IntermediateField K L) := by
+  constructor
   rintro ⟨x, hx⟩
   obtain ⟨s, hx⟩ := exists_finset_of_mem_supr' hx
   rw [isAlgebraic_iff, Subtype.coe_mk, ← Subtype.coe_mk (p := (· ∈ _)) x hx, ← isAlgebraic_iff]
   haveI : ∀ i : Σ i, t i, FiniteDimensional K K⟮(i.2 : L)⟯ := fun ⟨i, x⟩ ↦
-    adjoin.finiteDimensional (isIntegral_iff.1 (h i x).isIntegral)
-  apply Algebra.IsAlgebraic.of_finite
+    adjoin.finiteDimensional (isIntegral_iff.1 (Algebra.IsIntegral.isIntegral x))
+  apply IsAlgebraic.of_finite
 #align intermediate_field.is_algebraic_supr IntermediateField.isAlgebraic_iSup
 
 theorem isAlgebraic_adjoin {S : Set L} (hS : ∀ x ∈ S, IsIntegral K x) :

Mathlib/FieldTheory/AxGrothendieck.lean

@@ -31,7 +31,7 @@ open MvPolynomial Finset Function
 
 /-- Any injective polynomial map over an algebraic extension of a finite field is surjective. -/
 theorem ax_grothendieck_of_locally_finite {ι K R : Type*} [Field K] [Finite K] [CommRing R]
-    [Finite ι] [Algebra K R] (alg : Algebra.IsAlgebraic K R) (ps : ι → MvPolynomial ι R)
+    [Finite ι] [Algebra K R] [Algebra.IsAlgebraic K R] (ps : ι → MvPolynomial ι R)
     (hinj : Injective fun v i => MvPolynomial.eval v (ps i)) :
     Surjective fun v i => MvPolynomial.eval v (ps i) := by
   classical
@@ -48,7 +48,7 @@ theorem ax_grothendieck_of_locally_finite {ι K R : Type*} [Field K] [Finite K]
         k ∈ (ps i).support → coeff k (ps i) ∈ Algebra.adjoin K (s : Set R) :=
       fun i k hk => Algebra.subset_adjoin
         (mem_union_left _ (mem_biUnion.2 ⟨i, mem_univ _, mem_image_of_mem _ hk⟩))
-    letI := isNoetherian_adjoin_finset s fun x _ => alg.isIntegral x
+    letI := isNoetherian_adjoin_finset s fun x _ => Algebra.IsIntegral.isIntegral (R := K) x
     letI := Module.IsNoetherian.finite K (Algebra.adjoin K (s : Set R))
     letI : Finite (Algebra.adjoin K (s : Set R)) :=
       FiniteDimensional.finite_of_finite K (Algebra.adjoin K (s : Set R))

Mathlib/FieldTheory/Extension.lean

@@ -173,7 +173,8 @@ theorem nonempty_algHom_of_adjoin_splits : Nonempty (E →ₐ[F] K) :=
 variable {x : E} (hx : x ∈ adjoin F S) {y : K} (hy : aeval y (minpoly F x) = 0)
 
 theorem exists_algHom_adjoin_of_splits_of_aeval : ∃ φ : adjoin F S →ₐ[F] K, φ ⟨x, hx⟩ = y := by
-  have ix := isAlgebraic_adjoin (fun s hs ↦ (hK s hs).1) ⟨x, hx⟩
+  have := isAlgebraic_adjoin (fun s hs ↦ (hK s hs).1)
+  have ix : IsAlgebraic F _ := Algebra.IsAlgebraic.isAlgebraic (⟨x, hx⟩ : adjoin F S)
   rw [isAlgebraic_iff_isIntegral, isIntegral_iff] at ix
   obtain ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits hK ((algHomAdjoinIntegralEquiv F ix).symm
     ⟨y, mem_aroots.mpr ⟨minpoly.ne_zero ix, hy⟩⟩) (adjoin_simple_le_iff.mpr hx)
@@ -207,12 +208,12 @@ of `x` over `F`. -/
 theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits {F K : Type*} (L : Type*)
     [Field F] [Field K] [Field L] [Algebra F L] [Algebra F K]
     (hA : ∀ x : K, (minpoly F x).Splits (algebraMap F L))
-    (hK : Algebra.IsAlgebraic F K) (x : K) :
+    [Algebra.IsAlgebraic F K] (x : K) :
     (Set.range fun (ψ : K →ₐ[F] L) => ψ x) = (minpoly F x).rootSet L := by
   ext a
-  rw [mem_rootSet_of_ne (minpoly.ne_zero (hK.isIntegral x))]
+  rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x))]
   refine ⟨fun ⟨ψ, hψ⟩ ↦ ?_, fun ha ↦ IntermediateField.exists_algHom_of_splits_of_aeval
-    (fun x ↦ ⟨hK.isIntegral x, hA x⟩) ha⟩
+    (fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, hA x⟩) ha⟩
   rw [← hψ, Polynomial.aeval_algHom_apply ψ x, minpoly.aeval, map_zero]
 
 end Algebra.IsAlgebraic

Mathlib/FieldTheory/Fixed.lean

@@ -275,13 +275,14 @@ section Finite
 
 variable [Finite G]
 
-instance normal : Normal (FixedPoints.subfield G F) F :=
-  ⟨fun x => (isIntegral G F x).isAlgebraic, fun x =>
+instance normal : Normal (FixedPoints.subfield G F) F where
+  isAlgebraic x := (isIntegral G F x).isAlgebraic
+  splits' x :=
     (Polynomial.splits_id_iff_splits _).1 <| by
       cases nonempty_fintype G
       rw [← minpoly_eq_minpoly, minpoly, coe_algebraMap, ← Subfield.toSubring_subtype_eq_subtype,
         Polynomial.map_toSubring _ (subfield G F).toSubring, prodXSubSMul]
-      exact Polynomial.splits_prod _ fun _ _ => Polynomial.splits_X_sub_C _⟩
+      exact Polynomial.splits_prod _ fun _ _ => Polynomial.splits_X_sub_C _
 #align fixed_points.normal FixedPoints.normal
 
 instance separable : IsSeparable (FixedPoints.subfield G F) F :=

Mathlib/FieldTheory/IntermediateField.lean

@@ -834,24 +834,25 @@ theorem minpoly_eq (x : S) : minpoly K x = minpoly K (x : L) :=
 end IntermediateField
 
 /-- If `L/K` is algebraic, the `K`-subalgebras of `L` are all fields.  -/
-def subalgebraEquivIntermediateField (alg : Algebra.IsAlgebraic K L) :
+def subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] :
     Subalgebra K L ≃o IntermediateField K L where
-  toFun S := S.toIntermediateField fun x hx => S.inv_mem_of_algebraic (alg (⟨x, hx⟩ : S))
+  toFun S := S.toIntermediateField fun x hx => S.inv_mem_of_algebraic
+    (Algebra.IsAlgebraic.isAlgebraic ((⟨x, hx⟩ : S) : L))
   invFun S := S.toSubalgebra
   left_inv _ := toSubalgebra_toIntermediateField _ _
   right_inv := toIntermediateField_toSubalgebra
   map_rel_iff' := Iff.rfl
 #align subalgebra_equiv_intermediate_field subalgebraEquivIntermediateField
 
 @[simp]
-theorem mem_subalgebraEquivIntermediateField (alg : Algebra.IsAlgebraic K L) {S : Subalgebra K L}
-    {x : L} : x ∈ subalgebraEquivIntermediateField alg S ↔ x ∈ S :=
+theorem mem_subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] {S : Subalgebra K L}
+    {x : L} : x ∈ subalgebraEquivIntermediateField S ↔ x ∈ S :=
   Iff.rfl
 #align mem_subalgebra_equiv_intermediate_field mem_subalgebraEquivIntermediateField
 
 @[simp]
-theorem mem_subalgebraEquivIntermediateField_symm (alg : Algebra.IsAlgebraic K L)
+theorem mem_subalgebraEquivIntermediateField_symm [Algebra.IsAlgebraic K L]
     {S : IntermediateField K L} {x : L} :
-    x ∈ (subalgebraEquivIntermediateField alg).symm S ↔ x ∈ S :=
+    x ∈ subalgebraEquivIntermediateField.symm S ↔ x ∈ S :=
   Iff.rfl
 #align mem_subalgebra_equiv_intermediate_field_symm mem_subalgebraEquivIntermediateField_symm

Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

@@ -380,10 +380,11 @@ def ofStepHom (n) : Step k n →ₐ[k] AlgebraicClosureAux k :=
           0 n n.zero_le x }
 #noalign algebraic_closure.of_step_hom
 
-theorem isAlgebraic : Algebra.IsAlgebraic k (AlgebraicClosureAux k) := fun z =>
-  IsIntegral.isAlgebraic <|
-    let ⟨n, x, hx⟩ := exists_ofStep k z
-    hx ▸ (Step.isIntegral k n x).map (ofStepHom k n)
+instance isAlgebraic : Algebra.IsAlgebraic k (AlgebraicClosureAux k) :=
+  ⟨fun z =>
+    IsIntegral.isAlgebraic <|
+      let ⟨n, x, hx⟩ := exists_ofStep k z
+      hx ▸ (Step.isIntegral k n x).map (ofStepHom k n)⟩
 
 @[local instance] theorem isAlgClosure : IsAlgClosure k (AlgebraicClosureAux k) :=
   ⟨AlgebraicClosureAux.instIsAlgClosed k, isAlgebraic k⟩
@@ -451,10 +452,9 @@ instance isAlgClosed : IsAlgClosed (AlgebraicClosure k) :=
 
 instance : IsAlgClosure k (AlgebraicClosure k) := by
   rw [isAlgClosure_iff]
-  refine ⟨inferInstance, (algEquivAlgebraicClosureAux k).symm.isAlgebraic <|
-    AlgebraicClosureAux.isAlgebraic _⟩
+  exact ⟨inferInstance, (algEquivAlgebraicClosureAux k).symm.isAlgebraic⟩
 
-theorem isAlgebraic : Algebra.IsAlgebraic k (AlgebraicClosure k) :=
+instance isAlgebraic : Algebra.IsAlgebraic k (AlgebraicClosure k) :=
   IsAlgClosure.algebraic
 #align algebraic_closure.is_algebraic AlgebraicClosure.isAlgebraic