feat: Define the different ideal. (#9063)

Mathlib/FieldTheory/Separable.lean

@@ -595,6 +595,19 @@ theorem IsSeparable.of_algHom (E' : Type*) [Field E'] [Algebra F E'] (f : E →
   exact isSeparable_tower_bot_of_isSeparable F E E'
 #align is_separable.of_alg_hom IsSeparable.of_algHom
 
+lemma IsSeparable.of_equiv_equiv {A₁ B₁ A₂ B₂ : Type*} [Field A₁] [Field B₁]
+    [Field A₂] [Field B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂)
+    (he : RingHom.comp (algebraMap A₂ B₂) ↑e₁ = RingHom.comp ↑e₂ (algebraMap A₁ B₁))
+    [IsSeparable A₁ B₁] : IsSeparable A₂ B₂ := by
+  letI := e₁.toRingHom.toAlgebra
+  letI := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
+  haveI : IsScalarTower A₁ A₂ B₁ := IsScalarTower.of_algebraMap_eq
+    (fun x ↦ by simp [RingHom.algebraMap_toAlgebra])
+  let e : B₁ ≃ₐ[A₂] B₂ := { e₂ with commutes' := fun r ↦ by simpa [RingHom.algebraMap_toAlgebra]
+                                                  using FunLike.congr_fun he.symm (e₁.symm r) }
+  haveI := isSeparable_tower_top_of_isSeparable A₁ A₂ B₁
+  exact IsSeparable.of_algHom _ _ e.symm.toAlgHom
+
 end IsSeparableTower
 
 section CardAlgHom

Mathlib/RingTheory/DedekindDomain/Different.lean

@@ -13,9 +13,9 @@ import Mathlib.RingTheory.DedekindDomain.IntegralClosure
 ## Main definition
 - `Submodule.traceDual`: The dual `L`-sub `B`-module under the trace form.
 - `FractionalIdeal.dual`: The dual fractional ideal under the trace form.
+- `differentIdeal`: The different ideal of an extension of integral domains.
 
 ## TODO
-- Define the relative different ideal
 - Show properties of the different ideal
 -/
 
@@ -153,6 +153,35 @@ lemma isIntegral_discr_mul_of_mem_traceDual
 
 variable (A K)
 
+lemma map_equiv_traceDual [NoZeroSMulDivisors A B] (I : Submodule B (FractionRing B)) :
+    (traceDual A (FractionRing A) I).map (FractionRing.algEquiv B L) =
+      traceDual A K (I.map (FractionRing.algEquiv B L)) := by
+  show Submodule.map (FractionRing.algEquiv B L).toLinearEquiv.toLinearMap _ =
+    traceDual A K (I.map (FractionRing.algEquiv B L).toLinearEquiv.toLinearMap)
+  rw [Submodule.map_equiv_eq_comap_symm, Submodule.map_equiv_eq_comap_symm]
+  ext x
+  simp only [AlgEquiv.toLinearEquiv_symm, AlgEquiv.toLinearEquiv_toLinearMap,
+    traceDual, traceForm_apply, Submodule.mem_comap, AlgEquiv.toLinearMap_apply,
+    Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk, Set.mem_setOf_eq]
+  apply (FractionRing.algEquiv B L).forall_congr
+  simp only [restrictScalars_mem, traceForm_apply, AlgEquiv.toEquiv_eq_coe,
+    EquivLike.coe_coe, mem_comap, AlgEquiv.toLinearMap_apply, AlgEquiv.symm_apply_apply]
+  refine fun {y} ↦ (forall_congr' $ fun hy ↦ ?_)
+  rw [Algebra.trace_eq_of_equiv_equiv (FractionRing.algEquiv A K).toRingEquiv
+    (FractionRing.algEquiv B L).toRingEquiv]
+  swap
+  · apply IsLocalization.ringHom_ext (M := A⁰); ext
+    simp only [AlgEquiv.toRingEquiv_eq_coe, AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_comp,
+      RingHom.coe_coe, Function.comp_apply, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
+    rw [IsScalarTower.algebraMap_apply A B (FractionRing B), AlgEquiv.commutes,
+      ← IsScalarTower.algebraMap_apply]
+  simp only [AlgEquiv.toRingEquiv_eq_coe, _root_.map_mul, AlgEquiv.coe_ringEquiv,
+    AlgEquiv.apply_symm_apply]
+  show (FractionRing.algEquiv A K).symm _ ∈ (algebraMap A (FractionRing A)).range ↔ _
+  rw [← (FractionRing.algEquiv A K).symm.toAlgHom.comp_algebraMap, ← RingHom.map_range,
+    AlgEquiv.toAlgHom_eq_coe, AlgEquiv.coe_ringHom_commutes, Subring.mem_map_equiv]
+  simp
+
 open scoped Classical
 
 namespace FractionalIdeal
@@ -176,11 +205,13 @@ def dual (I : FractionalIdeal B⁰ L) :
       · ext w; exact (IsIntegralClosure.isIntegral_iff (A := B)).symm
       · rw [Algebra.smul_def, RingHom.map_mul, hy, ← Algebra.smul_def]⟩
 
-variable [IsDedekindDomain B] {A K} {I J : FractionalIdeal B⁰ L} (hI : I ≠ 0) (hJ : J ≠ 0)
+variable [IsDedekindDomain B] {I J : FractionalIdeal B⁰ L} (hI : I ≠ 0) (hJ : J ≠ 0)
 
 lemma coe_dual :
     (dual A K I : Submodule B L) = Iᵛ := by rw [dual, dif_neg hI]; rfl
 
+variable (B L)
+
 @[simp]
 lemma coe_dual_one :
     (dual A K (1 : FractionalIdeal B⁰ L) : Submodule B L) = 1ᵛ := by
@@ -191,10 +222,14 @@ lemma coe_dual_one :
 lemma dual_zero :
     dual A K (0 : FractionalIdeal B⁰ L) = 0 := by rw [dual, dif_pos rfl]
 
+variable {A K L B}
+
 lemma mem_dual {x} :
     x ∈ dual A K I ↔ ∀ a ∈ I, traceForm K L x a ∈ (algebraMap A K).range := by
   rw [dual, dif_neg hI]; rfl
 
+variable (A K)
+
 lemma dual_ne_zero :
     dual A K I ≠ 0 := by
   obtain ⟨b, hb, hb'⟩ := I.prop
@@ -213,13 +248,18 @@ lemma dual_ne_zero :
     exact IsIntegralClosure.isIntegral_iff (A := B)
   · exact (Algebra.smul_def _ _).symm
 
+variable {A K}
+
 @[simp]
 lemma dual_eq_zero_iff :
-    dual A K I = 0 ↔ I = 0 := ⟨not_imp_not.mp dual_ne_zero, fun e ↦ e.symm ▸ dual_zero⟩
+    dual A K I = 0 ↔ I = 0 :=
+  ⟨not_imp_not.mp (dual_ne_zero A K), fun e ↦ e.symm ▸ dual_zero A K L B⟩
 
 lemma dual_ne_zero_iff :
     dual A K I ≠ 0 ↔ I ≠ 0 := dual_eq_zero_iff.not
 
+variable (A K)
+
 lemma le_dual_inv_aux (hIJ : I * J ≤ 1) :
     J ≤ dual A K I := by
   rw [dual, dif_neg hI]
@@ -233,42 +273,42 @@ lemma le_dual_inv_aux (hIJ : I * J ≤ 1) :
 
 lemma one_le_dual_one :
     1 ≤ dual A K (1 : FractionalIdeal B⁰ L) :=
-  le_dual_inv_aux one_ne_zero (by rw [one_mul])
+  le_dual_inv_aux A K one_ne_zero (by rw [one_mul])
 
 lemma le_dual_iff :
     I ≤ dual A K J ↔ I * J ≤ dual A K 1 := by
   by_cases hI : I = 0
   · simp [hI, zero_le]
-  rw [← coe_le_coe, ← coe_le_coe, coe_mul, coe_dual hJ, coe_dual_one, le_traceDual]
+  rw [← coe_le_coe, ← coe_le_coe, coe_mul, coe_dual A K hJ, coe_dual_one, le_traceDual]
 
 variable (I)
 
 lemma inv_le_dual :
     I⁻¹ ≤ dual A K I :=
-  if hI : I = 0 then by simp [hI] else le_dual_inv_aux hI (le_of_eq (mul_inv_cancel hI))
+  if hI : I = 0 then by simp [hI] else le_dual_inv_aux A K hI (le_of_eq (mul_inv_cancel hI))
 
 lemma dual_inv_le :
     (dual A K I)⁻¹ ≤ I := by
   by_cases hI : I = 0; · simp [hI]
   convert mul_right_mono ((dual A K I)⁻¹)
-    (mul_left_mono I (inv_le_dual (A := A) (K := K) I)) using 1
+    (mul_left_mono I (inv_le_dual A K I)) using 1
   · simp only [mul_inv_cancel hI, one_mul]
-  · simp only [mul_inv_cancel (dual_ne_zero (hI := hI)), mul_assoc, mul_one]
+  · simp only [mul_inv_cancel (dual_ne_zero A K (hI := hI)), mul_assoc, mul_one]
 
 lemma dual_eq_mul_inv :
     dual A K I = dual A K 1 * I⁻¹ := by
   by_cases hI : I = 0; · simp [hI]
   apply le_antisymm
   · suffices : dual A K I * I ≤ dual A K 1
     · convert mul_right_mono I⁻¹ this using 1; simp only [mul_inv_cancel hI, mul_one, mul_assoc]
-    rw [← le_dual_iff hI]
-  rw [le_dual_iff hI, mul_assoc, inv_mul_cancel hI, mul_one]
+    rw [← le_dual_iff A K hI]
+  rw [le_dual_iff A K hI, mul_assoc, inv_mul_cancel hI, mul_one]
 
 variable {I}
 
 lemma dual_div_dual :
     dual A K J / dual A K I = I / J := by
-  rw [dual_eq_mul_inv J, dual_eq_mul_inv I, mul_div_mul_comm, div_self, one_mul]
+  rw [dual_eq_mul_inv A K J, dual_eq_mul_inv A K I, mul_div_mul_comm, div_self, one_mul]
   exact inv_div_inv J I
   simp only [ne_eq, dual_eq_zero_iff, one_ne_zero, not_false_eq_true]
 
@@ -278,7 +318,7 @@ lemma dual_mul_self :
 
 lemma self_mul_dual :
     I * dual A K I = dual A K 1 := by
-  rw [mul_comm, dual_mul_self hI]
+  rw [mul_comm, dual_mul_self A K hI]
 
 lemma dual_inv :
     dual A K I⁻¹ = dual A K 1 * I := by rw [dual_eq_mul_inv, inv_inv]
@@ -288,25 +328,107 @@ variable (I)
 @[simp]
 lemma dual_dual :
     dual A K (dual A K I) = I := by
-  rw [dual_eq_mul_inv, dual_eq_mul_inv (I := I), mul_inv, inv_inv, ← mul_assoc, mul_inv_cancel,
+  rw [dual_eq_mul_inv, dual_eq_mul_inv A K (I := I), mul_inv, inv_inv, ← mul_assoc, mul_inv_cancel,
     one_mul]
   rw [dual_ne_zero_iff]
   exact one_ne_zero
 
-lemma dual_involutive :
-    Function.Involutive (dual A K : FractionalIdeal B⁰ L → FractionalIdeal B⁰ L) := dual_dual
-
-lemma dual_injective :
-    Function.Injective (dual A K : FractionalIdeal B⁰ L → FractionalIdeal B⁰ L) :=
-  dual_involutive.injective
-
 variable {I}
 
 @[simp]
 lemma dual_le_dual :
     dual A K I ≤ dual A K J ↔ J ≤ I := by
-  nth_rewrite 2 [← dual_dual (A := A) (K := K) I]
-  rw [le_dual_iff hJ, le_dual_iff (I := J), mul_comm]
-  rwa [dual_ne_zero_iff]
+  nth_rewrite 2 [← dual_dual A K I]
+  rw [le_dual_iff A K hJ, le_dual_iff A K (I := J) (by rwa [dual_ne_zero_iff]), mul_comm]
+
+variable {A K}
+
+lemma dual_involutive :
+    Function.Involutive (dual A K : FractionalIdeal B⁰ L → FractionalIdeal B⁰ L) := dual_dual A K
+
+lemma dual_injective :
+    Function.Injective (dual A K : FractionalIdeal B⁰ L → FractionalIdeal B⁰ L) :=
+  dual_involutive.injective
 
 end FractionalIdeal
+
+variable (B)
+variable [IsDedekindDomain B]
+
+/-- The different ideal of an extension of integral domains `B/A` is the inverse of the dual of `A`
+as an ideal of `B`. See `coeIdeal_differentIdeal` and `coeSubmodule_differentIdeal`. -/
+def differentIdeal [NoZeroSMulDivisors A B] : Ideal B :=
+  (1 / Submodule.traceDual A (FractionRing A) 1 : Submodule B (FractionRing B)).comap
+    (Algebra.linearMap B (FractionRing B))
+
+lemma coeSubmodule_differentIdeal_fractionRing
+    [NoZeroSMulDivisors A B] (hAB : Algebra.IsIntegral A B)
+    [IsSeparable (FractionRing A) (FractionRing B)]
+    [FiniteDimensional (FractionRing A) (FractionRing B)] :
+    coeSubmodule (FractionRing B) (differentIdeal A B) =
+      1 / Submodule.traceDual A (FractionRing A) 1 := by
+  have : IsIntegralClosure B A (FractionRing B) :=
+    IsIntegralClosure.of_isIntegrallyClosed _ _ _ hAB
+  rw [coeSubmodule, differentIdeal, Submodule.map_comap_eq, inf_eq_right]
+  have := FractionalIdeal.dual_inv_le (A := A) (K := FractionRing A)
+    (1 : FractionalIdeal B⁰ (FractionRing B))
+  have : _ ≤ ((1 : FractionalIdeal B⁰ (FractionRing B)) : Submodule B (FractionRing B)) := this
+  simp only [← one_div, FractionalIdeal.val_eq_coe] at this
+  rw [FractionalIdeal.coe_div (FractionalIdeal.dual_ne_zero _ _ _),
+    FractionalIdeal.coe_dual] at this
+  simpa only [FractionalIdeal.coe_one] using this
+  · exact one_ne_zero
+  · exact one_ne_zero
+
+lemma coeSubmodule_differentIdeal [NoZeroSMulDivisors A B] :
+    coeSubmodule L (differentIdeal A B) = 1 / Submodule.traceDual A K 1 := by
+  have : (FractionRing.algEquiv B L).toLinearEquiv.comp (Algebra.linearMap B (FractionRing B)) =
+    Algebra.linearMap B L := by ext; simp
+  rw [coeSubmodule, ← this]
+  have H : RingHom.comp (algebraMap (FractionRing A) (FractionRing B))
+    ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
+      RingHom.comp ↑(FractionRing.algEquiv B L).symm.toRingEquiv (algebraMap K L)
+  · apply IsLocalization.ringHom_ext A⁰
+    ext
+    simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
+      AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes,
+      ← IsScalarTower.algebraMap_apply]
+    rw [IsScalarTower.algebraMap_apply A B L, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]
+  have : IsSeparable (FractionRing A) (FractionRing B) := IsSeparable.of_equiv_equiv _ _ H
+  have : FiniteDimensional (FractionRing A) (FractionRing B) := Module.Finite.of_equiv_equiv _ _ H
+  simp only [AlgEquiv.toLinearEquiv_toLinearMap, Submodule.map_comp]
+  rw [← coeSubmodule, coeSubmodule_differentIdeal_fractionRing _ _
+      (IsIntegralClosure.isIntegral_algebra _ L),
+    Submodule.map_div, ← AlgEquiv.toAlgHom_toLinearMap, Submodule.map_one]
+  congr 1
+  refine (map_equiv_traceDual A K _).trans ?_
+  congr 1
+  ext
+  simp
+
+variable (L)
+
+lemma coeIdeal_differentIdeal [NoZeroSMulDivisors A B] :
+    ↑(differentIdeal A B) = (FractionalIdeal.dual A K (1 : FractionalIdeal B⁰ L))⁻¹ := by
+  apply FractionalIdeal.coeToSubmodule_injective
+  simp only [FractionalIdeal.coe_div
+    (FractionalIdeal.dual_ne_zero _ _ (@one_ne_zero (FractionalIdeal B⁰ L) _ _ _)),
+    FractionalIdeal.coe_coeIdeal, coeSubmodule_differentIdeal A K, inv_eq_one_div,
+    FractionalIdeal.coe_dual_one, FractionalIdeal.coe_one]
+
+variable {A K B L}
+
+lemma differentialIdeal_le_fractionalIdeal_iff
+    {I : FractionalIdeal B⁰ L} (hI : I ≠ 0) [NoZeroSMulDivisors A B] :
+    differentIdeal A B ≤ I ↔ (((I⁻¹ : _) : Submodule B L).restrictScalars A).map
+      ((Algebra.trace K L).restrictScalars A) ≤ 1 := by
+  rw [coeIdeal_differentIdeal A K L B, FractionalIdeal.inv_le_comm (by simp) hI,
+    ← FractionalIdeal.coe_le_coe, FractionalIdeal.coe_dual_one]
+  refine le_traceDual_iff_map_le_one.trans ?_
+  simp
+
+lemma differentialIdeal_le_iff {I : Ideal B} (hI : I ≠ ⊥) [NoZeroSMulDivisors A B] :
+    differentIdeal A B ≤ I ↔ (((I⁻¹ : FractionalIdeal B⁰ L) : Submodule B L).restrictScalars A).map
+      ((Algebra.trace K L).restrictScalars A) ≤ 1 :=
+  (FractionalIdeal.coeIdeal_le_coeIdeal _).symm.trans
+    (differentialIdeal_le_fractionalIdeal_iff (I := (I : FractionalIdeal B⁰ L)) (by simpa))

Mathlib/RingTheory/DedekindDomain/Ideal.lean

@@ -768,9 +768,18 @@ theorem Associates.le_singleton_iff (x : A) (n : ℕ) (I : Ideal A) :
     Ideal.dvd_span_singleton]
 #align associates.le_singleton_iff Associates.le_singleton_iff
 
+variable {K}
+
+lemma FractionalIdeal.le_inv_comm {I J : FractionalIdeal A⁰ K} (hI : I ≠ 0) (hJ : J ≠ 0) :
+    I ≤ J⁻¹ ↔ J ≤ I⁻¹ := by
+  rw [inv_eq, inv_eq, le_div_iff_mul_le hI, le_div_iff_mul_le hJ, mul_comm]
+
+lemma FractionalIdeal.inv_le_comm {I J : FractionalIdeal A⁰ K} (hI : I ≠ 0) (hJ : J ≠ 0) :
+    I⁻¹ ≤ J ↔ J⁻¹ ≤ I := by
+  simpa using le_inv_comm (A := A) (K := K) (inv_ne_zero hI) (inv_ne_zero hJ)
+
 open FractionalIdeal
 
-variable {K}
 
 /-- Strengthening of `IsLocalization.exist_integer_multiples`:
 Let `J ≠ ⊤` be an ideal in a Dedekind domain `A`, and `f ≠ 0` a finite collection

Mathlib/RingTheory/Finiteness.lean

@@ -657,6 +657,19 @@ theorem trans {R : Type*} (A M : Type*) [CommSemiring R] [Semiring A] [Algebra R
             Submodule.restrictScalars_top]⟩⟩
 #align module.finite.trans Module.Finite.trans
 
+lemma of_equiv_equiv {A₁ B₁ A₂ B₂ : Type*} [CommRing A₁] [CommRing B₁]
+    [CommRing A₂] [CommRing B₂] [Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂)
+    (he : RingHom.comp (algebraMap A₂ B₂) ↑e₁ = RingHom.comp ↑e₂ (algebraMap A₁ B₁))
+    [Module.Finite A₁ B₁] : Module.Finite A₂ B₂ := by
+  letI := e₁.toRingHom.toAlgebra
+  letI := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
+  haveI : IsScalarTower A₁ A₂ B₁ := IsScalarTower.of_algebraMap_eq
+    (fun x ↦ by simp [RingHom.algebraMap_toAlgebra])
+  let e : B₁ ≃ₐ[A₂] B₂ := { e₂ with commutes' := fun r ↦ by simpa [RingHom.algebraMap_toAlgebra]
+                                                  using FunLike.congr_fun he.symm (e₁.symm r) }
+  haveI := Module.Finite.of_restrictScalars_finite A₁ A₂ B₁
+  exact Module.Finite.equiv e.toLinearEquiv
+
 end Algebra
 
 end Finite

Mathlib/RingTheory/IntegrallyClosed.lean

@@ -79,7 +79,7 @@ end Iff
 
 namespace IsIntegrallyClosed
 
-variable {R : Type*} [CommRing R] [id : IsDomain R] [iic : IsIntegrallyClosed R]
+variable {R S : Type*} [CommRing R] [CommRing S] [id : IsDomain R] [iic : IsIntegrallyClosed R]
 
 variable {K : Type*} [CommRing K] [Algebra R K] [ifr : IsFractionRing R K]
 
@@ -101,7 +101,17 @@ theorem exists_algebraMap_eq_of_pow_mem_subalgebra {K : Type*} [CommRing K] [Alg
   exists_algebraMap_eq_of_isIntegral_pow hn <| isIntegral_iff.mpr ⟨⟨x ^ n, hx⟩, rfl⟩
 #align is_integrally_closed.exists_algebra_map_eq_of_pow_mem_subalgebra IsIntegrallyClosed.exists_algebraMap_eq_of_pow_mem_subalgebra
 
-variable (K)
+variable (R S K)
+
+lemma _root_.IsIntegralClosure.of_isIntegrallyClosed
+    [Algebra S R] [Algebra S K] [IsScalarTower S R K] (hRS : Algebra.IsIntegral S R) :
+    IsIntegralClosure R S K := by
+  refine ⟨IsLocalization.injective _ le_rfl, fun {x} ↦
+    ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (IsIntegral.tower_top (A := R) hx), ?_⟩⟩
+  rintro ⟨y, rfl⟩
+  exact IsIntegral.map (IsScalarTower.toAlgHom S R K) (hRS y)
+
+variable {R}
 
 theorem integralClosure_eq_bot_iff : integralClosure R K = ⊥ ↔ IsIntegrallyClosed R := by
   refine' eq_bot_iff.trans _