feat: remove separability assumption from Algebra.dvd_algebraMap_intNorm_self (#30478)

Continuing the work of #30323 and #30448  we remove the separability assumption from `Algebra.dvd_algebraMap_intNorm_self`.

Author: riccardobrasca

Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

@@ -172,8 +172,7 @@ theorem spanNorm_mul_of_bot_or_top (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨
   rw [hJ]
   exact le_top
 
-theorem spanNorm_le_comap [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (I : Ideal S) :
-    spanNorm R I ≤ comap (algebraMap R S) I := by
+theorem spanNorm_le_comap (I : Ideal S) : spanNorm R I ≤ comap (algebraMap R S) I := by
   rw [spanNorm, Ideal.map, Ideal.span_le, ← Submodule.span_le]
   intro x hx
   induction hx using Submodule.span_induction with
@@ -328,8 +327,8 @@ open MulSemiringAction Pointwise in
 theorem relNorm_smul {G : Type*} [Group G] [MulSemiringAction G S] [SMulCommClass G R S] (g : G)
     (I : Ideal S) : relNorm R (g • I) = relNorm R I := relNorm_map_algEquiv (toAlgEquiv R S g) I
 
-theorem relNorm_le_comap [Algebra.IsSeparable (FractionRing R) (FractionRing S)] (I : Ideal S) :
-    relNorm R I ≤ comap (algebraMap R S) I := spanNorm_le_comap R I
+theorem relNorm_le_comap (I : Ideal S) : relNorm R I ≤ comap (algebraMap R S) I :=
+  spanNorm_le_comap R I
 
 theorem relNorm_relNorm (T : Type*) [CommRing T] [IsDedekindDomain T] [IsIntegrallyClosed T]
     [Algebra R T] [Algebra T S] [IsScalarTower R T S] [Module.Finite R T] [Module.Finite T S]

Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

@@ -524,8 +524,8 @@ lemma Algebra.algebraMap_intNorm_of_isGalois [IsGalois (FractionRing A) (Fractio
   simp only [MulEquiv.toEquiv_eq_coe, EquivLike.coe_coe]
   convert (prod_galRestrict_eq_norm A (FractionRing A) (FractionRing B) B x).symm
 
-theorem Algebra.dvd_algebraMap_intNorm_self [Algebra.IsSeparable (FractionRing A) (FractionRing B)]
-    (x : B) : x ∣ algebraMap A B (intNorm A B x) := by
+open Polynomial IsScalarTower in
+theorem Algebra.dvd_algebraMap_intNorm_self (x : B) : x ∣ algebraMap A B (intNorm A B x) := by
   classical
   by_cases hx : x = 0
   · exact ⟨1, by simp [hx]⟩
@@ -537,18 +537,27 @@ theorem Algebra.dvd_algebraMap_intNorm_self [Algebra.IsSeparable (FractionRing A
       _root_.IsIntegral.tower_top (A := B) this
     refine ⟨y, ?_⟩
     apply FaithfulSMul.algebraMap_injective B L
-    rw [← IsScalarTower.algebraMap_apply, map_mul, hy, mul_inv_cancel_left₀]
+    rw [← algebraMap_apply, map_mul, hy, mul_inv_cancel_left₀]
     exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B L)).mpr hx
-  rw [← isIntegral_algHom_iff (IsScalarTower.toAlgHom A L E)
-    (FaithfulSMul.algebraMap_injective L E), IsScalarTower.coe_toAlgHom', map_mul, map_inv₀,
-    IsScalarTower.algebraMap_apply A K L, algebraMap_intNorm (L := L),
-    ← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply, norm_eq_prod_embeddings,
-    ← Finset.univ.mul_prod_erase _ (Finset.mem_univ (IsScalarTower.toAlgHom K L E)),
-    IsScalarTower.coe_toAlgHom', ← IsScalarTower.algebraMap_apply, inv_mul_cancel_left₀]
-  · refine _root_.IsIntegral.prod _ fun σ _ ↦ ?_
-    change IsIntegral A ((σ.restrictScalars A) (IsScalarTower.toAlgHom A B L x))
-    rw [isIntegral_algHom_iff _ (RingHom.injective _),
-      isIntegral_algHom_iff _ (FaithfulSMul.algebraMap_injective B L)]
-    exact IsIntegral.isIntegral x
+  rw [← isIntegral_algHom_iff (toAlgHom A L E)
+    (FaithfulSMul.algebraMap_injective L E), coe_toAlgHom', map_mul, map_inv₀,
+    algebraMap_apply A K L, algebraMap_intNorm (L := L), ← algebraMap_apply, ← algebraMap_apply,
+    norm_eq_prod_roots _ (IsAlgClosed.splits_codomain _), ← Multiset.prod_erase
+    (a := algebraMap B E x)]
   · have := NoZeroSMulDivisors.trans_faithfulSMul B L E
-    exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B E)).mpr hx
+    rw [mul_pow, ← mul_pow_sub_one (Nat.pos_iff_ne_zero.1 Module.finrank_pos) (algebraMap B E x),
+      mul_assoc, inv_mul_cancel_left₀]
+    · refine IsIntegral.mul (IsIntegral.pow ?_ _)
+        (IsIntegral.pow (IsIntegral.multiset_prod (fun a ha ↦ ⟨minpoly A x, minpoly.monic
+          (IsIntegral.isIntegral x), ?_⟩)) _)
+      · exact (isIntegral_algebraMap_iff (NoZeroSMulDivisors.iff_algebraMap_injective.1 this)).mpr
+          (IsIntegral.isIntegral x)
+      · replace ha := Multiset.erase_subset _ _ ha
+        suffices (aeval a) ((minpoly A x).map (algebraMap A K)) = 0 by simpa
+        rw [← minpoly.isIntegrallyClosed_eq_field_fractions K L (IsIntegral.isIntegral x)]
+        simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap] at ha
+        exact ha.2
+    · exact (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective B E)).mpr hx
+  · simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap]
+    refine ⟨minpoly.ne_zero (IsIntegral.isIntegral _), ?_⟩
+    simp [algebraMap_apply B L E, aeval_algebraMap_apply]