From a9b268f6d9ab29307631902be31bb9aca0ddf72e Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sat, 26 Oct 2024 13:22:39 +0000 Subject: [PATCH] =?UTF-8?q?refactor:=20change=20the=20definition=20of=20`1?= =?UTF-8?q?=20:=20Submodule=20R=20A`=20to=20the=20range=20of=20`(=C2=B7=20?= =?UTF-8?q?=E2=80=A2=201)`=20(#18092)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Previously, it's defined to be the range of `algebraMap R A`. In the noncommutative setting, we want to write `1 : Ideal R` where `Ideal R := Submodule R R`, but `R` isn't an `R`-algebra if `R` is not commutative. If we were to introduce a new typeclass by removing the `commutes'` field from `Algebra`, we could keep the current definition, but I'd argue that it's still better to use SMul to define `1 : Submodule R A`, because `Submodule` only depends on the Module/SMul, not on the algebraMap/RingHom. Requires fixes in 11 other files. --- Mathlib/Algebra/Algebra/Bilinear.lean | 3 + Mathlib/Algebra/Algebra/Operations.lean | 75 +++++++++++-------- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean | 7 +- .../BilinearForm/DualLattice.lean | 8 +- .../CliffordAlgebra/Grading.lean | 4 +- .../Dimension/FreeAndStrongRankCondition.lean | 3 +- .../LinearAlgebra/ExteriorAlgebra/Basic.lean | 3 +- Mathlib/LinearAlgebra/LinearDisjoint.lean | 4 +- .../LinearAlgebra/TensorAlgebra/Basic.lean | 2 +- .../TensorProduct/Submodule.lean | 20 +++-- .../RingTheory/DedekindDomain/Different.lean | 14 ++-- .../DedekindDomain/IntegralClosure.lean | 2 +- Mathlib/RingTheory/FractionalIdeal/Basic.lean | 2 +- 13 files changed, 87 insertions(+), 60 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Bilinear.lean b/Mathlib/Algebra/Algebra/Bilinear.lean index 65e3fda3f286f..82c8c45e63e1c 100644 --- a/Mathlib/Algebra/Algebra/Bilinear.lean +++ b/Mathlib/Algebra/Algebra/Bilinear.lean @@ -215,6 +215,9 @@ theorem pow_mulRight (a : A) (n : ℕ) : mulRight R a ^ n = mulRight R (a ^ n) : exact LinearMap.coe_injective (((mulRight R a).coe_pow n).symm ▸ mul_right_iterate a n) +theorem toSpanSingleton_eq_algebra_linearMap : toSpanSingleton R A 1 = Algebra.linearMap R A := by + ext; simp + end Semiring section Ring diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean index ce82654752d9f..a962fa9ac33d8 100644 --- a/Mathlib/Algebra/Algebra/Operations.lean +++ b/Mathlib/Algebra/Algebra/Operations.lean @@ -36,6 +36,11 @@ It is proved that `Submodule R A` is a semiring, and also an algebra over `Set A Additionally, in the `Pointwise` locale we promote `Submodule.pointwiseDistribMulAction` to a `MulSemiringAction` as `Submodule.pointwiseMulSemiringAction`. +When `R` is not necessarily commutative, and `A` is merely a `R`-module with a ring structure +such that `IsScalarTower R A A` holds (equivalent to the data of a ring homomorphism `R →+* A` +by `ringHomEquivModuleIsScalarTower`), we can still define `1 : Submodule R A` and +`Mul (Submodule R A)`, but `1` is only a left identity, not necessarily a right one. + ## Tags multiplication of submodules, division of submodules, submodule semiring @@ -62,49 +67,57 @@ end SubMulAction namespace Submodule -variable {ι : Sort uι} -variable {R : Type u} [CommSemiring R] - -section Ring +section Module -variable {A : Type v} [Semiring A] [Algebra R A] -variable (S T : Set A) {M N P Q : Submodule R A} {m n : A} +variable {R : Type u} [Semiring R] {A : Type v} [Semiring A] [Module R A] -/-- `1 : Submodule R A` is the submodule R of A. -/ +/-- `1 : Submodule R A` is the submodule `R ∙ 1` of A. +TODO: potentially change this back to `LinearMap.range (Algebra.linearMap R A)` +once a version of `Algebra` without the `commutes'` field is introduced. +See issue #18110. +-/ instance one : One (Submodule R A) := - -- Porting note: `f.range` notation doesn't work - ⟨LinearMap.range (Algebra.linearMap R A)⟩ + ⟨LinearMap.range (LinearMap.toSpanSingleton R A 1)⟩ -theorem one_eq_range : (1 : Submodule R A) = LinearMap.range (Algebra.linearMap R A) := - rfl +theorem one_eq_span : (1 : Submodule R A) = R ∙ 1 := + (LinearMap.span_singleton_eq_range _ _ _).symm theorem le_one_toAddSubmonoid : 1 ≤ (1 : Submodule R A).toAddSubmonoid := by rintro x ⟨n, rfl⟩ - exact ⟨n, map_natCast (algebraMap R A) n⟩ - -theorem algebraMap_mem (r : R) : algebraMap R A r ∈ (1 : Submodule R A) := - LinearMap.mem_range_self (Algebra.linearMap R A) _ - -@[simp] -theorem mem_one {x : A} : x ∈ (1 : Submodule R A) ↔ ∃ y, algebraMap R A y = x := - Iff.rfl + exact ⟨n, show (n : R) • (1 : A) = n by rw [Nat.cast_smul_eq_nsmul, nsmul_one]⟩ @[simp] theorem toSubMulAction_one : (1 : Submodule R A).toSubMulAction = 1 := - SetLike.ext fun _ => mem_one.trans SubMulAction.mem_one'.symm - -theorem one_eq_span : (1 : Submodule R A) = R ∙ 1 := by - apply Submodule.ext - intro a - simp only [mem_one, mem_span_singleton, Algebra.smul_def, mul_one] + SetLike.ext fun _ ↦ by rw [one_eq_span, SubMulAction.mem_one]; exact mem_span_singleton theorem one_eq_span_one_set : (1 : Submodule R A) = span R 1 := one_eq_span -theorem one_le : (1 : Submodule R A) ≤ P ↔ (1 : A) ∈ P := by +theorem one_le {P : Submodule R A} : (1 : Submodule R A) ≤ P ↔ (1 : A) ∈ P := by -- Porting note: simpa no longer closes refl goals, so added `SetLike.mem_coe` simp only [one_eq_span, span_le, Set.singleton_subset_iff, SetLike.mem_coe] +end Module + +variable {ι : Sort uι} +variable {R : Type u} [CommSemiring R] + +section AlgebraSemiring + +variable {A : Type v} [Semiring A] [Algebra R A] +variable (S T : Set A) {M N P Q : Submodule R A} {m n : A} + +theorem one_eq_range : (1 : Submodule R A) = LinearMap.range (Algebra.linearMap R A) := by + rw [one_eq_span, LinearMap.span_singleton_eq_range, + LinearMap.toSpanSingleton_eq_algebra_linearMap] + +theorem algebraMap_mem (r : R) : algebraMap R A r ∈ (1 : Submodule R A) := by + rw [one_eq_range]; exact LinearMap.mem_range_self _ _ + +@[simp] +theorem mem_one {x : A} : x ∈ (1 : Submodule R A) ↔ ∃ y, algebraMap R A y = x := by + rw [one_eq_range]; rfl + protected theorem map_one {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') : map f.toLinearMap (1 : Submodule R A) = 1 := by ext @@ -423,7 +436,7 @@ protected theorem pow_induction_on_left' {C : ∀ (n : ℕ) (x), x ∈ M ^ n → induction n generalizing x with | zero => rw [pow_zero] at hx - obtain ⟨r, rfl⟩ := hx + obtain ⟨r, rfl⟩ := mem_one.mp hx exact algebraMap r | succ n n_ih => revert hx @@ -444,7 +457,7 @@ protected theorem pow_induction_on_right' {C : ∀ (n : ℕ) (x), x ∈ M ^ n induction n generalizing x with | zero => rw [pow_zero] at hx - obtain ⟨r, rfl⟩ := hx + obtain ⟨r, rfl⟩ := mem_one.mp hx exact algebraMap r | succ n n_ih => revert hx @@ -549,9 +562,9 @@ scoped[Pointwise] attribute [instance] Submodule.pointwiseMulSemiringAction end -end Ring +end AlgebraSemiring -section CommRing +section AlgebraCommSemiring variable {A : Type v} [CommSemiring A] [Algebra R A] variable {M N : Submodule R A} {m n : A} @@ -687,6 +700,6 @@ protected theorem map_div {B : Type*} [CommSemiring B] [Algebra R B] (I J : Subm end Quotient -end CommRing +end AlgebraCommSemiring end Submodule diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean index a34f329d35336..7683b0c0af36d 100644 --- a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean +++ b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean @@ -776,7 +776,9 @@ instance : Inhabited (Subalgebra R A) := ⟨⊥⟩ theorem mem_bot {x : A} : x ∈ (⊥ : Subalgebra R A) ↔ x ∈ Set.range (algebraMap R A) := Iff.rfl -theorem toSubmodule_bot : Subalgebra.toSubmodule (⊥ : Subalgebra R A) = 1 := rfl +/-- TODO: change proof to `rfl` when fixing #18110. -/ +theorem toSubmodule_bot : Subalgebra.toSubmodule (⊥ : Subalgebra R A) = 1 := + Submodule.one_eq_range.symm @[simp] theorem coe_bot : ((⊥ : Subalgebra R A) : Set A) = Set.range (algebraMap R A) := rfl @@ -799,7 +801,8 @@ theorem map_top (f : A →ₐ[R] B) : (⊤ : Subalgebra R A).map f = f.range := @[simp] theorem map_bot (f : A →ₐ[R] B) : (⊥ : Subalgebra R A).map f = ⊥ := - Subalgebra.toSubmodule_injective <| Submodule.map_one _ + Subalgebra.toSubmodule_injective <| by + simpa only [Subalgebra.map_toSubmodule, toSubmodule_bot] using Submodule.map_one _ @[simp] theorem comap_top (f : A →ₐ[R] B) : (⊤ : Subalgebra R B).comap f = ⊤ := diff --git a/Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean b/Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean index 24c02406a750c..8fba55a7ccff6 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean @@ -51,12 +51,12 @@ lemma le_flip_dualSubmodule {N₁ N₂ : Submodule R M} : This is bundled as a bilinear map in `BilinForm.dualSubmoduleToDual`. -/ noncomputable def dualSubmoduleParing {N : Submodule R M} (x : B.dualSubmodule N) (y : N) : R := - (x.prop y y.prop).choose + (Submodule.mem_one.mp <| x.prop y y.prop).choose @[simp] lemma dualSubmoduleParing_spec {N : Submodule R M} (x : B.dualSubmodule N) (y : N) : algebraMap R S (B.dualSubmoduleParing x y) = B x y := - (x.prop y y.prop).choose_spec + (Submodule.mem_one.mp <| x.prop y y.prop).choose_spec /-- The natural paring of `B.dualSubmodule N` and `N`. -/ -- TODO: Show that this is perfect when `N` is a lattice and `B` is nondegenerate. @@ -94,7 +94,7 @@ lemma dualSubmodule_span_of_basis {ι} [Finite ι] [DecidableEq ι] rw [← (B.dualBasis hB b).sum_repr x] apply sum_mem rintro i - - obtain ⟨r, hr⟩ := hx (b i) (Submodule.subset_span ⟨_, rfl⟩) + obtain ⟨r, hr⟩ := Submodule.mem_one.mp <| hx (b i) (Submodule.subset_span ⟨_, rfl⟩) simp only [dualBasis_repr_apply, ← hr, Algebra.linearMap_apply, algebraMap_smul] apply Submodule.smul_mem exact Submodule.subset_span ⟨_, rfl⟩ @@ -107,7 +107,7 @@ lemma dualSubmodule_span_of_basis {ι} [Finite ι] [DecidableEq ι] rw [← IsScalarTower.algebraMap_smul S (f j), map_smul] simp_rw [apply_dualBasis_left] rw [smul_eq_mul, mul_ite, mul_one, mul_zero, ← (algebraMap R S).map_zero, ← apply_ite] - exact ⟨_, rfl⟩ + exact Submodule.mem_one.mpr ⟨_, rfl⟩ lemma dualSubmodule_dualSubmodule_flip_of_basis {ι : Type*} [Finite ι] (hB : B.Nondegenerate) (b : Basis ι S M) : diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean index 145bb1e7b4a15..e0cba62521842 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean @@ -197,8 +197,8 @@ theorem even_induction {motive : ∀ x, x ∈ evenOdd Q 0 → Prop} motive (ι Q m₁ * ι Q m₂ * x) (zero_add (0 : ZMod 2) ▸ SetLike.mul_mem_graded (ι_mul_ι_mem_evenOdd_zero Q m₁ m₂) hx)) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) : motive x hx := by - refine evenOdd_induction _ _ (motive := motive) (fun rx => ?_) add ι_mul_ι_mul x hx - rintro ⟨r, rfl⟩ + refine evenOdd_induction _ _ (motive := motive) (fun rx h => ?_) add ι_mul_ι_mul x hx + obtain ⟨r, rfl⟩ := Submodule.mem_one.mp h exact algebraMap r /-- To show a property is true on the odd parts, it suffices to show it is true on the diff --git a/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean b/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean index 43e1a1eedf450..212770aa65383 100644 --- a/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean +++ b/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean @@ -271,7 +271,8 @@ theorem rank_eq_one_iff [Nontrivial E] [Module.Free F S] : Module.rank F S = 1 obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := F) (M := (⊥ : Subalgebra F E)) refine le_antisymm ?_ ?_ · have := lift_rank_range_le (Algebra.linearMap F E) - rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff] at this + rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff, + ← Algebra.toSubmodule_bot, rank_toSubmodule] at this · by_contra H rw [not_le, lt_one_iff_zero] at H haveI := mk_eq_zero_iff.1 (H ▸ b.mk_eq_rank'') diff --git a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean index 75b12c7d91e55..b81a28f1405ee 100644 --- a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean @@ -239,7 +239,8 @@ theorem ι_range_disjoint_one : Disjoint (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M)) (1 : Submodule R (ExteriorAlgebra R M)) := by rw [Submodule.disjoint_def] - rintro _ ⟨x, hx⟩ ⟨r, rfl : algebraMap R (ExteriorAlgebra R M) r = _⟩ + rintro _ ⟨x, hx⟩ h + obtain ⟨r, rfl : algebraMap R (ExteriorAlgebra R M) r = _⟩ := Submodule.mem_one.mp h rw [ι_eq_algebraMap_iff x] at hx rw [hx.2, RingHom.map_zero] diff --git a/Mathlib/LinearAlgebra/LinearDisjoint.lean b/Mathlib/LinearAlgebra/LinearDisjoint.lean index f290e4e777d86..efcf71db426f2 100644 --- a/Mathlib/LinearAlgebra/LinearDisjoint.lean +++ b/Mathlib/LinearAlgebra/LinearDisjoint.lean @@ -232,12 +232,12 @@ theorem bot_right : M.LinearDisjoint (⊥ : Submodule R S) := /-- The image of `R` in `S` is linearly disjoint with any other submodules. -/ theorem one_left : (1 : Submodule R S).LinearDisjoint N := by - rw [linearDisjoint_iff, mulMap_one_left_eq] + rw [linearDisjoint_iff, ← Algebra.toSubmodule_bot, mulMap_one_left_eq] exact N.injective_subtype.comp N.lTensorOne.injective /-- The image of `R` in `S` is linearly disjoint with any other submodules. -/ theorem one_right : M.LinearDisjoint (1 : Submodule R S) := by - rw [linearDisjoint_iff, mulMap_one_right_eq] + rw [linearDisjoint_iff, ← Algebra.toSubmodule_bot, mulMap_one_right_eq] exact M.injective_subtype.comp M.rTensorOne.injective /-- If for any finitely generated submodules `M'` of `M`, `M'` and `N` are linearly disjoint, diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean index 9355d09c2992a..f24b144938533 100644 --- a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean @@ -288,7 +288,7 @@ theorem ι_ne_one [Nontrivial R] (x : M) : ι R x ≠ 1 := by theorem ι_range_disjoint_one : Disjoint (LinearMap.range (ι R : M →ₗ[R] TensorAlgebra R M)) (1 : Submodule R (TensorAlgebra R M)) := by - rw [Submodule.disjoint_def] + rw [Submodule.disjoint_def, Submodule.one_eq_range] rintro _ ⟨x, hx⟩ ⟨r, rfl⟩ rw [Algebra.linearMap_apply, ι_eq_algebraMap_iff] at hx rw [hx.2, map_zero] diff --git a/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean b/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean index 838f15025ec00..074c5389f0f01 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean @@ -121,8 +121,9 @@ theorem mulMap'_surjective : Function.Surjective (mulMap' M N) := by `i(R) ⊗[R] N →ₗ[R] N` induced by multiplication in `S`, here `i : R → S` is the structure map. This is promoted to an isomorphism of `R`-modules as `Submodule.lTensorOne`. Use that instead. -/ def lTensorOne' : (⊥ : Subalgebra R S) ⊗[R] N →ₗ[R] N := - show (1 : Submodule R S) ⊗[R] N →ₗ[R] N from - (LinearEquiv.ofEq _ _ (by rw [mulMap_range, one_mul])).toLinearMap ∘ₗ (mulMap _ N).rangeRestrict + show Subalgebra.toSubmodule ⊥ ⊗[R] N →ₗ[R] N from + (LinearEquiv.ofEq _ _ (by rw [Algebra.toSubmodule_bot, mulMap_range, one_mul])).toLinearMap ∘ₗ + (mulMap _ N).rangeRestrict variable {N} in @[simp] @@ -130,7 +131,7 @@ theorem lTensorOne'_tmul (y : R) (n : N) : N.lTensorOne' (algebraMap R _ y ⊗ₜ[R] n) = y • n := Subtype.val_injective <| by simp_rw [lTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul, Algebra.smul_def] - exact mulMap_tmul 1 N _ _ + exact mulMap_tmul _ N _ _ variable {N} in @[simp] @@ -163,15 +164,17 @@ variable {N} in @[simp] theorem lTensorOne_symm_apply (n : N) : N.lTensorOne.symm n = 1 ⊗ₜ[R] n := rfl -theorem mulMap_one_left_eq : mulMap 1 N = N.subtype ∘ₗ N.lTensorOne.toLinearMap := +theorem mulMap_one_left_eq : + mulMap (Subalgebra.toSubmodule ⊥) N = N.subtype ∘ₗ N.lTensorOne.toLinearMap := TensorProduct.ext' fun _ _ ↦ rfl /-- If `M` is a submodule in an algebra `S` over `R`, there is the natural `R`-linear map `M ⊗[R] i(R) →ₗ[R] M` induced by multiplication in `S`, here `i : R → S` is the structure map. This is promoted to an isomorphism of `R`-modules as `Submodule.rTensorOne`. Use that instead. -/ def rTensorOne' : M ⊗[R] (⊥ : Subalgebra R S) →ₗ[R] M := - show M ⊗[R] (1 : Submodule R S) →ₗ[R] M from - (LinearEquiv.ofEq _ _ (by rw [mulMap_range, mul_one])).toLinearMap ∘ₗ (mulMap M _).rangeRestrict + show M ⊗[R] Subalgebra.toSubmodule ⊥ →ₗ[R] M from + (LinearEquiv.ofEq _ _ (by rw [Algebra.toSubmodule_bot, mulMap_range, mul_one])).toLinearMap ∘ₗ + (mulMap M _).rangeRestrict variable {M} in @[simp] @@ -180,7 +183,7 @@ theorem rTensorOne'_tmul (y : R) (m : M) : simp_rw [rTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul] rw [Algebra.smul_def, Algebra.commutes] - exact mulMap_tmul M 1 _ _ + exact mulMap_tmul M _ _ _ variable {M} in @[simp] @@ -213,7 +216,8 @@ variable {M} in @[simp] theorem rTensorOne_symm_apply (m : M) : M.rTensorOne.symm m = m ⊗ₜ[R] 1 := rfl -theorem mulMap_one_right_eq : mulMap M 1 = M.subtype ∘ₗ M.rTensorOne.toLinearMap := +theorem mulMap_one_right_eq : + mulMap M (Subalgebra.toSubmodule ⊥) = M.subtype ∘ₗ M.rTensorOne.toLinearMap := TensorProduct.ext' fun _ _ ↦ rfl @[simp] diff --git a/Mathlib/RingTheory/DedekindDomain/Different.lean b/Mathlib/RingTheory/DedekindDomain/Different.lean index a9e9ad8924c5b..0abb74d5ac750 100644 --- a/Mathlib/RingTheory/DedekindDomain/Different.lean +++ b/Mathlib/RingTheory/DedekindDomain/Different.lean @@ -59,7 +59,7 @@ namespace Submodule lemma mem_traceDual {I : Submodule B L} {x} : x ∈ Iᵛ ↔ ∀ a ∈ I, traceForm K L x a ∈ (algebraMap A K).range := - Iff.rfl + forall₂_congr fun _ _ ↦ mem_one lemma le_traceDual_iff_map_le_one {I J : Submodule B L} : I ≤ Jᵛ ↔ ((I * J : Submodule B L).restrictScalars A).map @@ -149,14 +149,15 @@ variable [IsIntegrallyClosed A] lemma Submodule.mem_traceDual_iff_isIntegral {I : Submodule B L} {x} : x ∈ Iᵛ ↔ ∀ a ∈ I, IsIntegral A (traceForm K L x a) := - forall₂_congr (fun _ _ ↦ IsIntegrallyClosed.isIntegral_iff.symm) + forall₂_congr fun _ _ ↦ mem_one.trans IsIntegrallyClosed.isIntegral_iff.symm variable [FiniteDimensional K L] [IsIntegralClosure B A L] lemma Submodule.one_le_traceDual_one : (1 : Submodule B L) ≤ 1ᵛ := by - rw [le_traceDual_iff_map_le_one, mul_one] + rw [le_traceDual_iff_map_le_one, mul_one, one_eq_range] rintro _ ⟨x, ⟨x, rfl⟩, rfl⟩ + rw [mem_one] apply IsIntegrallyClosed.isIntegral_iff.mp apply isIntegral_trace rw [IsIntegralClosure.isIntegral_iff (A := B)] @@ -262,7 +263,7 @@ variable {A K L B} lemma mem_dual (hI : I ≠ 0) {x} : x ∈ dual A K I ↔ ∀ a ∈ I, traceForm K L x a ∈ (algebraMap A K).range := by - rw [dual, dif_neg hI]; rfl + rw [dual, dif_neg hI]; exact forall₂_congr fun _ _ ↦ mem_one variable (A K) @@ -300,6 +301,7 @@ lemma le_dual_inv_aux (hI : I ≠ 0) (hIJ : I * J ≤ 1) : J ≤ dual A K I := by rw [dual, dif_neg hI] intro x hx y hy + rw [mem_one] apply IsIntegrallyClosed.isIntegral_iff.mp apply isIntegral_trace rw [IsIntegralClosure.isIntegral_iff (A := B)] @@ -412,7 +414,7 @@ lemma coeSubmodule_differentIdeal_fractionRing 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 + · simpa only [FractionalIdeal.coe_one, Submodule.one_eq_range] using this · exact one_ne_zero · exact one_ne_zero @@ -559,7 +561,7 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B] derivative_map, aeval_map_algebraMap, aeval_algebraMap_apply, mul_assoc, FractionalIdeal.mem_one_iff, forall_exists_index, forall_apply_eq_imp_iff] simp_rw [← IsScalarTower.toAlgHom_apply A B L x, ← AlgHom.map_adjoin_singleton] - simp only [Subalgebra.mem_map, IsScalarTower.coe_toAlgHom', + simp only [Subalgebra.mem_map, IsScalarTower.coe_toAlgHom', Submodule.one_eq_range, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, ← _root_.map_mul] exact ⟨fun H b ↦ (mul_one b) ▸ H b 1 (one_mem _), fun H _ _ _ ↦ H _⟩ diff --git a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean index 86796148fbcf3..81f78b774ad8d 100644 --- a/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean +++ b/Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean @@ -95,7 +95,7 @@ theorem IsIntegralClosure.range_le_span_dualBasis [Algebra.IsSeparable K L] {ι rintro _ ⟨i, rfl⟩ _ ⟨y, rfl⟩ simp only [LinearMap.coe_restrictScalars, linearMap_apply, LinearMap.BilinForm.flip_apply, traceForm_apply] - refine IsIntegrallyClosed.isIntegral_iff.mp ?_ + refine Submodule.mem_one.mpr <| IsIntegrallyClosed.isIntegral_iff.mp ?_ exact isIntegral_trace ((IsIntegralClosure.isIntegral A L y).algebraMap.mul (hb_int i)) theorem integralClosure_le_span_dualBasis [Algebra.IsSeparable K L] {ι : Type*} [Fintype ι] diff --git a/Mathlib/RingTheory/FractionalIdeal/Basic.lean b/Mathlib/RingTheory/FractionalIdeal/Basic.lean index 4ebe1fa201f1f..4056634b451c7 100644 --- a/Mathlib/RingTheory/FractionalIdeal/Basic.lean +++ b/Mathlib/RingTheory/FractionalIdeal/Basic.lean @@ -215,7 +215,7 @@ theorem isFractional_of_le_one (I : Submodule R P) (h : I ≤ 1) : IsFractional use 1, S.one_mem intro b hb rw [one_smul] - obtain ⟨b', b'_mem, rfl⟩ := h hb + obtain ⟨b', b'_mem, rfl⟩ := mem_one.mp (h hb) exact Set.mem_range_self b' theorem isFractional_of_le {I : Submodule R P} {J : FractionalIdeal S P} (hIJ : I ≤ J) :