chore(ring_theory): protect algebra.is_integral (#18178)

alreadydone · alreadydone · commit 825edd3cd735 · 2023-01-27T01:10:41.000Z
Co-authored-by: Junyan Xu &lt;junyanxu.math@gmail.com&gt;
diff --git a/src/field_theory/intermediate_field.lean b/src/field_theory/intermediate_field.lean
@@ -360,7 +360,7 @@ begin
 end
 
 lemma coe_is_integral_iff {R : Type*} [comm_ring R] [algebra R K] [algebra R L]
-  [is_scalar_tower R K L] {x : S} : is_integral R (x : L) ↔ _root_.is_integral R x :=
+  [is_scalar_tower R K L] {x : S} : is_integral R (x : L) ↔ is_integral R x :=
 begin
   refine ⟨λ h, _, λ h, _⟩,
   { obtain ⟨P, hPmo, hProot⟩ := h,
diff --git a/src/field_theory/minpoly/is_integrally_closed.lean b/src/field_theory/minpoly/is_integrally_closed.lean
@@ -180,14 +180,14 @@ alg_equiv.of_bijective (minpoly.to_adjoin R x)
 
 /-- The `power_basis` of `adjoin R {x}` given by `x`. See `algebra.adjoin.power_basis` for a version
 over a field. -/
-@[simps] def _root_.algebra.adjoin.power_basis' (hx : _root_.is_integral R x) :
-  _root_.power_basis R (algebra.adjoin R ({x} : set S)) :=
+@[simps] def _root_.algebra.adjoin.power_basis' (hx : is_integral R x) :
+  power_basis R (algebra.adjoin R ({x} : set S)) :=
 power_basis.map (adjoin_root.power_basis' (minpoly.monic hx)) (minpoly.equiv_adjoin hx)
 
 /-- The power basis given by `x` if `B.gen ∈ adjoin R {x}`. -/
-@[simps] noncomputable def _root_.power_basis.of_gen_mem_adjoin' (B : _root_.power_basis R S)
+@[simps] noncomputable def _root_.power_basis.of_gen_mem_adjoin' (B : power_basis R S)
   (hint : is_integral R x) (hx : B.gen ∈ adjoin R ({x} : set S)) :
-  _root_.power_basis R S :=
+  power_basis R S :=
 (algebra.adjoin.power_basis' hint).map $
   (subalgebra.equiv_of_eq _ _ $ power_basis.adjoin_eq_top_of_gen_mem_adjoin hx).trans
   subalgebra.top_equiv
diff --git a/src/ring_theory/adjoin/power_basis.lean b/src/ring_theory/adjoin/power_basis.lean
@@ -27,11 +27,11 @@ open_locale big_operators
 
 /-- The elements `1, x, ..., x ^ (d - 1)` for a basis for the `K`-module `K[x]`,
 where `d` is the degree of the minimal polynomial of `x`. -/
-noncomputable def adjoin.power_basis_aux {x : S} (hx : _root_.is_integral K x) :
+noncomputable def adjoin.power_basis_aux {x : S} (hx : is_integral K x) :
   basis (fin (minpoly K x).nat_degree) K (adjoin K ({x} : set S)) :=
 begin
   have hST : function.injective (algebra_map (adjoin K ({x} : set S)) S) := subtype.coe_injective,
-  have hx' : _root_.is_integral K
+  have hx' : is_integral K
     (show adjoin K ({x} : set S), from ⟨x, subset_adjoin (set.mem_singleton x)⟩),
   { apply (is_integral_algebra_map_iff hST).mp,
     convert hx,
@@ -55,7 +55,7 @@ end
 /-- The power basis `1, x, ..., x ^ (d - 1)` for `K[x]`,
 where `d` is the degree of the minimal polynomial of `x`. See `algebra.adjoin.power_basis'` for
 a version over a more general base ring. -/
-@[simps gen dim] noncomputable def adjoin.power_basis {x : S} (hx : _root_.is_integral K x) :
+@[simps gen dim] noncomputable def adjoin.power_basis {x : S} (hx : is_integral K x) :
   power_basis K (adjoin K ({x} : set S)) :=
 { gen := ⟨x, subset_adjoin (set.mem_singleton x)⟩,
   dim := (minpoly K x).nat_degree,
@@ -69,7 +69,7 @@ open algebra
 /-- The power basis given by `x` if `B.gen ∈ adjoin K {x}`. See `power_basis.of_gen_mem_adjoin'`
 for a version over a more general base ring. -/
 @[simps] noncomputable def power_basis.of_gen_mem_adjoin {x : S} (B : power_basis K S)
-  (hint : _root_.is_integral K x) (hx : B.gen ∈ adjoin K ({x} : set S)) : power_basis K S :=
+  (hint : is_integral K x) (hx : B.gen ∈ adjoin K ({x} : set S)) : power_basis K S :=
 (algebra.adjoin.power_basis hint).map $
   (subalgebra.equiv_of_eq _ _ $ power_basis.adjoin_eq_top_of_gen_mem_adjoin hx).trans
   subalgebra.top_equiv
@@ -173,7 +173,7 @@ if `minpoly K B.gen = (minpoly R B.gen).map (algebra_map R L)`. This is the case
 if `R` is a GCD domain and `K` is its fraction ring. -/
 lemma to_matrix_is_integral {B B' : power_basis K S} {P : R[X]} (h : aeval B.gen P = B'.gen)
   (hB : is_integral R B.gen) (hmin : minpoly K B.gen = (minpoly R B.gen).map (algebra_map R K)) :
-  ∀ i j, _root_.is_integral R (B.basis.to_matrix B'.basis i j) :=
+  ∀ i j, is_integral R (B.basis.to_matrix B'.basis i j) :=
 begin
   intros i j,
   rw [B.basis.to_matrix_apply, B'.coe_basis],
diff --git a/src/ring_theory/discriminant.lean b/src/ring_theory/discriminant.lean
@@ -261,8 +261,6 @@ section integral
 
 variables {R : Type z} [comm_ring R] [algebra R K] [algebra R L] [is_scalar_tower R K L]
 
-local notation `is_integral` := _root_.is_integral
-
 /-- If `K` and `L` are fields and `is_scalar_tower R K L`, and `b : ι → L` satisfies
 ` ∀ i, is_integral R (b i)`, then `is_integral R (discr K b)`. -/
 lemma discr_is_integral {b : ι → L} (h : ∀ i, is_integral R (b i)) :
diff --git a/src/ring_theory/integral_closure.lean b/src/ring_theory/integral_closure.lean
@@ -59,7 +59,7 @@ def is_integral (x : A) : Prop :=
 variable (A)
 
 /-- An algebra is integral if every element of the extension is integral over the base ring -/
-def algebra.is_integral : Prop :=
+protected def algebra.is_integral : Prop :=
 (algebra_map R A).is_integral
 
 variables {R A}
@@ -865,7 +865,7 @@ variables [algebra R A] [is_scalar_tower R A B]
 
 /-- If A is an R-algebra all of whose elements are integral over R,
 and x is an element of an A-algebra that is integral over A, then x is integral over R.-/
-lemma is_integral_trans (A_int : is_integral R A) (x : B) (hx : is_integral A x) :
+lemma is_integral_trans (A_int : algebra.is_integral R A) (x : B) (hx : is_integral A x) :
   is_integral R x :=
 begin
   rcases hx with ⟨p, pmonic, hp⟩,
@@ -883,7 +883,8 @@ end
 /-- If A is an R-algebra all of whose elements are integral over R,
 and B is an A-algebra all of whose elements are integral over A,
 then all elements of B are integral over R.-/
-lemma algebra.is_integral_trans (hA : is_integral R A) (hB : is_integral A B) : is_integral R B :=
+lemma algebra.is_integral_trans (hA : algebra.is_integral R A) (hB : algebra.is_integral A B) :
+  algebra.is_integral R B :=
 λ x, is_integral_trans hA x (hB x)
 
 lemma ring_hom.is_integral_trans (hf : f.is_integral) (hg : g.is_integral) :
@@ -895,8 +896,8 @@ lemma ring_hom.is_integral_trans (hf : f.is_integral) (hg : g.is_integral) :
 lemma ring_hom.is_integral_of_surjective (hf : function.surjective f) : f.is_integral :=
 λ x, (hf x).rec_on (λ y hy, (hy ▸ f.is_integral_map : f.is_integral_elem x))
 
-lemma is_integral_of_surjective (h : function.surjective (algebra_map R A)) : is_integral R A :=
-(algebra_map R A).is_integral_of_surjective h
+lemma is_integral_of_surjective (h : function.surjective (algebra_map R A)) :
+  algebra.is_integral R A := (algebra_map R A).is_integral_of_surjective h
 
 /-- If `R → A → B` is an algebra tower with `A → B` injective,
 then if the entire tower is an integral extension so is `R → A` -/
@@ -949,8 +950,8 @@ begin
   simpa only [hom_eval₂, eval₂_map] using congr_arg (ideal.quotient.mk I) hpx
 end
 
-lemma is_integral_quotient_of_is_integral {I : ideal A} (hRA : is_integral R A) :
-  is_integral (R ⧸ I.comap (algebra_map R A)) (A ⧸ I) :=
+lemma is_integral_quotient_of_is_integral {I : ideal A} (hRA : algebra.is_integral R A) :
+  algebra.is_integral (R ⧸ I.comap (algebra_map R A)) (A ⧸ I) :=
 (algebra_map R A).is_integral_quotient_of_is_integral hRA
 
 lemma is_integral_quotient_map_iff {I : ideal S} :
@@ -967,7 +968,7 @@ end
 /-- If the integral extension `R → S` is injective, and `S` is a field, then `R` is also a field. -/
 lemma is_field_of_is_integral_of_is_field
   {R S : Type*} [comm_ring R] [nontrivial R] [comm_ring S] [is_domain S]
-  [algebra R S] (H : is_integral R S) (hRS : function.injective (algebra_map R S))
+  [algebra R S] (H : algebra.is_integral R S) (hRS : function.injective (algebra_map R S))
   (hS : is_field S) : is_field R :=
 begin
   refine ⟨⟨0, 1, zero_ne_one⟩, mul_comm, λ a ha, _⟩,
diff --git a/src/ring_theory/norm.lean b/src/ring_theory/norm.lean
@@ -191,7 +191,7 @@ variable {K}
 section intermediate_field
 
 lemma _root_.intermediate_field.adjoin_simple.norm_gen_eq_one {x : L}
-  (hx : ¬_root_.is_integral K x) : norm K (adjoin_simple.gen K x) = 1 :=
+  (hx : ¬is_integral K x) : norm K (adjoin_simple.gen K x) = 1 :=
 begin
   rw [norm_eq_one_of_not_exists_basis],
   contrapose! hx,
@@ -207,9 +207,9 @@ lemma _root_.intermediate_field.adjoin_simple.norm_gen_eq_prod_roots (x : L)
     ((minpoly K x).map (algebra_map K F)).roots.prod :=
 begin
   have injKxL := (algebra_map K⟮x⟯ L).injective,
-  by_cases hx : _root_.is_integral K x, swap,
+  by_cases hx : is_integral K x, swap,
   { simp [minpoly.eq_zero hx, intermediate_field.adjoin_simple.norm_gen_eq_one hx] },
-  have hx' : _root_.is_integral K (adjoin_simple.gen K x),
+  have hx' : is_integral K (adjoin_simple.gen K x),
   { rwa [← is_integral_algebra_map_iff injKxL, adjoin_simple.algebra_map_gen],
     apply_instance },
   rw [← adjoin.power_basis_gen hx, power_basis.norm_gen_eq_prod_roots];
@@ -297,10 +297,10 @@ begin
 end
 
 lemma is_integral_norm [algebra R L] [algebra R K] [is_scalar_tower R K L]
-  [is_separable K L] [finite_dimensional K L] {x : L} (hx : _root_.is_integral R x) :
-  _root_.is_integral R (norm K x) :=
+  [is_separable K L] [finite_dimensional K L] {x : L} (hx : is_integral R x) :
+  is_integral R (norm K x) :=
 begin
-  have hx' : _root_.is_integral K x := is_integral_of_is_scalar_tower hx,
+  have hx' : is_integral K x := is_integral_of_is_scalar_tower hx,
   rw [← is_integral_algebra_map_iff (algebra_map K (algebraic_closure L)).injective,
       norm_eq_prod_roots],
   { refine (is_integral.multiset_prod (λ y hy, _)).pow _,
diff --git a/src/ring_theory/trace.lean b/src/ring_theory/trace.lean
@@ -283,10 +283,10 @@ variables [algebra R L] [algebra L F] [algebra R F] [is_scalar_tower R L F]
 
 open polynomial
 
-lemma algebra.is_integral_trace [finite_dimensional L F] {x : F} (hx : _root_.is_integral R x) :
-  _root_.is_integral R (algebra.trace L F x) :=
+lemma algebra.is_integral_trace [finite_dimensional L F] {x : F} (hx : is_integral R x) :
+  is_integral R (algebra.trace L F x) :=
 begin
-  have hx' : _root_.is_integral L x := is_integral_of_is_scalar_tower hx,
+  have hx' : is_integral L x := is_integral_of_is_scalar_tower hx,
   rw [← is_integral_algebra_map_iff (algebra_map L (algebraic_closure F)).injective,
       trace_eq_sum_roots],
   { refine (is_integral.multiset_sum _).nsmul _,
