From 94d510ab4d29bbec7e9b54d213f352243377ee39 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 14 Oct 2024 00:08:20 +0200 Subject: [PATCH 01/23] refactor: generalize mul of Submodule and smul of Ideal on Submodule to noncommutative setting --- Mathlib/Algebra/Algebra/Bilinear.lean | 3 + Mathlib/Algebra/Algebra/Operations.lean | 337 +++++++------ Mathlib/Algebra/Group/Defs.lean | 12 + Mathlib/Algebra/Group/Subgroup/Pointwise.lean | 13 + .../Algebra/Group/Submonoid/Pointwise.lean | 64 ++- Mathlib/RingTheory/Ideal/Maps.lean | 112 +++- Mathlib/RingTheory/Ideal/Operations.lean | 477 ++++++++---------- Mathlib/RingTheory/JacobsonIdeal.lean | 25 +- 8 files changed, 607 insertions(+), 436 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 ed2b456a4db5b..4c3f77f73afb3 100644 --- a/Mathlib/Algebra/Algebra/Operations.lean +++ b/Mathlib/Algebra/Algebra/Operations.lean @@ -36,6 +36,10 @@ 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, 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,99 +66,58 @@ 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. -/ instance one : One (Submodule R A) := - -- Porting note: `f.range` notation doesn't work - ⟨LinearMap.range (Algebra.linearMap R A)⟩ + ⟨R ∙ 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 := rfl 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 mem_span_singleton.mpr + ⟨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] -protected theorem map_one {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') : - map f.toLinearMap (1 : Submodule R A) = 1 := by - ext - simp +variable [IsScalarTower R A A] -@[simp] -theorem map_op_one : - map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (1 : Submodule R A) = 1 := by - ext x - induction x - simp - -@[simp] -theorem comap_op_one : - comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (1 : Submodule R Aᵐᵒᵖ) = 1 := by - ext - simp +/-- Multiplication of sub-R-modules of an R-module A that is also a semiring. The submodule `M * N` +consists of finite sums of elements `m * n` for `m ∈ M` and `n ∈ N`. -/ +instance mul : Mul (Submodule R A) where + mul M N := + { __ := M.toAddSubmonoid * N.toAddSubmonoid + smul_mem' := fun r a ha ↦ AddSubmonoid.mul_induction_on ha + (fun m h n h' ↦ by rw [← smul_mul_assoc]; exact AddSubmonoid.mul_mem_mul (M.smul_mem r h) h') + fun a₁ a₂ h₁ h₂ ↦ by rw [smul_add]; apply (M.1 * N.1).add_mem h₁ h₂ } -@[simp] -theorem map_unop_one : - map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (1 : Submodule R Aᵐᵒᵖ) = 1 := by - rw [← comap_equiv_eq_map_symm, comap_op_one] - -@[simp] -theorem comap_unop_one : - comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (1 : Submodule R A) = 1 := by - rw [← map_equiv_eq_comap_symm, map_op_one] - -/-- Multiplication of sub-R-modules of an R-algebra A. The submodule `M * N` is the -smallest R-submodule of `A` containing the elements `m * n` for `m ∈ M` and `n ∈ N`. -/ -instance mul : Mul (Submodule R A) := - ⟨Submodule.map₂ <| LinearMap.mul R A⟩ +variable (S T : Set A) {M N P Q : Submodule R A} {m n : A} theorem mul_mem_mul (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N := - apply_mem_map₂ _ hm hn + AddSubmonoid.mul_mem_mul hm hn theorem mul_le : M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P := - map₂_le + AddSubmonoid.mul_le theorem mul_toAddSubmonoid (M N : Submodule R A) : - (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid := by - dsimp [HMul.hMul, Mul.mul] -- Porting note: added `hMul` - rw [map₂, iSup_toAddSubmonoid] - rfl + (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid := rfl @[elab_as_elim] protected theorem mul_induction_on {C : A → Prop} {r : A} (hr : r ∈ M * N) - (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)) (ha : ∀ x y, C x → C y → C (x + y)) : C r := by - rw [← mem_toAddSubmonoid, mul_toAddSubmonoid] at hr - exact AddSubmonoid.mul_induction_on hr hm ha + (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)) (ha : ∀ x y, C x → C y → C (x + y)) : C r := + AddSubmonoid.mul_induction_on hr hm ha /-- A dependent version of `mul_induction_on`. -/ @[elab_as_elim] @@ -168,61 +131,177 @@ protected theorem mul_induction_on' {C : ∀ r, r ∈ M * N → Prop} (fun x hx y hy => ⟨_, mem_mul_mem _ hx _ hy⟩) fun x y ⟨_, hx⟩ ⟨_, hy⟩ => ⟨_, add _ _ _ _ hx hy⟩ -variable (R) - -theorem span_mul_span : span R S * span R T = span R (S * T) := - map₂_span_span _ _ _ _ - -variable {R} -variable (M N P Q) +variable (M) @[simp] theorem mul_bot : M * ⊥ = ⊥ := - map₂_bot_right _ _ + toAddSubmonoid_injective (AddSubmonoid.mul_bot _) @[simp] theorem bot_mul : ⊥ * M = ⊥ := - map₂_bot_left _ _ + toAddSubmonoid_injective (AddSubmonoid.bot_mul _) -- @[simp] -- Porting note (#10618): simp can prove this once we have a monoid structure protected theorem one_mul : (1 : Submodule R A) * M = M := by - conv_lhs => rw [one_eq_span, ← span_eq M] - erw [span_mul_span, one_mul, span_eq] - --- @[simp] -- Porting note (#10618): simp can prove this once we have a monoid structure -protected theorem mul_one : M * 1 = M := by - conv_lhs => rw [one_eq_span, ← span_eq M] - erw [span_mul_span, mul_one, span_eq] + refine le_antisymm (mul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_ + · obtain ⟨r, rfl⟩ := mem_span_singleton.mp hr + rw [smul_one_mul]; exact M.smul_mem r hm + · rw [← one_mul m]; exact mul_mem_mul (subset_span rfl) hm -variable {M N P Q} +variable {M} @[mono] theorem mul_le_mul (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q := - map₂_le_map₂ hmp hnq + AddSubmonoid.mul_le_mul hmp hnq theorem mul_le_mul_left (h : M ≤ N) : M * P ≤ N * P := - map₂_le_map₂_left h + AddSubmonoid.mul_le_mul_left h theorem mul_le_mul_right (h : N ≤ P) : M * N ≤ M * P := - map₂_le_map₂_right h + AddSubmonoid.mul_le_mul_right h variable (M N P) theorem mul_sup : M * (N ⊔ P) = M * N ⊔ M * P := - map₂_sup_right _ _ _ _ + toAddSubmonoid_injective <| by + simp_rw [mul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.mul_sup, mul_toAddSubmonoid] theorem sup_mul : (M ⊔ N) * P = M * P ⊔ N * P := - map₂_sup_left _ _ _ _ + toAddSubmonoid_injective <| by + simp_rw [mul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.sup_mul, mul_toAddSubmonoid] theorem mul_subset_mul : (↑M : Set A) * (↑N : Set A) ⊆ (↑(M * N) : Set A) := - image2_subset_map₂ (Algebra.lmul R A).toLinearMap M N + AddSubmonoid.mul_subset_mul + +lemma restrictScalars_mul {A B C} [Semiring A] [Semiring B] [Semiring C] + [SMul A B] [Module A C] [Module B C] [IsScalarTower A C C] [IsScalarTower B C C] + [IsScalarTower A B C] {I J : Submodule B C} : + (I * J).restrictScalars A = I.restrictScalars A * J.restrictScalars A := + rfl + +variable {ι : Sort uι} + +theorem iSup_mul (s : ι → Submodule R A) (t : Submodule R A) : (⨆ i, s i) * t = ⨆ i, s i * t := + toAddSubmonoid_injective <| by + simp_rw [mul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.iSup_mul, mul_toAddSubmonoid] + +theorem mul_iSup (t : Submodule R A) (s : ι → Submodule R A) : (t * ⨆ i, s i) = ⨆ i, t * s i := + toAddSubmonoid_injective <| by + simp_rw [mul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.mul_iSup, mul_toAddSubmonoid] + +/-- Sub-`R`-modules of an `R`-module form an idempotent semiring. -/ +instance : NonUnitalSemiring (Submodule R A) where + __ := toAddSubmonoid_injective.semigroup _ mul_toAddSubmonoid + zero_mul := bot_mul + mul_zero := mul_bot + left_distrib := mul_sup + right_distrib := sup_mul + +instance : Pow (Submodule R A) ℕ where + pow s n := npowRec n s + +theorem pow_eq_npowRec {n : ℕ} : M ^ n = npowRec n M := rfl + +protected theorem pow_zero : M ^ 0 = 1 := rfl + +protected theorem pow_succ {n : ℕ} : M ^ (n + 1) = M ^ n * M := rfl + +protected theorem pow_one : M ^ 1 = M := by + rw [Submodule.pow_succ, Submodule.pow_zero, Submodule.one_mul] + +theorem pow_toAddSubmonoid {n : ℕ} (h : n ≠ 0) : (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n := by + induction n with + | zero => exact (h rfl).elim + | succ n ih => + rw [Submodule.pow_succ, pow_succ, mul_toAddSubmonoid] + cases n with + | zero => rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul] + | succ n => rw [ih n.succ_ne_zero] + +theorem le_pow_toAddSubmonoid {n : ℕ} : M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid := by + obtain rfl | hn := Decidable.eq_or_ne n 0 + · rw [Submodule.pow_zero, pow_zero] + exact le_one_toAddSubmonoid + · exact (pow_toAddSubmonoid M hn).ge + +theorem pow_subset_pow {n : ℕ} : (↑M : Set A) ^ n ⊆ ↑(M ^ n : Submodule R A) := + trans AddSubmonoid.pow_subset_pow (le_pow_toAddSubmonoid M) + +theorem pow_mem_pow {x : A} (hx : x ∈ M) (n : ℕ) : x ^ n ∈ M ^ n := + pow_subset_pow _ <| Set.pow_mem_pow hx _ + +end Module + +variable {ι : Sort uι} +variable {R : Type u} [CommSemiring R] + +section Ring + +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 + simp + +@[simp] +theorem map_op_one : + map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (1 : Submodule R A) = 1 := by + ext x + induction x + simp + +@[simp] +theorem comap_op_one : + comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (1 : Submodule R Aᵐᵒᵖ) = 1 := by + ext + simp + +@[simp] +theorem map_unop_one : + map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (1 : Submodule R Aᵐᵒᵖ) = 1 := by + rw [← comap_equiv_eq_map_symm, comap_op_one] + +@[simp] +theorem comap_unop_one : + comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (1 : Submodule R A) = 1 := by + rw [← map_equiv_eq_comap_symm, map_op_one] + +theorem mul_eq_map₂ : M * N = map₂ (LinearMap.mul R A) M N := + le_antisymm (mul_le.mpr fun _m hm _n ↦ apply_mem_map₂ _ hm) + (map₂_le.mpr fun _m hm _n ↦ mul_mem_mul hm) + +variable (R) + +theorem span_mul_span : span R S * span R T = span R (S * T) := by + rw [mul_eq_map₂]; apply map₂_span_span + +variable {R} (M N P Q) + +-- @[simp] -- Porting note (#10618): simp can prove this once we have a monoid structure +protected theorem mul_one : M * 1 = M := by + conv_lhs => rw [one_eq_span, ← span_eq M] + erw [span_mul_span, mul_one, span_eq] protected theorem map_mul {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') : map f.toLinearMap (M * N) = map f.toLinearMap M * map f.toLinearMap N := calc - map f.toLinearMap (M * N) = ⨆ i : M, (N.map (LinearMap.mul R A i)).map f.toLinearMap := - map_iSup _ _ + map f.toLinearMap (M * N) = ⨆ i : M, (N.map (LinearMap.mul R A i)).map f.toLinearMap := by + rw [mul_eq_map₂]; apply map_iSup _ = map f.toLinearMap M * map f.toLinearMap N := by + rw [mul_eq_map₂] apply congr_arg sSup ext S constructor <;> rintro ⟨y, hy⟩ @@ -273,16 +352,6 @@ theorem comap_op_mul (M N : Submodule R Aᵐᵒᵖ) : comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M := by simp_rw [comap_equiv_eq_map_symm, map_unop_mul] -lemma restrictScalars_mul {A B C} [CommSemiring A] [CommSemiring B] [Semiring C] - [Algebra A B] [Algebra A C] [Algebra B C] [IsScalarTower A B C] {I J : Submodule B C} : - (I * J).restrictScalars A = I.restrictScalars A * J.restrictScalars A := by - apply le_antisymm - · intro x (hx : x ∈ I * J) - refine Submodule.mul_induction_on hx ?_ ?_ - · exact fun m hm n hn ↦ mul_mem_mul hm hn - · exact fun _ _ ↦ add_mem - · exact mul_le.mpr (fun _ hm _ hn ↦ mul_mem_mul hm hn) - section open Pointwise @@ -312,14 +381,8 @@ theorem mem_span_mul_finite_of_mem_span_mul {R A} [Semiring R] [AddCommMonoid A] end DecidableEq -theorem mul_eq_span_mul_set (s t : Submodule R A) : s * t = span R ((s : Set A) * (t : Set A)) := - map₂_eq_span_image2 _ s t - -theorem iSup_mul (s : ι → Submodule R A) (t : Submodule R A) : (⨆ i, s i) * t = ⨆ i, s i * t := - map₂_iSup_left _ s t - -theorem mul_iSup (t : Submodule R A) (s : ι → Submodule R A) : (t * ⨆ i, s i) = ⨆ i, t * s i := - map₂_iSup_right _ t s +theorem mul_eq_span_mul_set (s t : Submodule R A) : s * t = span R ((s : Set A) * (t : Set A)) := by + rw [mul_eq_map₂]; exact map₂_eq_span_image2 _ s t theorem mem_span_mul_finite_of_mem_mul {P Q : Submodule R A} {x : A} (hx : x ∈ P * Q) : ∃ T T' : Finset A, (T : Set A) ⊆ P ∧ (T' : Set A) ⊆ Q ∧ x ∈ span R (T * T' : Set A) := @@ -329,13 +392,11 @@ theorem mem_span_mul_finite_of_mem_mul {P Q : Submodule R A} {x : A} (hx : x ∈ variable {M N P} theorem mem_span_singleton_mul {x y : A} : x ∈ span R {y} * P ↔ ∃ z ∈ P, y * z = x := by - -- Porting note: need both `*` and `Mul.mul` - simp_rw [(· * ·), Mul.mul, map₂_span_singleton_eq_map] + simp_rw [mul_eq_map₂, (· * ·), map₂_span_singleton_eq_map] rfl theorem mem_mul_span_singleton {x y : A} : x ∈ P * span R {y} ↔ ∃ z ∈ P, z * y = x := by - -- Porting note: need both `*` and `Mul.mul` - simp_rw [(· * ·), Mul.mul, map₂_span_singleton_eq_map_flip] + simp_rw [mul_eq_map₂, (· * ·), map₂_span_singleton_eq_map_flip] rfl lemma span_singleton_mul {x : A} {p : Submodule R A} : @@ -368,19 +429,11 @@ theorem mul_smul_mul_eq_smul_mul_smul (x y : R) : (x * y) • (M * N) = (x • M exact smul_mem_pointwise_smul _ _ _ (mul_mem_mul hm hn) /-- Sub-R-modules of an R-algebra form an idempotent semiring. -/ -instance idemSemiring : IdemSemiring (Submodule R A) := - { toAddSubmonoid_injective.semigroup _ fun m n : Submodule R A => mul_toAddSubmonoid m n, - AddMonoidWithOne.unary, Submodule.pointwiseAddCommMonoid, - (by infer_instance : - Lattice (Submodule R A)) with - one_mul := Submodule.one_mul - mul_one := Submodule.mul_one - zero_mul := bot_mul - mul_zero := mul_bot - left_distrib := mul_sup - right_distrib := sup_mul, - -- Porting note: removed `(by infer_instance : OrderBot (Submodule R A))` - bot_le := fun _ => bot_le } +instance idemSemiring : IdemSemiring (Submodule R A) where + __ := instNonUnitalSemiring + one_mul := Submodule.one_mul + mul_one := Submodule.mul_one + bot_le _ := bot_le variable (M) @@ -391,27 +444,6 @@ theorem span_pow (s : Set A) : ∀ n : ℕ, span R s ^ n = span R (s ^ n) theorem pow_eq_span_pow_set (n : ℕ) : M ^ n = span R ((M : Set A) ^ n) := by rw [← span_pow, span_eq] -theorem pow_subset_pow {n : ℕ} : (↑M : Set A) ^ n ⊆ ↑(M ^ n : Submodule R A) := - (pow_eq_span_pow_set M n).symm ▸ subset_span - -theorem pow_mem_pow {x : A} (hx : x ∈ M) (n : ℕ) : x ^ n ∈ M ^ n := - pow_subset_pow _ <| Set.pow_mem_pow hx _ - -theorem pow_toAddSubmonoid {n : ℕ} (h : n ≠ 0) : (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n := by - induction n with - | zero => exact (h rfl).elim - | succ n ih => - rw [pow_succ, pow_succ, mul_toAddSubmonoid] - cases n with - | zero => rw [pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, one_mul] - | succ n => rw [ih n.succ_ne_zero] - -theorem le_pow_toAddSubmonoid {n : ℕ} : M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid := by - obtain rfl | hn := Decidable.eq_or_ne n 0 - · rw [pow_zero, pow_zero] - exact le_one_toAddSubmonoid - · exact (pow_toAddSubmonoid M hn).ge - /-- Dependent version of `Submodule.pow_induction_on_left`. -/ @[elab_as_elim] protected theorem pow_induction_on_left' {C : ∀ (n : ℕ) (x), x ∈ M ^ n → Prop} @@ -425,7 +457,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 @@ -446,7 +478,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 @@ -541,11 +573,10 @@ variable {α : Type*} [Monoid α] [MulSemiringAction α A] [SMulCommClass α R A This is available as an instance in the `Pointwise` locale. This is a stronger version of `Submodule.pointwiseDistribMulAction`. -/ -protected def pointwiseMulSemiringAction : MulSemiringAction α (Submodule R A) := - { - Submodule.pointwiseDistribMulAction with - smul_mul := fun r x y => Submodule.map_mul x y <| MulSemiringAction.toAlgHom R A r - smul_one := fun r => Submodule.map_one <| MulSemiringAction.toAlgHom R A r } +protected def pointwiseMulSemiringAction : MulSemiringAction α (Submodule R A) where + __ := Submodule.pointwiseDistribMulAction + smul_mul r x y := Submodule.map_mul x y <| MulSemiringAction.toAlgHom R A r + smul_one r := Submodule.map_one <| MulSemiringAction.toAlgHom R A r scoped[Pointwise] attribute [instance] Submodule.pointwiseMulSemiringAction diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index 7f7d7ece643cd..284ecf430bdf1 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -436,6 +436,18 @@ def nsmulRec [Zero M] [Add M] : ℕ → M → M attribute [to_additive existing] npowRec +variable [One M] [Semigroup M] (m n : ℕ) (hn : n ≠ 0) (a : M) (ha : 1 * a = a) +include hn ha + +@[to_additive] theorem npowRec_add : npowRec (m + n) a = npowRec m a * npowRec n a := by + obtain _ | n := n; · exact (hn rfl).elim + induction n with + | zero => simp only [Nat.zero_add, npowRec, ha] + | succ n ih => rw [← Nat.add_assoc, npowRec, ih n.succ_ne_zero]; simp only [npowRec, mul_assoc] + +@[to_additive] theorem npowRec_succ : npowRec (n + 1) a = a * npowRec n a := by + rw [Nat.add_comm, npowRec_add 1 n hn a ha, npowRec, npowRec, ha] + end library_note "forgetful inheritance"/-- diff --git a/Mathlib/Algebra/Group/Subgroup/Pointwise.lean b/Mathlib/Algebra/Group/Subgroup/Pointwise.lean index 48ad4a5c50a1d..0ba849fba4351 100644 --- a/Mathlib/Algebra/Group/Subgroup/Pointwise.lean +++ b/Mathlib/Algebra/Group/Subgroup/Pointwise.lean @@ -543,4 +543,17 @@ theorem le_pointwise_smul_iff₀ {a : α} (ha : a ≠ 0) {S T : AddSubgroup A} : end GroupWithZero +section Mul + +variable {R : Type*} [NonUnitalNonAssocRing R] + +protected def mul : Mul (AddSubgroup R) where + mul M N := + { __ := M.toAddSubmonoid * N.toAddSubmonoid + neg_mem' := fun h ↦ AddSubmonoid.mul_induction_on h + (fun m hm n hn ↦ by rw [← neg_mul]; exact AddSubmonoid.mul_mem_mul (M.neg_mem hm) hn) + fun r₁ r₂ h₁ h₂ ↦ by rw [neg_add]; exact (M.1 * N.1).add_mem h₁ h₂ } + +end Mul + end AddSubgroup diff --git a/Mathlib/Algebra/Group/Submonoid/Pointwise.lean b/Mathlib/Algebra/Group/Submonoid/Pointwise.lean index 9434237fea0f1..89361a4d0b451 100644 --- a/Mathlib/Algebra/Group/Submonoid/Pointwise.lean +++ b/Mathlib/Algebra/Group/Submonoid/Pointwise.lean @@ -487,20 +487,47 @@ theorem bot_mul (S : AddSubmonoid R) : ⊥ * S = ⊥ := eq_bot_iff.2 <| mul_le.2 fun m hm n _ => by rw [AddSubmonoid.mem_bot] at hm ⊢; rw [hm, zero_mul] +variable {M N P Q : AddSubmonoid R} + @[mono] -theorem mul_le_mul {M N P Q : AddSubmonoid R} (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q := +theorem mul_le_mul (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q := mul_le.2 fun _m hm _n hn => mul_mem_mul (hmp hm) (hnq hn) -theorem mul_le_mul_left {M N P : AddSubmonoid R} (h : M ≤ N) : M * P ≤ N * P := +theorem mul_le_mul_left (h : M ≤ N) : M * P ≤ N * P := mul_le_mul h (le_refl P) -theorem mul_le_mul_right {M N P : AddSubmonoid R} (h : N ≤ P) : M * N ≤ M * P := +theorem mul_le_mul_right (h : N ≤ P) : M * N ≤ M * P := mul_le_mul (le_refl M) h -theorem mul_subset_mul {M N : AddSubmonoid R} : - (↑M : Set R) * (↑N : Set R) ⊆ (↑(M * N) : Set R) := +theorem mul_subset_mul : (↑M : Set R) * (↑N : Set R) ⊆ (↑(M * N) : Set R) := mul_subset_iff.2 fun _i hi _j hj ↦ mul_mem_mul hi hj +theorem mul_sup : M * (N ⊔ P) = M * N ⊔ M * P := + le_antisymm (mul_le.mpr fun m hm np hnp ↦ by + obtain ⟨n, hn, p, hp, rfl⟩ := mem_sup.mp hnp + rw [left_distrib]; exact add_mem_sup (mul_mem_mul hm hn) <| mul_mem_mul hm hp) + (sup_le (mul_le_mul_right le_sup_left) <| mul_le_mul_right le_sup_right) + +theorem sup_mul : (M ⊔ N) * P = M * P ⊔ N * P := + le_antisymm (mul_le.mpr fun mn hmn p hp ↦ by + obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn + rw [right_distrib]; exact add_mem_sup (mul_mem_mul hm hp) <| mul_mem_mul hn hp) + (sup_le (mul_le_mul_left le_sup_left) <| mul_le_mul_left le_sup_right) + +variable {ι : Sort*} + +theorem iSup_mul (S : ι → AddSubmonoid R) (T : AddSubmonoid R) : (⨆ i, S i) * T = ⨆ i, S i * T := + le_antisymm (mul_le.mpr fun s hs t ht ↦ iSup_induction _ (C := (· * t ∈ _)) hs + (fun i s hs ↦ mem_iSup_of_mem i <| mul_mem_mul hs ht) (by simp_rw [zero_mul]; apply zero_mem) + fun _ _ ↦ by simp_rw [right_distrib]; apply add_mem) <| + iSup_le fun i ↦ mul_le_mul_left (le_iSup _ i) + +theorem mul_iSup (T : AddSubmonoid R) (S : ι → AddSubmonoid R) : (T * ⨆ i, S i) = ⨆ i, T * S i := + le_antisymm (mul_le.mpr fun t ht s hs ↦ iSup_induction _ (C := (t * · ∈ _)) hs + (fun i s hs ↦ mem_iSup_of_mem i <| mul_mem_mul ht hs) (by simp_rw [mul_zero]; apply zero_mem) + fun _ _ ↦ by simp_rw [left_distrib]; apply add_mem) <| + iSup_le fun i ↦ mul_le_mul_right (le_iSup _ i) + end NonUnitalNonAssocSemiring section NonUnitalNonAssocRing @@ -588,6 +615,33 @@ theorem pow_subset_pow {s : AddSubmonoid R} {n : ℕ} : (↑s : Set R) ^ n ⊆ end Semiring +section SMul + +variable [AddMonoid R] [DistribSMul R A] + +instance : SMul (AddSubmonoid R) (AddSubmonoid A) where + smul M N := ⨆ s : M, N.map (DistribSMul.toAddMonoidHom A s.1) + +variable {M M' : AddSubmonoid R} {N P : AddSubmonoid A} {m : R} {n : A} + +theorem smul_mem_smul (hm : m ∈ M) (hn : n ∈ N) : m • n ∈ M • N := + (le_iSup _ ⟨m, hm⟩ : _ ≤ M • N) ⟨n, hn, by rfl⟩ + +theorem smul_le : M • N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m • n ∈ P := + ⟨fun H _m hm _n hn => H <| smul_mem_smul hm hn, fun H => + iSup_le fun ⟨m, hm⟩ => map_le_iff_le_comap.2 fun n hn => H m hm n hn⟩ + +@[elab_as_elim] +protected theorem smul_induction_on {C : A → Prop} {a : A} (ha : a ∈ M • N) + (hm : ∀ m ∈ M, ∀ n ∈ N, C (m • n)) (hadd : ∀ x y, C x → C y → C (x + y)) : C a := + (@smul_le _ _ _ _ _ _ _ ⟨⟨setOf C, hadd _ _⟩, by + simpa only [smul_zero] using hm _ (zero_mem _) _ (zero_mem _)⟩).2 hm ha + +theorem smul_le_smul (h : M ≤ M') (hnp : N ≤ P) : M • N ≤ M' • P := + smul_le.2 fun _m hm _n hn => smul_mem_smul (h hm) (hnp hn) + +end SMul + end AddSubmonoid namespace Set.IsPWO diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean index 6a3982baf6a29..752dedfa1877e 100644 --- a/Mathlib/RingTheory/Ideal/Maps.lean +++ b/Mathlib/RingTheory/Ideal/Maps.lean @@ -251,11 +251,7 @@ is also the smallest `R`-submodule that does so. -/ @[simp] theorem restrictScalars_mul {R S : Type*} [CommSemiring R] [CommSemiring S] [Algebra R S] (I J : Ideal S) : (I * J).restrictScalars R = I.restrictScalars R * J.restrictScalars R := - le_antisymm - (fun _ hx => - Submodule.mul_induction_on hx (fun _ hx _ hy => Submodule.mul_mem_mul hx hy) fun _ _ => - Submodule.add_mem _) - (Submodule.mul_le.mpr fun _ hx _ hy => Ideal.mul_mem_mul hx hy) + rfl section Surjective @@ -637,6 +633,112 @@ theorem ker_isMaximal_of_surjective {R K F : Type*} [Ring R] [Field K] end RingHom +section annihilator + +section Semiring + +variable {R M M' : Type*} +variable [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] + +variable (R M) in +/-- `Module.annihilator R M` is the ideal of all elements `r : R` such that `r • M = 0`. -/ +def Module.annihilator : Ideal R := RingHom.ker (Module.toAddMonoidEnd R M) + +theorem Module.mem_annihilator {r} : r ∈ Module.annihilator R M ↔ ∀ m : M, r • m = 0 := + ⟨fun h ↦ (congr($h ·)), (AddMonoidHom.ext ·)⟩ + +theorem LinearMap.annihilator_le_of_injective (f : M →ₗ[R] M') (hf : Function.Injective f) : + Module.annihilator R M' ≤ Module.annihilator R M := fun x h ↦ by + rw [Module.mem_annihilator] at h ⊢; exact fun m ↦ hf (by rw [map_smul, h, f.map_zero]) + +theorem LinearMap.annihilator_le_of_surjective (f : M →ₗ[R] M') + (hf : Function.Surjective f) : Module.annihilator R M ≤ Module.annihilator R M' := fun x h ↦ by + rw [Module.mem_annihilator] at h ⊢ + intro m; obtain ⟨m, rfl⟩ := hf m + rw [← map_smul, h, f.map_zero] + +theorem LinearEquiv.annihilator_eq (e : M ≃ₗ[R] M') : + Module.annihilator R M = Module.annihilator R M' := + (e.annihilator_le_of_surjective e.surjective).antisymm (e.annihilator_le_of_injective e.injective) + +namespace Submodule + +/-- `N.annihilator` is the ideal of all elements `r : R` such that `r • N = 0`. -/ +abbrev annihilator (N : Submodule R M) : Ideal R := + Module.annihilator R N + +theorem annihilator_top : (⊤ : Submodule R M).annihilator = Module.annihilator R M := + topEquiv.annihilator_eq + +variable {I J : Ideal R} {N P : Submodule R M} + +theorem mem_annihilator {r} : r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = (0 : M) := by + simp_rw [annihilator, Module.mem_annihilator, Subtype.forall, Subtype.ext_iff]; rfl + +theorem annihilator_bot : (⊥ : Submodule R M).annihilator = ⊤ := + top_le_iff.mp fun _ _ ↦ mem_annihilator.mpr fun _ ↦ by rintro rfl; rw [smul_zero] + +theorem annihilator_eq_top_iff : N.annihilator = ⊤ ↔ N = ⊥ := + ⟨fun H ↦ + eq_bot_iff.2 fun (n : M) hn => + (mem_bot R).2 <| one_smul R n ▸ mem_annihilator.1 ((Ideal.eq_top_iff_one _).1 H) n hn, + fun H ↦ H.symm ▸ annihilator_bot⟩ + +theorem annihilator_mono (h : N ≤ P) : P.annihilator ≤ N.annihilator := fun _ hrp => + mem_annihilator.2 fun n hn => mem_annihilator.1 hrp n <| h hn + +theorem annihilator_iSup (ι : Sort w) (f : ι → Submodule R M) : + annihilator (⨆ i, f i) = ⨅ i, annihilator (f i) := + le_antisymm (le_iInf fun _ => annihilator_mono <| le_iSup _ _) fun r H => + mem_annihilator.2 fun n hn ↦ iSup_induction f (C := (r • · = 0)) hn + (fun i ↦ mem_annihilator.1 <| (mem_iInf _).mp H i) (smul_zero _) + fun m₁ m₂ h₁ h₂ ↦ by simp_rw [smul_add, h₁, h₂, add_zero] + +@[simp] +theorem annihilator_smul (N : Submodule R M) : annihilator N • N = ⊥ := + eq_bot_iff.2 (smul_le.2 fun _ => mem_annihilator.1) + +@[simp] +theorem annihilator_mul (I : Ideal R) : annihilator I * I = ⊥ := + annihilator_smul I + +end Submodule + +end Semiring + +namespace Submodule + +variable {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} + +theorem mem_annihilator' {r} : r ∈ N.annihilator ↔ N ≤ comap (r • (LinearMap.id : M →ₗ[R] M)) ⊥ := + mem_annihilator.trans ⟨fun H n hn => (mem_bot R).2 <| H n hn, fun H _ hn => (mem_bot R).1 <| H hn⟩ + +theorem mem_annihilator_span (s : Set M) (r : R) : + r ∈ (Submodule.span R s).annihilator ↔ ∀ n : s, r • (n : M) = 0 := by + rw [Submodule.mem_annihilator] + constructor + · intro h n + exact h _ (Submodule.subset_span n.prop) + · intro h n hn + refine Submodule.span_induction hn ?_ ?_ ?_ ?_ + · intro x hx + exact h ⟨x, hx⟩ + · exact smul_zero _ + · intro x y hx hy + rw [smul_add, hx, hy, zero_add] + · intro a x hx + rw [smul_comm, hx, smul_zero] + +theorem mem_annihilator_span_singleton (g : M) (r : R) : + r ∈ (Submodule.span R ({g} : Set M)).annihilator ↔ r • g = 0 := by simp [mem_annihilator_span] + +@[simp] +theorem mul_annihilator (I : Ideal R) : I * annihilator I = ⊥ := by rw [mul_comm, annihilator_mul] + +end Submodule + +end annihilator + namespace Ideal variable {R : Type*} {S : Type*} {F : Type*} diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index fcedd7484f313..e3412b7384319 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/Mathlib/RingTheory/Ideal/Operations.lean @@ -24,148 +24,61 @@ namespace Submodule variable {R : Type u} {M : Type v} {M' F G : Type*} -section CommSemiring +section Semiring -variable [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] +variable [Semiring R] [AddCommMonoid M] [Module R M] -open Pointwise - -instance hasSMul' : SMul (Ideal R) (Submodule R M) := - ⟨Submodule.map₂ (LinearMap.lsmul R M)⟩ +instance : SMul (Ideal R) (Submodule R M) where + smul I N := + { __ := I.toAddSubmonoid • N.toAddSubmonoid + smul_mem' := fun r m hm ↦ AddSubmonoid.smul_induction_on hm + (fun m hm n ↦ by rw [smul_smul]; exact AddSubmonoid.smul_mem_smul <| I.smul_mem _ hm) + fun m₁ m₂ h₁ h₂ ↦ by rw [smul_add]; exact (I.1 • N.1).add_mem h₁ h₂ } /-- This duplicates the global `smul_eq_mul`, but doesn't have to unfold anywhere near as much to apply. -/ protected theorem _root_.Ideal.smul_eq_mul (I J : Ideal R) : I • J = I * J := rfl -variable (R M) in -/-- `Module.annihilator R M` is the ideal of all elements `r : R` such that `r • M = 0`. -/ -def _root_.Module.annihilator : Ideal R := LinearMap.ker (LinearMap.lsmul R M) - -theorem _root_.Module.mem_annihilator {r} : r ∈ Module.annihilator R M ↔ ∀ m : M, r • m = 0 := - ⟨fun h ↦ (congr($h ·)), (LinearMap.ext ·)⟩ - -theorem _root_.LinearMap.annihilator_le_of_injective (f : M →ₗ[R] M') (hf : Function.Injective f) : - Module.annihilator R M' ≤ Module.annihilator R M := fun x h ↦ by - rw [Module.mem_annihilator] at h ⊢; exact fun m ↦ hf (by rw [map_smul, h, f.map_zero]) - -theorem _root_.LinearMap.annihilator_le_of_surjective (f : M →ₗ[R] M') - (hf : Function.Surjective f) : Module.annihilator R M ≤ Module.annihilator R M' := fun x h ↦ by - rw [Module.mem_annihilator] at h ⊢ - intro m; obtain ⟨m, rfl⟩ := hf m - rw [← map_smul, h, f.map_zero] - -theorem _root_.LinearEquiv.annihilator_eq (e : M ≃ₗ[R] M') : - Module.annihilator R M = Module.annihilator R M' := - (e.annihilator_le_of_surjective e.surjective).antisymm (e.annihilator_le_of_injective e.injective) - -/-- `N.annihilator` is the ideal of all elements `r : R` such that `r • N = 0`. -/ -abbrev annihilator (N : Submodule R M) : Ideal R := - Module.annihilator R N - -theorem annihilator_top : (⊤ : Submodule R M).annihilator = Module.annihilator R M := - topEquiv.annihilator_eq - variable {I J : Ideal R} {N P : Submodule R M} -theorem mem_annihilator {r} : r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = (0 : M) := by - simp_rw [annihilator, Module.mem_annihilator, Subtype.forall, Subtype.ext_iff]; rfl - -theorem mem_annihilator' {r} : r ∈ N.annihilator ↔ N ≤ comap (r • (LinearMap.id : M →ₗ[R] M)) ⊥ := - mem_annihilator.trans ⟨fun H n hn => (mem_bot R).2 <| H n hn, fun H _ hn => (mem_bot R).1 <| H hn⟩ - -theorem mem_annihilator_span (s : Set M) (r : R) : - r ∈ (Submodule.span R s).annihilator ↔ ∀ n : s, r • (n : M) = 0 := by - rw [Submodule.mem_annihilator] - constructor - · intro h n - exact h _ (Submodule.subset_span n.prop) - · intro h n hn - refine Submodule.span_induction hn ?_ ?_ ?_ ?_ - · intro x hx - exact h ⟨x, hx⟩ - · exact smul_zero _ - · intro x y hx hy - rw [smul_add, hx, hy, zero_add] - · intro a x hx - rw [smul_comm, hx, smul_zero] - -theorem mem_annihilator_span_singleton (g : M) (r : R) : - r ∈ (Submodule.span R ({g} : Set M)).annihilator ↔ r • g = 0 := by simp [mem_annihilator_span] - -theorem annihilator_bot : (⊥ : Submodule R M).annihilator = ⊤ := - (Ideal.eq_top_iff_one _).2 <| mem_annihilator'.2 bot_le - -theorem annihilator_eq_top_iff : N.annihilator = ⊤ ↔ N = ⊥ := - ⟨fun H => - eq_bot_iff.2 fun (n : M) hn => - (mem_bot R).2 <| one_smul R n ▸ mem_annihilator.1 ((Ideal.eq_top_iff_one _).1 H) n hn, - fun H => H.symm ▸ annihilator_bot⟩ - -theorem annihilator_mono (h : N ≤ P) : P.annihilator ≤ N.annihilator := fun _ hrp => - mem_annihilator.2 fun n hn => mem_annihilator.1 hrp n <| h hn - -theorem annihilator_iSup (ι : Sort w) (f : ι → Submodule R M) : - annihilator (⨆ i, f i) = ⨅ i, annihilator (f i) := - le_antisymm (le_iInf fun _ => annihilator_mono <| le_iSup _ _) fun _ H => - mem_annihilator'.2 <| - iSup_le fun i => - have := (mem_iInf _).1 H i - mem_annihilator'.1 this - theorem smul_mem_smul {r} {n} (hr : r ∈ I) (hn : n ∈ N) : r • n ∈ I • N := - apply_mem_map₂ _ hr hn + AddSubmonoid.smul_mem_smul hr hn -theorem smul_le {P : Submodule R M} : I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P := - map₂_le +theorem smul_le : I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P := + AddSubmonoid.smul_le @[simp, norm_cast] lemma coe_set_smul : (I : Set R) • N = I • N := - Submodule.set_smul_eq_of_le _ _ _ - (fun _ _ hr hx => smul_mem_smul hr hx) - (smul_le.mpr fun _ hr _ hx => mem_set_smul_of_mem_mem hr hx) + set_smul_eq_of_le _ _ _ + (fun _ _ hr hx ↦ smul_mem_smul hr hx) + (smul_le.mpr fun _ hr _ hx ↦ mem_set_smul_of_mem_mem hr hx) @[elab_as_elim] theorem smul_induction_on {p : M → Prop} {x} (H : x ∈ I • N) (smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n)) - (add : ∀ x y, p x → p y → p (x + y)) : p x := by - have H0 : p 0 := by simpa only [zero_smul] using smul 0 I.zero_mem 0 N.zero_mem - refine Submodule.iSup_induction (x := x) _ H ?_ H0 add - rintro ⟨i, hi⟩ m ⟨j, hj, hj'⟩ - rw [← hj'] - exact smul _ hi _ hj + (add : ∀ x y, p x → p y → p (x + y)) : p x := + AddSubmonoid.smul_induction_on H smul add /-- Dependent version of `Submodule.smul_induction_on`. -/ @[elab_as_elim] theorem smul_induction_on' {x : M} (hx : x ∈ I • N) {p : ∀ x, x ∈ I • N → Prop} (smul : ∀ (r : R) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) (smul_mem_smul hr hn)) - (add : ∀ x hx y hy, p x hx → p y hy → p (x + y) (Submodule.add_mem _ ‹_› ‹_›)) : p x hx := by - refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) => H - exact - smul_induction_on hx (fun a ha x hx => ⟨_, smul _ ha _ hx⟩) fun x y ⟨_, hx⟩ ⟨_, hy⟩ => - ⟨_, add _ _ _ _ hx hy⟩ - -theorem mem_smul_span_singleton {I : Ideal R} {m : M} {x : M} : - x ∈ I • span R ({m} : Set M) ↔ ∃ y ∈ I, y • m = x := - ⟨fun hx => - smul_induction_on hx - (fun r hri _ hnm => - let ⟨s, hs⟩ := mem_span_singleton.1 hnm - ⟨r * s, I.mul_mem_right _ hri, hs ▸ mul_smul r s m⟩) - fun m1 m2 ⟨y1, hyi1, hy1⟩ ⟨y2, hyi2, hy2⟩ => - ⟨y1 + y2, I.add_mem hyi1 hyi2, by rw [add_smul, hy1, hy2]⟩, - fun ⟨_, hyi, hy⟩ => hy ▸ smul_mem_smul hyi (subset_span <| Set.mem_singleton m)⟩ + (add : ∀ x hx y hy, p x hx → p y hy → p (x + y) (add_mem ‹_› ‹_›)) : p x hx := by + refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H + exact smul_induction_on hx (fun a ha x hx ↦ ⟨_, smul _ ha _ hx⟩) + fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩ theorem smul_le_right : I • N ≤ N := - smul_le.2 fun r _ _ => N.smul_mem r + smul_le.2 fun r _ _ ↦ N.smul_mem r theorem smul_mono (hij : I ≤ J) (hnp : N ≤ P) : I • N ≤ J • P := - map₂_le_map₂ hij hnp + AddSubmonoid.smul_le_smul hij hnp theorem smul_mono_left (h : I ≤ J) : I • N ≤ J • N := - map₂_le_map₂_left h + smul_mono h le_rfl instance : CovariantClass (Ideal R) (Submodule R M) HSMul.hSMul LE.le := - ⟨fun _ _ => map₂_le_map₂_right⟩ + ⟨fun _ _ => smul_mono le_rfl⟩ @[deprecated smul_mono_right (since := "2024-03-31")] protected theorem smul_mono_right (h : N ≤ P) : I • N ≤ I • P := @@ -177,65 +90,122 @@ theorem map_le_smul_top (I : Ideal R) (f : R →ₗ[R] M) : rw [← mul_one y, ← smul_eq_mul, f.map_smul] exact smul_mem_smul hy mem_top -@[simp] -theorem annihilator_smul (N : Submodule R M) : annihilator N • N = ⊥ := - eq_bot_iff.2 (smul_le.2 fun _ => mem_annihilator.1) - -@[simp] -theorem annihilator_mul (I : Ideal R) : annihilator I * I = ⊥ := - annihilator_smul I - -@[simp] -theorem mul_annihilator (I : Ideal R) : I * annihilator I = ⊥ := by rw [mul_comm, annihilator_mul] - variable (I J N P) @[simp] theorem smul_bot : I • (⊥ : Submodule R M) = ⊥ := - map₂_bot_right _ _ + le_bot_iff.mp <| smul_le.mpr <| by rintro _ _ _ rfl; rw [smul_zero]; exact zero_mem _ @[simp] theorem bot_smul : (⊥ : Ideal R) • N = ⊥ := - map₂_bot_left _ _ + le_bot_iff.mp <| smul_le.mpr <| by rintro _ rfl _ _; rw [zero_smul]; exact zero_mem _ @[simp] theorem top_smul : (⊤ : Ideal R) • N = N := le_antisymm smul_le_right fun r hri => one_smul R r ▸ smul_mem_smul mem_top hri theorem smul_sup : I • (N ⊔ P) = I • N ⊔ I • P := - map₂_sup_right _ _ _ _ + le_antisymm (smul_le.mpr fun m hm np hnp ↦ by + obtain ⟨n, hn, p, hp, rfl⟩ := mem_sup.mp hnp + rw [smul_add]; exact add_mem_sup (smul_mem_smul hm hn) <| smul_mem_smul hm hp) + (sup_le (smul_mono_right _ le_sup_left) <| smul_mono_right _ le_sup_right) theorem sup_smul : (I ⊔ J) • N = I • N ⊔ J • N := - map₂_sup_left _ _ _ _ + le_antisymm (smul_le.mpr fun mn hmn p hp ↦ by + obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn + rw [add_smul]; exact add_mem_sup (smul_mem_smul hm hp) <| smul_mem_smul hn hp) + (sup_le (smul_mono_left le_sup_left) <| smul_mono_left le_sup_right) protected theorem smul_assoc : (I • J) • N = I • J • N := le_antisymm - (smul_le.2 fun _ hrsij t htn => - smul_induction_on hrsij - (fun r hr s hs => - (@smul_eq_mul R _ r s).symm ▸ smul_smul r s t ▸ smul_mem_smul hr (smul_mem_smul hs htn)) - fun x y => (add_smul x y t).symm ▸ Submodule.add_mem _) - (smul_le.2 fun r hr _ hsn => - suffices J • N ≤ Submodule.comap (r • (LinearMap.id : M →ₗ[R] M)) ((I • J) • N) from this hsn - smul_le.2 fun s hs n hn => - show r • s • n ∈ (I • J) • N from mul_smul r s n ▸ smul_mem_smul (smul_mem_smul hr hs) hn) + (smul_le.2 fun _ hrsij t htn ↦ smul_induction_on hrsij + (fun r hr s hs ↦ smul_assoc r s t ▸ smul_mem_smul hr (smul_mem_smul hs htn)) + fun x y ↦ (add_smul x y t).symm ▸ add_mem) + (smul_le.2 fun r hr _ hsn ↦ smul_induction_on hsn + (fun j hj n hn ↦ (smul_assoc r j n).symm ▸ smul_mem_smul (smul_mem_smul hr hj) hn) + fun m₁ m₂ ↦ (smul_add r m₁ m₂) ▸ add_mem) @[deprecated smul_inf_le (since := "2024-03-31")] protected theorem smul_inf_le (M₁ M₂ : Submodule R M) : I • (M₁ ⊓ M₂) ≤ I • M₁ ⊓ I • M₂ := smul_inf_le _ _ _ theorem smul_iSup {ι : Sort*} {I : Ideal R} {t : ι → Submodule R M} : I • iSup t = ⨆ i, I • t i := - map₂_iSup_right _ _ _ + le_antisymm (smul_le.mpr fun t ht s hs ↦ iSup_induction _ (C := (t • · ∈ _)) hs + (fun i s hs ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs) (by simp_rw [smul_zero]; apply zero_mem) + fun _ _ ↦ by simp_rw [smul_add]; apply add_mem) <| + iSup_le fun i ↦ smul_mono_right _ (le_iSup _ i) @[deprecated smul_iInf_le (since := "2024-03-31")] protected theorem smul_iInf_le {ι : Sort*} {I : Ideal R} {t : ι → Submodule R M} : I • iInf t ≤ ⨅ i, I • t i := smul_iInf_le +theorem mem_of_span_top_of_smul_mem (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (x : M) + (H : ∀ r : s, (r : R) • x ∈ M') : x ∈ M' := by + suffices LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M' by + rw [← LinearMap.toSpanSingleton_one R M x] + exact this (LinearMap.mem_range_self _ 1) + rw [LinearMap.range_eq_map, ← hs, map_le_iff_le_comap, Ideal.span, span_le] + exact fun r hr ↦ H ⟨r, hr⟩ + +variable {M' : Type w} [AddCommMonoid M'] [Module R M'] + +@[simp] +theorem map_smul'' (f : M →ₗ[R] M') : (I • N).map f = I • N.map f := + le_antisymm + (map_le_iff_le_comap.2 <| + smul_le.2 fun r hr n hn => + show f (r • n) ∈ I • N.map f from + (f.map_smul r n).symm ▸ smul_mem_smul hr (mem_map_of_mem hn)) <| + smul_le.2 fun r hr _ hn => + let ⟨p, hp, hfp⟩ := mem_map.1 hn + hfp ▸ f.map_smul r p ▸ mem_map_of_mem (smul_mem_smul hr hp) + +theorem mem_smul_top_iff (N : Submodule R M) (x : N) : + x ∈ I • (⊤ : Submodule R N) ↔ (x : M) ∈ I • N := by + change _ ↔ N.subtype x ∈ I • N + have : Submodule.map N.subtype (I • ⊤) = I • N := by + rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype] + rw [← this] + exact (Function.Injective.mem_set_image N.injective_subtype).symm + +@[simp] +theorem smul_comap_le_comap_smul (f : M →ₗ[R] M') (S : Submodule R M') (I : Ideal R) : + I • S.comap f ≤ (I • S).comap f := by + refine Submodule.smul_le.mpr fun r hr x hx => ?_ + rw [Submodule.mem_comap] at hx ⊢ + rw [f.map_smul] + exact Submodule.smul_mem_smul hr hx + +end Semiring + +section CommSemiring + +variable [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] + +open Pointwise + +theorem mem_smul_span_singleton {I : Ideal R} {m : M} {x : M} : + x ∈ I • span R ({m} : Set M) ↔ ∃ y ∈ I, y • m = x := + ⟨fun hx => + smul_induction_on hx + (fun r hri _ hnm => + let ⟨s, hs⟩ := mem_span_singleton.1 hnm + ⟨r * s, I.mul_mem_right _ hri, hs ▸ mul_smul r s m⟩) + fun m1 m2 ⟨y1, hyi1, hy1⟩ ⟨y2, hyi2, hy2⟩ => + ⟨y1 + y2, I.add_mem hyi1 hyi2, by rw [add_smul, hy1, hy2]⟩, + fun ⟨_, hyi, hy⟩ => hy ▸ smul_mem_smul hyi (subset_span <| Set.mem_singleton m)⟩ + +variable {I J : Ideal R} {N P : Submodule R M} variable (S : Set R) (T : Set M) -theorem span_smul_span : Ideal.span S • span R T = span R (⋃ (s ∈ S) (t ∈ T), {s • t}) := - (map₂_span_span _ _ _ _).trans <| congr_arg _ <| Set.image2_eq_iUnion _ _ _ +theorem smul_eq_map₂ : I • N = Submodule.map₂ (LinearMap.lsmul R M) I N := + le_antisymm (smul_le.mpr fun _m hm _n ↦ Submodule.apply_mem_map₂ _ hm) + (map₂_le.mpr fun _m hm _n ↦ smul_mem_smul hm) + +theorem span_smul_span : Ideal.span S • span R T = span R (⋃ (s ∈ S) (t ∈ T), {s • t}) := by + rw [smul_eq_map₂] + exact (map₂_span_span _ _ _ _).trans <| congr_arg _ <| Set.image2_eq_iUnion _ _ _ theorem ideal_span_singleton_smul (r : R) (N : Submodule R M) : (Ideal.span {r} : Ideal R) • N = r • N := by @@ -245,14 +215,6 @@ theorem ideal_span_singleton_smul (r : R) (N : Submodule R M) : conv_lhs => rw [← span_eq N, span_smul_span] simpa -theorem mem_of_span_top_of_smul_mem (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (x : M) - (H : ∀ r : s, (r : R) • x ∈ M') : x ∈ M' := by - suffices (⊤ : Ideal R) • span R ({x} : Set M) ≤ M' by - rw [top_smul] at this - exact this (subset_span (Set.mem_singleton x)) - rw [← hs, span_smul_span, span_le] - simpa using H - /-- Given `s`, a generating set of `R`, to check that an `x : M` falls in a submodule `M'` of `x`, we only need to show that `r ^ n • x ∈ M'` for some `n` for each `r : s`. -/ theorem mem_of_span_eq_top_of_smul_pow_mem (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) @@ -268,27 +230,12 @@ theorem mem_of_span_eq_top_of_smul_pow_mem (M' : Submodule R M) (s : Set R) (hs simp only [Subtype.coe_mk, smul_smul, ← pow_add] rw [tsub_add_cancel_of_le (Finset.le_sup (s'.mem_attach _) : n₁ ⟨r, hr⟩ ≤ N)] -variable {M' : Type w} [AddCommMonoid M'] [Module R M'] - -@[simp] -theorem map_smul'' (f : M →ₗ[R] M') : (I • N).map f = I • N.map f := - le_antisymm - (map_le_iff_le_comap.2 <| - smul_le.2 fun r hr n hn => - show f (r • n) ∈ I • N.map f from - (f.map_smul r n).symm ▸ smul_mem_smul hr (mem_map_of_mem hn)) <| - smul_le.2 fun r hr _ hn => - let ⟨p, hp, hfp⟩ := mem_map.1 hn - hfp ▸ f.map_smul r p ▸ mem_map_of_mem (smul_mem_smul hr hp) - open Pointwise in @[simp] theorem map_pointwise_smul (r : R) (N : Submodule R M) (f : M →ₗ[R] M') : (r • N).map f = r • N.map f := by simp_rw [← ideal_span_singleton_smul, map_smul''] -variable {I} - theorem mem_smul_span {s : Set M} {x : M} : x ∈ I • Submodule.span R s ↔ x ∈ Submodule.span R (⋃ (a ∈ I) (b ∈ s), ({a • b} : Set M)) := by rw [← I.span_eq, Submodule.span_smul_span, I.span_eq] @@ -328,22 +275,6 @@ theorem mem_ideal_smul_span_iff_exists_sum' {ι : Type*} (s : Set ι) (f : ι ∃ (a : s →₀ R) (_ : ∀ i, a i ∈ I), (a.sum fun i c => c • f i) = x := by rw [← Submodule.mem_ideal_smul_span_iff_exists_sum, ← Set.image_eq_range] -theorem mem_smul_top_iff (N : Submodule R M) (x : N) : - x ∈ I • (⊤ : Submodule R N) ↔ (x : M) ∈ I • N := by - change _ ↔ N.subtype x ∈ I • N - have : Submodule.map N.subtype (I • ⊤) = I • N := by - rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype] - rw [← this] - exact (Function.Injective.mem_set_image N.injective_subtype).symm - -@[simp] -theorem smul_comap_le_comap_smul (f : M →ₗ[R] M') (S : Submodule R M') (I : Ideal R) : - I • S.comap f ≤ (I • S).comap f := by - refine Submodule.smul_le.mpr fun r hr x hx => ?_ - rw [Submodule.mem_comap] at hx ⊢ - rw [f.map_smul] - exact Submodule.smul_mem_smul hr hx - end CommSemiring end Submodule @@ -370,16 +301,12 @@ theorem sum_eq_sup {ι : Type*} (s : Finset ι) (f : ι → Ideal R) : s.sum f = end Add -section MulAndRadical +section Semiring -variable {R : Type u} {ι : Type*} [CommSemiring R] -variable {I J K L : Ideal R} - -instance : Mul (Ideal R) := - ⟨(· • ·)⟩ +variable {R : Type u} [Semiring R] {I J K L : Ideal R} @[simp] -theorem one_eq_top : (1 : Ideal R) = ⊤ := by erw [Submodule.one_eq_range, LinearMap.range_id] +theorem one_eq_top : (1 : Ideal R) = ⊤ := Ideal.span_singleton_one theorem add_eq_one_iff : I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1 := by rw [one_eq_top, eq_top_iff_one, add_eq_sup, Submodule.mem_sup] @@ -387,12 +314,104 @@ theorem add_eq_one_iff : I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1 := by theorem mul_mem_mul {r s} (hr : r ∈ I) (hs : s ∈ J) : r * s ∈ I * J := Submodule.smul_mem_smul hr hs -theorem mul_mem_mul_rev {r s} (hr : r ∈ I) (hs : s ∈ J) : s * r ∈ I * J := - mul_comm r s ▸ mul_mem_mul hr hs - theorem pow_mem_pow {x : R} (hx : x ∈ I) (n : ℕ) : x ^ n ∈ I ^ n := Submodule.pow_mem_pow _ hx _ +theorem mul_le : I * J ≤ K ↔ ∀ r ∈ I, ∀ s ∈ J, r * s ∈ K := + Submodule.smul_le + +theorem mul_le_left : I * J ≤ J := + Ideal.mul_le.2 fun _ _ _ => J.mul_mem_left _ + +@[simp] +theorem sup_mul_left_self : I ⊔ J * I = I := + sup_eq_left.2 Ideal.mul_le_left + +@[simp] +theorem mul_left_self_sup : J * I ⊔ I = I := + sup_eq_right.2 Ideal.mul_le_left + +protected theorem mul_assoc : I * J * K = I * (J * K) := + Submodule.smul_assoc I J K + +variable (I) + +-- @[simp] -- Porting note (#10618): simp can prove this +theorem mul_bot : I * ⊥ = ⊥ := by simp + +-- @[simp] -- Porting note (#10618): simp can prove this +theorem bot_mul : ⊥ * I = ⊥ := by simp + +@[simp] +theorem top_mul : ⊤ * I = I := + Submodule.top_smul I + +variable {I} + +theorem mul_mono (hik : I ≤ K) (hjl : J ≤ L) : I * J ≤ K * L := + Submodule.smul_mono hik hjl + +theorem mul_mono_left (h : I ≤ J) : I * K ≤ J * K := + Submodule.smul_mono_left h + +theorem mul_mono_right (h : J ≤ K) : I * J ≤ I * K := + smul_mono_right I h + +variable (I J K) + +theorem mul_sup : I * (J ⊔ K) = I * J ⊔ I * K := + Submodule.smul_sup I J K + +theorem sup_mul : (I ⊔ J) * K = I * K ⊔ J * K := + Submodule.sup_smul I J K + +variable {I J K} + +theorem pow_le_pow_right {m n : ℕ} (h : m ≤ n) : I ^ n ≤ I ^ m := by + obtain _ | m := m + · rw [Submodule.pow_zero, one_eq_top]; exact le_top + obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h + simp_rw [add_comm, (· ^ ·), Pow.pow, npowRec_add _ _ m.succ_ne_zero _ I.one_mul] + exact mul_le_left + +theorem pow_le_self {n : ℕ} (hn : n ≠ 0) : I ^ n ≤ I := + calc + I ^ n ≤ I ^ 1 := pow_le_pow_right (Nat.pos_of_ne_zero hn) + _ = I := Submodule.pow_one _ + +theorem pow_right_mono {I J : Ideal R} (e : I ≤ J) (n : ℕ) : I ^ n ≤ J ^ n := by + induction' n with _ hn + · rw [Submodule.pow_zero, Submodule.pow_zero] + · rw [Submodule.pow_succ, Submodule.pow_succ] + exact Ideal.mul_mono hn e + +@[simp] +theorem mul_eq_bot {R : Type*} [CommSemiring R] [NoZeroDivisors R] {I J : Ideal R} : + I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥ := + ⟨fun hij => + or_iff_not_imp_left.mpr fun I_ne_bot => + J.eq_bot_iff.mpr fun j hj => + let ⟨i, hi, ne0⟩ := I.ne_bot_iff.mp I_ne_bot + Or.resolve_left (mul_eq_zero.mp ((I * J).eq_bot_iff.mp hij _ (mul_mem_mul hi hj))) ne0, + fun h => by obtain rfl | rfl := h; exacts [bot_mul _, mul_bot _]⟩ + +instance {R : Type*} [CommSemiring R] [NoZeroDivisors R] : NoZeroDivisors (Ideal R) where + eq_zero_or_eq_zero_of_mul_eq_zero := mul_eq_bot.1 + +instance {R : Type*} [CommSemiring R] {S : Type*} [CommRing S] [Algebra R S] + [NoZeroSMulDivisors R S] {I : Ideal S} : NoZeroSMulDivisors R I := + Submodule.noZeroSMulDivisors (Submodule.restrictScalars R I) + +end Semiring + +section MulAndRadical + +variable {R : Type u} {ι : Type*} [CommSemiring R] +variable {I J K L : Ideal R} + +theorem mul_mem_mul_rev {r s} (hr : r ∈ I) (hs : s ∈ J) : s * r ∈ I * J := + mul_comm r s ▸ mul_mem_mul hr hs + theorem prod_mem_prod {ι : Type*} {s : Finset ι} {I : ι → Ideal R} {x : ι → R} : (∀ i ∈ s, x i ∈ I i) → (∏ i ∈ s, x i) ∈ ∏ i ∈ s, I i := by classical @@ -406,12 +425,6 @@ theorem prod_mem_prod {ι : Type*} {s : Finset ι} {I : ι → Ideal R} {x : ι mul_mem_mul (h a <| Finset.mem_insert_self a s) (IH fun i hi => h i <| Finset.mem_insert_of_mem hi) -theorem mul_le : I * J ≤ K ↔ ∀ r ∈ I, ∀ s ∈ J, r * s ∈ K := - Submodule.smul_le - -theorem mul_le_left : I * J ≤ J := - Ideal.mul_le.2 fun _ _ _ => J.mul_mem_left _ - theorem mul_le_right : I * J ≤ I := Ideal.mul_le.2 fun _ hr _ _ => I.mul_mem_right _ hr @@ -419,27 +432,16 @@ theorem mul_le_right : I * J ≤ I := theorem sup_mul_right_self : I ⊔ I * J = I := sup_eq_left.2 Ideal.mul_le_right -@[simp] -theorem sup_mul_left_self : I ⊔ J * I = I := - sup_eq_left.2 Ideal.mul_le_left - @[simp] theorem mul_right_self_sup : I * J ⊔ I = I := sup_eq_right.2 Ideal.mul_le_right -@[simp] -theorem mul_left_self_sup : J * I ⊔ I = I := - sup_eq_right.2 Ideal.mul_le_left - variable (I J K) protected theorem mul_comm : I * J = J * I := le_antisymm (mul_le.2 fun _ hrI _ hsJ => mul_mem_mul_rev hsJ hrI) (mul_le.2 fun _ hrJ _ hsI => mul_mem_mul_rev hsI hrJ) -protected theorem mul_assoc : I * J * K = I * (J * K) := - Submodule.smul_assoc I J K - theorem span_mul_span (S T : Set R) : span S * span T = span (⋃ (s ∈ S) (t ∈ T), {s * t}) := Submodule.span_smul_span S T @@ -636,76 +638,11 @@ theorem pow_sup_eq_top {n : ℕ} (h : I ⊔ J = ⊤) : I ^ n ⊔ J = ⊤ := by theorem pow_sup_pow_eq_top {m n : ℕ} (h : I ⊔ J = ⊤) : I ^ m ⊔ J ^ n = ⊤ := sup_pow_eq_top (pow_sup_eq_top h) -variable (I) - --- @[simp] -- Porting note (#10618): simp can prove this -theorem mul_bot : I * ⊥ = ⊥ := by simp - --- @[simp] -- Porting note (#10618): simp can prove thisrove this -theorem bot_mul : ⊥ * I = ⊥ := by simp - +variable (I) in @[simp] theorem mul_top : I * ⊤ = I := Ideal.mul_comm ⊤ I ▸ Submodule.top_smul I -@[simp] -theorem top_mul : ⊤ * I = I := - Submodule.top_smul I - -variable {I} - -theorem mul_mono (hik : I ≤ K) (hjl : J ≤ L) : I * J ≤ K * L := - Submodule.smul_mono hik hjl - -theorem mul_mono_left (h : I ≤ J) : I * K ≤ J * K := - Submodule.smul_mono_left h - -theorem mul_mono_right (h : J ≤ K) : I * J ≤ I * K := - smul_mono_right _ h - -variable (I J K) - -theorem mul_sup : I * (J ⊔ K) = I * J ⊔ I * K := - Submodule.smul_sup I J K - -theorem sup_mul : (I ⊔ J) * K = I * K ⊔ J * K := - Submodule.sup_smul I J K - -variable {I J K} - -theorem pow_le_pow_right {m n : ℕ} (h : m ≤ n) : I ^ n ≤ I ^ m := by - cases' Nat.exists_eq_add_of_le h with k hk - rw [hk, pow_add] - exact le_trans mul_le_inf inf_le_left - -theorem pow_le_self {n : ℕ} (hn : n ≠ 0) : I ^ n ≤ I := - calc - I ^ n ≤ I ^ 1 := pow_le_pow_right (Nat.pos_of_ne_zero hn) - _ = I := pow_one _ - -theorem pow_right_mono {I J : Ideal R} (e : I ≤ J) (n : ℕ) : I ^ n ≤ J ^ n := by - induction' n with _ hn - · rw [pow_zero, pow_zero] - · rw [pow_succ, pow_succ] - exact Ideal.mul_mono hn e - -@[simp] -theorem mul_eq_bot {R : Type*} [CommSemiring R] [NoZeroDivisors R] {I J : Ideal R} : - I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥ := - ⟨fun hij => - or_iff_not_imp_left.mpr fun I_ne_bot => - J.eq_bot_iff.mpr fun _ hj => - let ⟨_, hi, ne0⟩ := I.ne_bot_iff.mp I_ne_bot - Or.resolve_left (mul_eq_zero.mp ((I * J).eq_bot_iff.mp hij _ (mul_mem_mul hi hj))) ne0, - fun h => by cases' h with h h <;> rw [← Ideal.mul_bot, h, Ideal.mul_comm]⟩ - -instance {R : Type*} [CommSemiring R] [NoZeroDivisors R] : NoZeroDivisors (Ideal R) where - eq_zero_or_eq_zero_of_mul_eq_zero := mul_eq_bot.1 - -instance {R : Type*} [CommSemiring R] {S : Type*} [CommRing S] [Algebra R S] - [NoZeroSMulDivisors R S] {I : Ideal S} : NoZeroSMulDivisors R I := - Submodule.noZeroSMulDivisors (Submodule.restrictScalars R I) - /-- A product of ideals in an integral domain is zero if and only if one of the terms is zero. -/ @[simp] lemma multiset_prod_eq_bot {R : Type*} [CommRing R] [IsDomain R] {s : Multiset (Ideal R)} : diff --git a/Mathlib/RingTheory/JacobsonIdeal.lean b/Mathlib/RingTheory/JacobsonIdeal.lean index adf95dc2bcc16..4ebd340409ee5 100644 --- a/Mathlib/RingTheory/JacobsonIdeal.lean +++ b/Mathlib/RingTheory/JacobsonIdeal.lean @@ -11,8 +11,11 @@ import Mathlib.RingTheory.TwoSidedIdeal.Operations /-! # Jacobson radical -The Jacobson radical of a ring `R` is defined to be the intersection of all maximal ideals of `R`. -This is similar to how the nilradical is equal to the intersection of all prime ideals of `R`. +The Jacobson radical of a module `M` over a ring `R` is defined to be the intersection of all +maximal submodules of `M`. The Jacobson radical of a ring `R` is the Jacobson radical of `R` as +an `R`-module, which is equal to the intersection of all maximal left ideals of `R`. +This is similar to how the nilradical of a commutative ring `R` is equal to the intersection +of all prime ideals of `R`. We can extend the idea of the nilradical of `R` to ideals of `R`, by letting the nilradical of an ideal `I` be the intersection of prime ideals containing `I`. @@ -22,7 +25,10 @@ as the intersection of maximal ideals containing `I`. ## Main definitions -Let `R` be a ring, and `I` be a left ideal of `R` +Let `R` be a ring, `I` a left ideal of `R`, and `M` an `R`-module. + +* `Module.jacobson R M` is the Jacobson radical of `M`, +i.e. the infimum of all maximal submodules in `M`. * `Ideal.jacobson I` is the Jacobson radical, i.e. the infimum of all maximal ideals containing `I`. @@ -48,6 +54,19 @@ Jacobson, Jacobson radical, Local Ideal universe u v +namespace Module + +variable (R : Type u) (M : Type v) + +/-- The Jacobson radical of an `R`-module `M` is the infimum of all maximal submodules in `M`. -/ +def jacobson : Submodule R M := + sInf { m : Submodule R M | IsCoatom m } + + + + +end Module + namespace Ideal variable {R : Type u} {S : Type v} From c31a232042f1d4731f0afb6b94204c1a94905827 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sun, 13 Oct 2024 18:17:58 -0400 Subject: [PATCH 02/23] Discard changes to Mathlib/RingTheory/JacobsonIdeal.lean --- Mathlib/RingTheory/JacobsonIdeal.lean | 25 +++---------------------- 1 file changed, 3 insertions(+), 22 deletions(-) diff --git a/Mathlib/RingTheory/JacobsonIdeal.lean b/Mathlib/RingTheory/JacobsonIdeal.lean index 4ebd340409ee5..adf95dc2bcc16 100644 --- a/Mathlib/RingTheory/JacobsonIdeal.lean +++ b/Mathlib/RingTheory/JacobsonIdeal.lean @@ -11,11 +11,8 @@ import Mathlib.RingTheory.TwoSidedIdeal.Operations /-! # Jacobson radical -The Jacobson radical of a module `M` over a ring `R` is defined to be the intersection of all -maximal submodules of `M`. The Jacobson radical of a ring `R` is the Jacobson radical of `R` as -an `R`-module, which is equal to the intersection of all maximal left ideals of `R`. -This is similar to how the nilradical of a commutative ring `R` is equal to the intersection -of all prime ideals of `R`. +The Jacobson radical of a ring `R` is defined to be the intersection of all maximal ideals of `R`. +This is similar to how the nilradical is equal to the intersection of all prime ideals of `R`. We can extend the idea of the nilradical of `R` to ideals of `R`, by letting the nilradical of an ideal `I` be the intersection of prime ideals containing `I`. @@ -25,10 +22,7 @@ as the intersection of maximal ideals containing `I`. ## Main definitions -Let `R` be a ring, `I` a left ideal of `R`, and `M` an `R`-module. - -* `Module.jacobson R M` is the Jacobson radical of `M`, -i.e. the infimum of all maximal submodules in `M`. +Let `R` be a ring, and `I` be a left ideal of `R` * `Ideal.jacobson I` is the Jacobson radical, i.e. the infimum of all maximal ideals containing `I`. @@ -54,19 +48,6 @@ Jacobson, Jacobson radical, Local Ideal universe u v -namespace Module - -variable (R : Type u) (M : Type v) - -/-- The Jacobson radical of an `R`-module `M` is the infimum of all maximal submodules in `M`. -/ -def jacobson : Submodule R M := - sInf { m : Submodule R M | IsCoatom m } - - - - -end Module - namespace Ideal variable {R : Type u} {S : Type v} From 71046e259ae16763cfbb881369b4018e277e48d4 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 14 Oct 2024 00:56:56 +0200 Subject: [PATCH 03/23] fixes --- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean | 6 ++++-- Mathlib/RingTheory/Ideal/Colon.lean | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean index 9f3d2d832688e..bfd1de5bdddd8 100644 --- a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean +++ b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean @@ -736,7 +736,8 @@ 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 +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 @@ -759,7 +760,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/RingTheory/Ideal/Colon.lean b/Mathlib/RingTheory/Ideal/Colon.lean index 903322d97d3f7..9d4dd89b510fc 100644 --- a/Mathlib/RingTheory/Ideal/Colon.lean +++ b/Mathlib/RingTheory/Ideal/Colon.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Kenny Lau -/ import Mathlib.LinearAlgebra.Quotient -import Mathlib.RingTheory.Ideal.Operations +import Mathlib.RingTheory.Ideal.Maps /-! # The colon ideal From fb0536c97e50598a8933d4f74e5dd88026735562 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 14 Oct 2024 01:56:13 +0200 Subject: [PATCH 04/23] fixes --- .../LinearAlgebra/TensorAlgebra/Basic.lean | 2 +- .../TensorProduct/Submodule.lean | 20 +++++++++++-------- Mathlib/RingTheory/Finiteness.lean | 4 ++-- 3 files changed, 15 insertions(+), 11 deletions(-) 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/Finiteness.lean b/Mathlib/RingTheory/Finiteness.lean index 9b6993825be28..c07ba303adbdb 100644 --- a/Mathlib/RingTheory/Finiteness.lean +++ b/Mathlib/RingTheory/Finiteness.lean @@ -432,8 +432,8 @@ section Mul variable {R : Type*} {A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] variable {M N : Submodule R A} -theorem FG.mul (hm : M.FG) (hn : N.FG) : (M * N).FG := - hm.map₂ _ hn +theorem FG.mul (hm : M.FG) (hn : N.FG) : (M * N).FG := by + rw [mul_eq_map₂]; exact hm.map₂ _ hn theorem FG.pow (h : M.FG) (n : ℕ) : (M ^ n).FG := Nat.recOn n ⟨{1}, by simp [one_eq_span]⟩ fun n ih => by simpa [pow_succ] using ih.mul h From 3cbb1e92c253c64f737e57a256e9b23286634466 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 14 Oct 2024 20:45:23 +0200 Subject: [PATCH 05/23] fixes --- .../LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean | 3 ++- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean | 4 ++-- Mathlib/RingTheory/FractionalIdeal/Basic.lean | 2 +- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean b/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean index 17254b66084e3..840f163aeeee0 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/TensorProduct/RightExactness.lean b/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean index 14d7396e79842..9f314085ec704 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean @@ -430,8 +430,8 @@ noncomputable def quotTensorEquivQuotSMul (I : Ideal R) : (rTensor.equiv M (exact_subtype_mkQ I) I.mkQ_surjective).symm.trans <| Submodule.Quotient.equiv _ _ (TensorProduct.lid R M) <| Eq.trans (LinearMap.range_comp _ _).symm <| - Eq.trans ((Submodule.topEquiv.lTensor I).range_comp _).symm <| - Eq.symm <| Eq.trans (map₂_eq_range_lift_comp_mapIncl _ _ _) <| + Eq.trans ((Submodule.topEquiv.lTensor I).range_comp _).symm <| Eq.symm <| + (Submodule.smul_eq_map₂.trans <| map₂_eq_range_lift_comp_mapIncl _ _ _).trans <| congrArg _ (TensorProduct.ext' (fun _ _ => rfl)) /-- Right tensoring a module with a quotient of the ring is the same as 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) : From 810908a52b65123e8bd1091a51702164f02dbb55 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 14 Oct 2024 21:56:01 +0200 Subject: [PATCH 06/23] fixes --- Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean | 8 ++++---- Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean | 4 ++-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean | 3 ++- Mathlib/LinearAlgebra/LinearDisjoint.lean | 4 ++-- Mathlib/RingTheory/Ideal/Cotangent.lean | 3 ++- 5 files changed, 12 insertions(+), 10 deletions(-) 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 e5f6c2be85383..b013a0dea4667 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/ExteriorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean index cd48d0d7611d4..cc09f7a2f5336 100644 --- a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean @@ -237,7 +237,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/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 9ce01fea0e26b..77ace6699c812 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -150,7 +150,8 @@ theorem cotangentEquivIdeal_apply (x : I.Cotangent) : theorem cotangentEquivIdeal_symm_apply (x : R) (hx : x ∈ I) : -- Note: #8386 had to specify `(R₂ := R)` because `I.toCotangent` suggested `R ⧸ I^2` instead I.cotangentEquivIdeal.symm ⟨(I ^ 2).mkQ x, - Submodule.mem_map_of_mem (F := R →ₗ[R] R ⧸ I ^ 2) (f := (I ^ 2).mkQ) hx⟩ = + -- timeout (200000 heartbeats) without `by exact` + by exact Submodule.mem_map_of_mem (F := R →ₗ[R] R ⧸ I ^ 2) (f := (I ^ 2).mkQ) hx⟩ = I.toCotangent (R := R) ⟨x, hx⟩ := by apply I.cotangentEquivIdeal.injective rw [I.cotangentEquivIdeal.apply_symm_apply] From 0c22392dadb21d08d839357c622bc07a6360f3e6 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 14 Oct 2024 22:12:15 +0200 Subject: [PATCH 07/23] fixes --- Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean | 2 +- Mathlib/RingTheory/DedekindDomain/PID.lean | 2 +- Mathlib/RingTheory/Kaehler/Basic.lean | 6 ++++-- 3 files changed, 6 insertions(+), 4 deletions(-) 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/DedekindDomain/PID.lean b/Mathlib/RingTheory/DedekindDomain/PID.lean index 258435cca7f9a..c8f81c06b067d 100644 --- a/Mathlib/RingTheory/DedekindDomain/PID.lean +++ b/Mathlib/RingTheory/DedekindDomain/PID.lean @@ -123,7 +123,7 @@ theorem FractionalIdeal.isPrincipal.of_finite_maximals_of_inv {A : Type*} [CommR SetLike.exists_of_lt ((IsLocalization.coeSubmodule_strictMono hS (hf.mem_toFinset.1 hM).ne_top.lt_top).trans_eq hinv.symm) - exact hxM (Submodule.map₂_le.2 h hx) + exact hxM (Submodule.mul_le.2 h hx) choose! a ha b hb hm using this choose! u hu hum using fun M hM => SetLike.not_le_iff_exists.1 (nle M hM) let v := ∑ M ∈ s, u M • b M diff --git a/Mathlib/RingTheory/Kaehler/Basic.lean b/Mathlib/RingTheory/Kaehler/Basic.lean index daf09320aeba7..40a8b8b474c92 100644 --- a/Mathlib/RingTheory/Kaehler/Basic.lean +++ b/Mathlib/RingTheory/Kaehler/Basic.lean @@ -815,12 +815,14 @@ def KaehlerDifferential.kerToTensor : noncomputable def KaehlerDifferential.kerCotangentToTensor : (RingHom.ker (algebraMap A B)).Cotangent →ₗ[A] B ⊗[A] Ω[A⁄R] := - Submodule.liftQ _ (kerToTensor R A B) (iSup_le_iff.mpr (by + Submodule.liftQ _ (kerToTensor R A B) <| by + rw [Submodule.smul_eq_map₂] + apply iSup_le_iff.mpr simp only [Submodule.map_le_iff_le_comap, Subtype.forall] rintro x hx y - simp only [Submodule.mem_comap, LinearMap.lsmul_apply, LinearMap.mem_ker, map_smul, kerToTensor_apply, TensorProduct.smul_tmul', ← algebraMap_eq_smul_one, - RingHom.mem_ker.mp hx, TensorProduct.zero_tmul])) + RingHom.mem_ker.mp hx, TensorProduct.zero_tmul] @[simp] lemma KaehlerDifferential.kerCotangentToTensor_toCotangent (x) : From 2af93aecad88d7b5d2ef2825aa23012adfa9dc8b Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 14 Oct 2024 22:28:38 +0200 Subject: [PATCH 08/23] fixes --- Mathlib/RingTheory/DedekindDomain/Different.lean | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/Mathlib/RingTheory/DedekindDomain/Different.lean b/Mathlib/RingTheory/DedekindDomain/Different.lean index 915f686f016f1..e4988f1c39a25 100644 --- a/Mathlib/RingTheory/DedekindDomain/Different.lean +++ b/Mathlib/RingTheory/DedekindDomain/Different.lean @@ -57,7 +57,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 @@ -147,14 +147,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)] @@ -260,7 +261,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) @@ -298,6 +299,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)] @@ -410,7 +412,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 @@ -557,7 +559,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 _⟩ From e3e517d9f4a52747d765a4925b27372caeaf9ea7 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 14 Oct 2024 19:21:03 -0400 Subject: [PATCH 09/23] missing docstring --- Mathlib/Algebra/Group/Subgroup/Pointwise.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Algebra/Group/Subgroup/Pointwise.lean b/Mathlib/Algebra/Group/Subgroup/Pointwise.lean index 0ba849fba4351..d3eb3c9eb8e56 100644 --- a/Mathlib/Algebra/Group/Subgroup/Pointwise.lean +++ b/Mathlib/Algebra/Group/Subgroup/Pointwise.lean @@ -547,6 +547,8 @@ section Mul variable {R : Type*} [NonUnitalNonAssocRing R] +/-- For additive subgroups `S` and `T` of a ring, the product of `S` and `T` as submonoids +is automatically a subgroup, which we define as the product of `S` and `T` as subgroups. -/ protected def mul : Mul (AddSubgroup R) where mul M N := { __ := M.toAddSubmonoid * N.toAddSubmonoid From ff7e3bb23f2e8b1ed736e84eb09532e7c06d9cc5 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Fri, 18 Oct 2024 21:48:42 +0000 Subject: [PATCH 10/23] fixes --- .../LinearAlgebra/TensorProduct/Quotient.lean | 33 +++++++------------ Mathlib/RingTheory/Ideal/Maps.lean | 6 ++-- 2 files changed, 15 insertions(+), 24 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean index f3cea863abf53..5bf265cb6fa82 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean @@ -5,7 +5,7 @@ Authors: Antoine Chambert-Loir, Jujian Zhang -/ import Mathlib.RingTheory.Ideal.Operations -import Mathlib.LinearAlgebra.TensorProduct.Basic +import Mathlib.LinearAlgebra.TensorProduct.RightExactness import Mathlib.LinearAlgebra.Quotient import Mathlib.LinearAlgebra.Prod import Mathlib.RingTheory.Ideal.Quotient @@ -60,11 +60,11 @@ noncomputable def quotientTensorQuotientEquiv (m : Submodule R M) (n : Submodule simp only [LinearMap.compr₂_apply, LinearMap.flip_apply, mk_apply, Submodule.mkQ_apply, LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero] exact Submodule.mem_sup_right ⟨y ⊗ₜ ⟨x, hx⟩, rfl⟩) fun x hx => by - ext y - simp only [LinearMap.coe_comp, Function.comp_apply, Submodule.mkQ_apply, LinearMap.flip_apply, - Submodule.liftQ_apply, LinearMap.compr₂_apply, mk_apply, LinearMap.zero_comp, - LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero] - exact Submodule.mem_sup_left ⟨⟨x, hx⟩ ⊗ₜ y, rfl⟩) + ext y + simp only [LinearMap.coe_comp, Function.comp_apply, Submodule.mkQ_apply, + LinearMap.flip_apply, Submodule.liftQ_apply, LinearMap.compr₂_apply, mk_apply, + LinearMap.zero_comp, LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero] + exact Submodule.mem_sup_left ⟨⟨x, hx⟩ ⊗ₜ y, rfl⟩) (Submodule.liftQ _ (map (Submodule.mkQ _) (Submodule.mkQ _)) fun x hx => by rw [Submodule.mem_sup] at hx rcases hx with ⟨_, ⟨a, rfl⟩, _, ⟨b, rfl⟩, rfl⟩ @@ -156,21 +156,12 @@ variable (M) in quotienting that module by the corresponding submodule. -/ noncomputable def quotTensorEquivQuotSMul (I : Ideal R) : ((R ⧸ I) ⊗[R] M) ≃ₗ[R] M ⧸ (I • (⊤ : Submodule R M)) := - quotientTensorEquiv M I ≪≫ₗ - Submodule.Quotient.equiv (M := R ⊗[R] M) (N := M) (f := TensorProduct.lid R M) (hf := rfl) ≪≫ₗ - Submodule.Quotient.equiv _ _ (LinearEquiv.refl R M) (by - erw [Submodule.map_id] - rw [TensorProduct.map_range_eq_span_tmul, Submodule.map_span] - refine le_antisymm (Submodule.span_le.2 ?_) (Submodule.map₂_le.2 ?_) - · rintro _ ⟨_, ⟨r, m, rfl⟩, rfl⟩ - simp only [Submodule.coe_subtype, LinearMap.id_coe, id_eq, lid_tmul, SetLike.mem_coe] - apply Submodule.apply_mem_map₂ <;> aesop - · rintro r hr m - - simp only [Submodule.coe_subtype, LinearMap.id_coe, id_eq, Subtype.exists, exists_prop, - LinearMap.lsmul_apply] - refine Submodule.subset_span ?_ - simp only [Set.mem_image, Set.mem_setOf_eq] - exact ⟨r ⊗ₜ m, ⟨r, hr, m, rfl⟩, rfl⟩) + (rTensor.equiv M (LinearMap.exact_subtype_mkQ I) I.mkQ_surjective).symm.trans <| + Submodule.Quotient.equiv _ _ (TensorProduct.lid R M) <| + Eq.trans (LinearMap.range_comp _ _).symm <| + Eq.trans ((Submodule.topEquiv.lTensor I).range_comp _).symm <| Eq.symm <| + (Submodule.smul_eq_map₂.trans <| map₂_eq_range_lift_comp_mapIncl _ _ _).trans <| + congrArg _ (TensorProduct.ext' (fun _ _ => rfl)) variable (M) in /-- Right tensoring a module with a quotient of the ring is the same as diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean index 21459bbb292b8..d755792c2a7d0 100644 --- a/Mathlib/RingTheory/Ideal/Maps.lean +++ b/Mathlib/RingTheory/Ideal/Maps.lean @@ -720,13 +720,13 @@ theorem mem_annihilator_span (s : Set M) (r : R) : · intro h n exact h _ (Submodule.subset_span n.prop) · intro h n hn - refine Submodule.span_induction hn ?_ ?_ ?_ ?_ + refine Submodule.span_induction ?_ ?_ ?_ ?_ hn · intro x hx exact h ⟨x, hx⟩ · exact smul_zero _ - · intro x y hx hy + · intro x y _ _ hx hy rw [smul_add, hx, hy, zero_add] - · intro a x hx + · intro a x _ hx rw [smul_comm, hx, smul_zero] theorem mem_annihilator_span_singleton (g : M) (r : R) : From 54e02d44fcf860da04386c5eba2b7444e80a6393 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sat, 26 Oct 2024 20:52:50 +0000 Subject: [PATCH 11/23] fixes --- Mathlib/Algebra/Algebra/Operations.lean | 8 ++--- Mathlib/RingTheory/Ideal/Operations.lean | 39 ++++++++++++------------ 2 files changed, 23 insertions(+), 24 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean index 9f156250ccde6..3843f96e73124 100644 --- a/Mathlib/Algebra/Algebra/Operations.lean +++ b/Mathlib/Algebra/Algebra/Operations.lean @@ -148,9 +148,9 @@ theorem bot_mul : ⊥ * M = ⊥ := protected theorem one_mul : (1 : Submodule R A) * M = M := by refine le_antisymm (mul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_ - · obtain ⟨r, rfl⟩ := mem_span_singleton.mp hr - rw [smul_one_mul]; exact M.smul_mem r hm - · rw [← one_mul m]; exact mul_mem_mul (subset_span rfl) hm + · obtain ⟨r, rfl⟩ := hr + rw [LinearMap.toSpanSingleton_apply, smul_one_mul]; exact M.smul_mem r hm + · rw [← one_mul m]; exact mul_mem_mul (one_le.mp le_rfl) hm variable {M} @@ -239,7 +239,7 @@ end Module variable {ι : Sort uι} variable {R : Type u} [CommSemiring R] -section Ring +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} diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index 598e08c592546..c664506cb50f8 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/Mathlib/RingTheory/Ideal/Operations.lean @@ -306,7 +306,8 @@ section Semiring variable {R : Type u} [Semiring R] {I J K L : Ideal R} @[simp] -theorem one_eq_top : (1 : Ideal R) = ⊤ := Ideal.span_singleton_one +theorem one_eq_top : (1 : Ideal R) = ⊤ := by + rw [Submodule.one_eq_span, ← Ideal.span, Ideal.span_singleton_one] theorem add_eq_one_iff : I + J = 1 ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1 := by rw [one_eq_top, eq_top_iff_one, add_eq_sup, Submodule.mem_sup] @@ -377,15 +378,14 @@ theorem pow_le_self {n : ℕ} (hn : n ≠ 0) : I ^ n ≤ I := I ^ n ≤ I ^ 1 := pow_le_pow_right (Nat.pos_of_ne_zero hn) _ = I := Submodule.pow_one _ -theorem pow_right_mono {I J : Ideal R} (e : I ≤ J) (n : ℕ) : I ^ n ≤ J ^ n := by +theorem pow_right_mono (e : I ≤ J) (n : ℕ) : I ^ n ≤ J ^ n := by induction' n with _ hn · rw [Submodule.pow_zero, Submodule.pow_zero] · rw [Submodule.pow_succ, Submodule.pow_succ] exact Ideal.mul_mono hn e @[simp] -theorem mul_eq_bot {R : Type*} [CommSemiring R] [NoZeroDivisors R] {I J : Ideal R} : - I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥ := +theorem mul_eq_bot [NoZeroDivisors R] : I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥ := ⟨fun hij => or_iff_not_imp_left.mpr fun I_ne_bot => J.eq_bot_iff.mpr fun j hj => @@ -393,24 +393,10 @@ theorem mul_eq_bot {R : Type*} [CommSemiring R] [NoZeroDivisors R] {I J : Ideal Or.resolve_left (mul_eq_zero.mp ((I * J).eq_bot_iff.mp hij _ (mul_mem_mul hi hj))) ne0, fun h => by obtain rfl | rfl := h; exacts [bot_mul _, mul_bot _]⟩ -lemma sup_pow_add_le_pow_sup_pow {R} [CommSemiring R] {I J : Ideal R} {n m : ℕ} : - (I ⊔ J) ^ (n + m) ≤ I ^ n ⊔ J ^ m := by - rw [← Ideal.add_eq_sup, ← Ideal.add_eq_sup, add_pow, Ideal.sum_eq_sup] - apply Finset.sup_le - intros i hi - by_cases hn : n ≤ i - · exact (Ideal.mul_le_right.trans (Ideal.mul_le_right.trans - ((Ideal.pow_le_pow_right hn).trans le_sup_left))) - · refine (Ideal.mul_le_right.trans (Ideal.mul_le_left.trans - ((Ideal.pow_le_pow_right ?_).trans le_sup_right))) - simp only [Finset.mem_range, Nat.lt_succ] at hi - rw [Nat.le_sub_iff_add_le hi] - nlinarith - -instance {R : Type*} [CommSemiring R] [NoZeroDivisors R] : NoZeroDivisors (Ideal R) where +instance [NoZeroDivisors R] : NoZeroDivisors (Ideal R) where eq_zero_or_eq_zero_of_mul_eq_zero := mul_eq_bot.1 -instance {R : Type*} [CommSemiring R] {S : Type*} [CommRing S] [Algebra R S] +instance {R : Type*} [CommSemiring R] {S : Type*} [Semiring S] [Algebra R S] [NoZeroSMulDivisors R S] {I : Ideal S} : NoZeroSMulDivisors R I := Submodule.noZeroSMulDivisors (Submodule.restrictScalars R I) @@ -448,6 +434,19 @@ theorem sup_mul_right_self : I ⊔ I * J = I := theorem mul_right_self_sup : I * J ⊔ I = I := sup_eq_right.2 Ideal.mul_le_right +lemma sup_pow_add_le_pow_sup_pow {n m : ℕ} : (I ⊔ J) ^ (n + m) ≤ I ^ n ⊔ J ^ m := by + rw [← Ideal.add_eq_sup, ← Ideal.add_eq_sup, add_pow, Ideal.sum_eq_sup] + apply Finset.sup_le + intros i hi + by_cases hn : n ≤ i + · exact (Ideal.mul_le_right.trans (Ideal.mul_le_right.trans + ((Ideal.pow_le_pow_right hn).trans le_sup_left))) + · refine (Ideal.mul_le_right.trans (Ideal.mul_le_left.trans + ((Ideal.pow_le_pow_right ?_).trans le_sup_right))) + simp only [Finset.mem_range, Nat.lt_succ] at hi + rw [Nat.le_sub_iff_add_le hi] + nlinarith + variable (I J K) protected theorem mul_comm : I * J = J * I := From b6a7eb95f7f192e28ff922f2d05f6883ab6f2e46 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sun, 27 Oct 2024 00:22:15 +0000 Subject: [PATCH 12/23] refactor: generalize AddSubmonoid Mul lemmas to SMul --- Mathlib/Algebra/Algebra/Operations.lean | 8 +- .../Algebra/Group/Submonoid/Pointwise.lean | 146 ++++++++++-------- .../Algebra/GroupWithZero/Action/Defs.lean | 2 +- Mathlib/Algebra/Module/Defs.lean | 3 + 4 files changed, 93 insertions(+), 66 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean index 3843f96e73124..fee60eadd7ee2 100644 --- a/Mathlib/Algebra/Algebra/Operations.lean +++ b/Mathlib/Algebra/Algebra/Operations.lean @@ -168,11 +168,11 @@ variable (M N P) theorem mul_sup : M * (N ⊔ P) = M * N ⊔ M * P := toAddSubmonoid_injective <| by - simp_rw [mul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.mul_sup, mul_toAddSubmonoid] + simp only [mul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.mul_sup] theorem sup_mul : (M ⊔ N) * P = M * P ⊔ N * P := toAddSubmonoid_injective <| by - simp_rw [mul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.sup_mul, mul_toAddSubmonoid] + simp only [mul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.sup_mul] theorem mul_subset_mul : (↑M : Set A) * (↑N : Set A) ⊆ (↑(M * N) : Set A) := AddSubmonoid.mul_subset_mul @@ -187,11 +187,11 @@ variable {ι : Sort uι} theorem iSup_mul (s : ι → Submodule R A) (t : Submodule R A) : (⨆ i, s i) * t = ⨆ i, s i * t := toAddSubmonoid_injective <| by - simp_rw [mul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.iSup_mul, mul_toAddSubmonoid] + simp only [mul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.iSup_mul] theorem mul_iSup (t : Submodule R A) (s : ι → Submodule R A) : (t * ⨆ i, s i) = ⨆ i, t * s i := toAddSubmonoid_injective <| by - simp_rw [mul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.mul_iSup, mul_toAddSubmonoid] + simp only [mul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.mul_iSup] /-- Sub-`R`-modules of an `R`-module form an idempotent semiring. -/ instance : NonUnitalSemiring (Submodule R A) where diff --git a/Mathlib/Algebra/Group/Submonoid/Pointwise.lean b/Mathlib/Algebra/Group/Submonoid/Pointwise.lean index 74f18f06313d8..9f032c5d53880 100644 --- a/Mathlib/Algebra/Group/Submonoid/Pointwise.lean +++ b/Mathlib/Algebra/Group/Submonoid/Pointwise.lean @@ -436,6 +436,69 @@ theorem one_eq_closure_one_set : (1 : AddSubmonoid R) = closure 1 := end AddMonoidWithOne +section SMul + +variable [AddMonoid R] [DistribSMul R A] + +/-- For `M : Submonoid R` and `N : AddSubmonoid A`, `M • N` is the additive submonoid +generated by all `m • n` where `m ∈ M` and `n ∈ N`. -/ +protected def smul : SMul (AddSubmonoid R) (AddSubmonoid A) where + smul M N := ⨆ s : M, N.map (DistribSMul.toAddMonoidHom A s.1) + +scoped[Pointwise] attribute [instance] AddSubmonoid.smul + +variable {M M' : AddSubmonoid R} {N P : AddSubmonoid A} {m : R} {n : A} + +theorem smul_mem_smul (hm : m ∈ M) (hn : n ∈ N) : m • n ∈ M • N := + (le_iSup _ ⟨m, hm⟩ : _ ≤ M • N) ⟨n, hn, by rfl⟩ + +theorem smul_le : M • N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m • n ∈ P := + ⟨fun H _m hm _n hn => H <| smul_mem_smul hm hn, fun H => + iSup_le fun ⟨m, hm⟩ => map_le_iff_le_comap.2 fun n hn => H m hm n hn⟩ + +@[elab_as_elim] +protected theorem smul_induction_on {C : A → Prop} {a : A} (ha : a ∈ M • N) + (hm : ∀ m ∈ M, ∀ n ∈ N, C (m • n)) (hadd : ∀ x y, C x → C y → C (x + y)) : C a := + (@smul_le _ _ _ _ _ _ _ ⟨⟨setOf C, hadd _ _⟩, by + simpa only [smul_zero] using hm _ (zero_mem _) _ (zero_mem _)⟩).2 hm ha + +@[simp] +theorem addSubmonoid_smul_bot (S : AddSubmonoid R) : S • (⊥ : AddSubmonoid A) = ⊥ := + eq_bot_iff.2 <| smul_le.2 fun m _ n hn => by + rw [AddSubmonoid.mem_bot] at hn ⊢; rw [hn, smul_zero] + +theorem smul_le_smul (h : M ≤ M') (hnp : N ≤ P) : M • N ≤ M' • P := + smul_le.2 fun _m hm _n hn => smul_mem_smul (h hm) (hnp hn) + +theorem smul_le_smul_left (h : M ≤ M') : M • P ≤ M' • P := + smul_le_smul h le_rfl + +theorem smul_le_smul_right (h : N ≤ P) : M • N ≤ M • P := + smul_le_smul le_rfl h + +theorem smul_subset_smul : (↑M : Set R) • (↑N : Set A) ⊆ (↑(M • N) : Set A) := + smul_subset_iff.2 fun _i hi _j hj ↦ smul_mem_smul hi hj + +theorem addSubmonoid_smul_sup : M • (N ⊔ P) = M • N ⊔ M • P := + le_antisymm (smul_le.mpr fun m hm np hnp ↦ by + refine closure_induction (p := fun x _ ↦ _ • x ∈ _) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp) + · rintro x (hx | hx) + exacts [le_sup_left (a := M • N) (smul_mem_smul hm hx), + le_sup_right (a := M • N) (smul_mem_smul hm hx)] + · apply (smul_zero (A := A) m).symm ▸ (M • N ⊔ M • P).zero_mem + · intros _ _ _ _ h1 h2; rw [smul_add]; exact add_mem h1 h2) + (sup_le (smul_le_smul_right le_sup_left) <| smul_le_smul_right le_sup_right) + +variable {ι : Sort*} + +theorem smul_iSup (T : AddSubmonoid R) (S : ι → AddSubmonoid A) : (T • ⨆ i, S i) = ⨆ i, T • S i := + le_antisymm (smul_le.mpr fun t ht s hs ↦ iSup_induction _ (C := (t • · ∈ _)) hs + (fun i s hs ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs) + (by simp_rw [smul_zero]; apply zero_mem) fun x y ↦ by simp_rw [smul_add]; apply add_mem) <| + iSup_le fun i ↦ smul_le_smul_right (le_iSup _ i) + +end SMul + section NonUnitalNonAssocSemiring variable [NonUnitalNonAssocSemiring R] @@ -446,21 +509,22 @@ protected def mul : Mul (AddSubmonoid R) := ⟨fun M N => ⨆ s : M, N.map (AddMonoidHom.mul s.1)⟩ scoped[Pointwise] attribute [instance] AddSubmonoid.mul +example {R} [Semiring R] : Mul.toSMul (AddSubmonoid R) = AddSubmonoid.smul := rfl + theorem mul_mem_mul {M N : AddSubmonoid R} {m n : R} (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N := - (le_iSup _ ⟨m, hm⟩ : _ ≤ M * N) ⟨n, hn, by rfl⟩ + smul_mem_smul hm hn theorem mul_le {M N P : AddSubmonoid R} : M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P := - ⟨fun H _m hm _n hn => H <| mul_mem_mul hm hn, fun H => - iSup_le fun ⟨m, hm⟩ => map_le_iff_le_comap.2 fun n hn => H m hm n hn⟩ + smul_le @[elab_as_elim] protected theorem mul_induction_on {M N : AddSubmonoid R} {C : R → Prop} {r : R} (hr : r ∈ M * N) (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)) (ha : ∀ x y, C x → C y → C (x + y)) : C r := - (@mul_le _ _ _ _ ⟨⟨setOf C, ha _ _⟩, by - simpa only [zero_mul] using hm _ (zero_mem _) _ (zero_mem _)⟩).2 hm hr + AddSubmonoid.smul_induction_on hr hm ha -- this proof is copied directly from `Submodule.span_mul_span` -- Porting note: proof rewritten +-- need `add_smul` to generalize to `SMul` theorem closure_mul_closure (S T : Set R) : closure S * closure T = closure (S * T) := by apply le_antisymm · refine mul_le.2 fun a ha b hb => ?_ @@ -480,9 +544,9 @@ theorem mul_eq_closure_mul_set (M N : AddSubmonoid R) : @[simp] theorem mul_bot (S : AddSubmonoid R) : S * ⊥ = ⊥ := - eq_bot_iff.2 <| mul_le.2 fun m _ n hn => by - rw [AddSubmonoid.mem_bot] at hn ⊢; rw [hn, mul_zero] + addSubmonoid_smul_bot S +-- need `zero_smul` to generalize to `SMul` @[simp] theorem bot_mul (S : AddSubmonoid R) : ⊥ * S = ⊥ := eq_bot_iff.2 <| mul_le.2 fun m hm n _ => by @@ -492,23 +556,21 @@ variable {M N P Q : AddSubmonoid R} @[mono] theorem mul_le_mul (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q := - mul_le.2 fun _m hm _n hn => mul_mem_mul (hmp hm) (hnq hn) + smul_le_smul hmp hnq theorem mul_le_mul_left (h : M ≤ N) : M * P ≤ N * P := - mul_le_mul h (le_refl P) + smul_le_smul_left h theorem mul_le_mul_right (h : N ≤ P) : M * N ≤ M * P := - mul_le_mul (le_refl M) h + smul_le_smul_right h theorem mul_subset_mul : (↑M : Set R) * (↑N : Set R) ⊆ (↑(M * N) : Set R) := - mul_subset_iff.2 fun _i hi _j hj ↦ mul_mem_mul hi hj + smul_subset_smul theorem mul_sup : M * (N ⊔ P) = M * N ⊔ M * P := - le_antisymm (mul_le.mpr fun m hm np hnp ↦ by - obtain ⟨n, hn, p, hp, rfl⟩ := mem_sup.mp hnp - rw [left_distrib]; exact add_mem_sup (mul_mem_mul hm hn) <| mul_mem_mul hm hp) - (sup_le (mul_le_mul_right le_sup_left) <| mul_le_mul_right le_sup_right) + addSubmonoid_smul_sup +-- need `zero_smul` and `add_smul` to generalize to `SMul` theorem sup_mul : (M ⊔ N) * P = M * P ⊔ N * P := le_antisymm (mul_le.mpr fun mn hmn p hp ↦ by obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn @@ -517,6 +579,7 @@ theorem sup_mul : (M ⊔ N) * P = M * P ⊔ N * P := variable {ι : Sort*} +-- need `zero_smul` and `add_smul` to generalize to `SMul` theorem iSup_mul (S : ι → AddSubmonoid R) (T : AddSubmonoid R) : (⨆ i, S i) * T = ⨆ i, S i * T := le_antisymm (mul_le.mpr fun s hs t ht ↦ iSup_induction _ (C := (· * t ∈ _)) hs (fun i s hs ↦ mem_iSup_of_mem i <| mul_mem_mul hs ht) (by simp_rw [zero_mul]; apply zero_mem) @@ -524,10 +587,7 @@ theorem iSup_mul (S : ι → AddSubmonoid R) (T : AddSubmonoid R) : (⨆ i, S i) iSup_le fun i ↦ mul_le_mul_left (le_iSup _ i) theorem mul_iSup (T : AddSubmonoid R) (S : ι → AddSubmonoid R) : (T * ⨆ i, S i) = ⨆ i, T * S i := - le_antisymm (mul_le.mpr fun t ht s hs ↦ iSup_induction _ (C := (t * · ∈ _)) hs - (fun i s hs ↦ mem_iSup_of_mem i <| mul_mem_mul ht hs) (by simp_rw [mul_zero]; apply zero_mem) - fun _ _ ↦ by simp_rw [left_distrib]; apply add_mem) <| - iSup_le fun i ↦ mul_le_mul_right (le_iSup _ i) + smul_iSup T S end NonUnitalNonAssocSemiring @@ -582,15 +642,12 @@ protected def semigroup : Semigroup (AddSubmonoid R) where mul := (· * ·) mul_assoc M N P := le_antisymm - (mul_le.2 fun _mn hmn p hp => - suffices M * N ≤ (M * (N * P)).comap (AddMonoidHom.mulRight p) from this hmn - mul_le.2 fun m hm n hn => - show m * n * p ∈ M * (N * P) from - (mul_assoc m n p).symm ▸ mul_mem_mul hm (mul_mem_mul hn hp)) - (mul_le.2 fun m hm _np hnp => - suffices N * P ≤ (M * N * P).comap (AddMonoidHom.mulLeft m) from this hnp - mul_le.2 fun n hn p hp => - show m * (n * p) ∈ M * N * P from mul_assoc m n p ▸ mul_mem_mul (mul_mem_mul hm hn) hp) + (mul_le.2 fun _mn hmn p hp => AddSubmonoid.mul_induction_on hmn + (fun m hm n hn ↦ mul_assoc m n p ▸ mul_mem_mul hm <| mul_mem_mul hn hp) + fun x y ↦ (add_mul x y p).symm ▸ add_mem) + (mul_le.2 fun m hm _np hnp => AddSubmonoid.mul_induction_on hnp + (fun n hn p hp ↦ mul_assoc m n p ▸ mul_mem_mul (mul_mem_mul hm hn) hp) + fun x y ↦ (mul_add m x y) ▸ add_mem) scoped[Pointwise] attribute [instance] AddSubmonoid.semigroup end NonUnitalSemiring @@ -616,39 +673,6 @@ theorem pow_subset_pow {s : AddSubmonoid R} {n : ℕ} : (↑s : Set R) ^ n ⊆ end Semiring -section SMul - -variable [AddMonoid R] [DistribSMul R A] - -/-- For `M : Submonoid R` and `N : AddSubmonoid A`, `M • N` is the additive submonoid -generated by all `m • n` where `m ∈ M` and `n ∈ N`. -/ -protected def smul : SMul (AddSubmonoid R) (AddSubmonoid A) where - smul M N := ⨆ s : M, N.map (DistribSMul.toAddMonoidHom A s.1) - -scoped[Pointwise] attribute [instance] AddSubmonoid.smul - -example {R} [Semiring R] : Mul.toSMul (AddSubmonoid R) = AddSubmonoid.smul := rfl - -variable {M M' : AddSubmonoid R} {N P : AddSubmonoid A} {m : R} {n : A} - -theorem smul_mem_smul (hm : m ∈ M) (hn : n ∈ N) : m • n ∈ M • N := - (le_iSup _ ⟨m, hm⟩ : _ ≤ M • N) ⟨n, hn, by rfl⟩ - -theorem smul_le : M • N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m • n ∈ P := - ⟨fun H _m hm _n hn => H <| smul_mem_smul hm hn, fun H => - iSup_le fun ⟨m, hm⟩ => map_le_iff_le_comap.2 fun n hn => H m hm n hn⟩ - -@[elab_as_elim] -protected theorem smul_induction_on {C : A → Prop} {a : A} (ha : a ∈ M • N) - (hm : ∀ m ∈ M, ∀ n ∈ N, C (m • n)) (hadd : ∀ x y, C x → C y → C (x + y)) : C a := - (@smul_le _ _ _ _ _ _ _ ⟨⟨setOf C, hadd _ _⟩, by - simpa only [smul_zero] using hm _ (zero_mem _) _ (zero_mem _)⟩).2 hm ha - -theorem smul_le_smul (h : M ≤ M') (hnp : N ≤ P) : M • N ≤ M' • P := - smul_le.2 fun _m hm _n hn => smul_mem_smul (h hm) (hnp hn) - -end SMul - end AddSubmonoid namespace Set.IsPWO diff --git a/Mathlib/Algebra/GroupWithZero/Action/Defs.lean b/Mathlib/Algebra/GroupWithZero/Action/Defs.lean index 77eac698ee0d5..f4420acfd2b38 100644 --- a/Mathlib/Algebra/GroupWithZero/Action/Defs.lean +++ b/Mathlib/Algebra/GroupWithZero/Action/Defs.lean @@ -169,7 +169,7 @@ abbrev DistribSMul.compFun (f : N → M) : DistribSMul N A := /-- Each element of the scalars defines an additive monoid homomorphism. -/ @[simps] def DistribSMul.toAddMonoidHom (x : M) : A →+ A := - { SMulZeroClass.toZeroHom A x with toFun := (· • ·) x, map_add' := smul_add x } + { SMulZeroClass.toZeroHom A x with toFun := (x • ·), map_add' := smul_add x } end DistribSMul diff --git a/Mathlib/Algebra/Module/Defs.lean b/Mathlib/Algebra/Module/Defs.lean index 059efa2c28483..394dd7a778e54 100644 --- a/Mathlib/Algebra/Module/Defs.lean +++ b/Mathlib/Algebra/Module/Defs.lean @@ -240,6 +240,9 @@ instance (priority := 910) Semiring.toModule [Semiring R] : Module R R where zero_smul := zero_mul smul_zero := mul_zero +instance [NonUnitalNonAssocSemiring R] : DistribSMul R R where + smul_add := left_distrib + /-- A ring homomorphism `f : R →+* M` defines a module structure by `r • x = f r * x`. -/ def RingHom.toModule [Semiring R] [Semiring S] (f : R →+* S) : Module R S := Module.compHom S f From b0ba705cf8a3bc6d008c950e0c1a6bcd91f2418f Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sun, 27 Oct 2024 00:23:16 +0000 Subject: [PATCH 13/23] golf Ideal/Operations using the SMul lemmas --- Mathlib/RingTheory/Ideal/Operations.lean | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index c664506cb50f8..56b657b799be3 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/Mathlib/RingTheory/Ideal/Operations.lean @@ -42,6 +42,8 @@ protected theorem _root_.Ideal.smul_eq_mul (I J : Ideal R) : I • J = I * J := variable {I J : Ideal R} {N P : Submodule R M} +theorem smul_toAddSubmonoid : (I • N).toAddSubmonoid = I.toAddSubmonoid • N.toAddSubmonoid := rfl + theorem smul_mem_smul {r} {n} (hr : r ∈ I) (hn : n ∈ N) : r • n ∈ I • N := AddSubmonoid.smul_mem_smul hr hn @@ -94,7 +96,7 @@ variable (I J N P) @[simp] theorem smul_bot : I • (⊥ : Submodule R M) = ⊥ := - le_bot_iff.mp <| smul_le.mpr <| by rintro _ _ _ rfl; rw [smul_zero]; exact zero_mem _ + toAddSubmonoid_injective <| AddSubmonoid.addSubmonoid_smul_bot _ @[simp] theorem bot_smul : (⊥ : Ideal R) • N = ⊥ := @@ -105,10 +107,8 @@ theorem top_smul : (⊤ : Ideal R) • N = N := le_antisymm smul_le_right fun r hri => one_smul R r ▸ smul_mem_smul mem_top hri theorem smul_sup : I • (N ⊔ P) = I • N ⊔ I • P := - le_antisymm (smul_le.mpr fun m hm np hnp ↦ by - obtain ⟨n, hn, p, hp, rfl⟩ := mem_sup.mp hnp - rw [smul_add]; exact add_mem_sup (smul_mem_smul hm hn) <| smul_mem_smul hm hp) - (sup_le (smul_mono_right _ le_sup_left) <| smul_mono_right _ le_sup_right) + toAddSubmonoid_injective <| by + simp only [smul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.addSubmonoid_smul_sup] theorem sup_smul : (I ⊔ J) • N = I • N ⊔ J • N := le_antisymm (smul_le.mpr fun mn hmn p hp ↦ by @@ -130,10 +130,8 @@ protected theorem smul_inf_le (M₁ M₂ : Submodule R M) : I • (M₁ ⊓ M₂) ≤ I • M₁ ⊓ I • M₂ := smul_inf_le _ _ _ theorem smul_iSup {ι : Sort*} {I : Ideal R} {t : ι → Submodule R M} : I • iSup t = ⨆ i, I • t i := - le_antisymm (smul_le.mpr fun t ht s hs ↦ iSup_induction _ (C := (t • · ∈ _)) hs - (fun i s hs ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs) (by simp_rw [smul_zero]; apply zero_mem) - fun _ _ ↦ by simp_rw [smul_add]; apply add_mem) <| - iSup_le fun i ↦ smul_mono_right _ (le_iSup _ i) + toAddSubmonoid_injective <| by + simp only [smul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.smul_iSup] @[deprecated smul_iInf_le (since := "2024-03-31")] protected theorem smul_iInf_le {ι : Sort*} {I : Ideal R} {t : ι → Submodule R M} : @@ -396,8 +394,8 @@ theorem mul_eq_bot [NoZeroDivisors R] : I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥ := instance [NoZeroDivisors R] : NoZeroDivisors (Ideal R) where eq_zero_or_eq_zero_of_mul_eq_zero := mul_eq_bot.1 -instance {R : Type*} [CommSemiring R] {S : Type*} [Semiring S] [Algebra R S] - [NoZeroSMulDivisors R S] {I : Ideal S} : NoZeroSMulDivisors R I := +instance {S A : Type*} [Semiring S] [SMul R S] [AddCommMonoid A] [Module R A] [Module S A] + [IsScalarTower R S A] [NoZeroSMulDivisors R A] {I : Submodule S A} : NoZeroSMulDivisors R I := Submodule.noZeroSMulDivisors (Submodule.restrictScalars R I) end Semiring From 62c1fa9c8c9adc25f2afc28818f9421045fc8bef Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sun, 27 Oct 2024 09:27:22 +0000 Subject: [PATCH 14/23] fix + minigolfs --- Mathlib/Algebra/Group/Submonoid/Pointwise.lean | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/Group/Submonoid/Pointwise.lean b/Mathlib/Algebra/Group/Submonoid/Pointwise.lean index 9f032c5d53880..fc97cb647e916 100644 --- a/Mathlib/Algebra/Group/Submonoid/Pointwise.lean +++ b/Mathlib/Algebra/Group/Submonoid/Pointwise.lean @@ -481,7 +481,7 @@ theorem smul_subset_smul : (↑M : Set R) • (↑N : Set A) ⊆ (↑(M • N) : theorem addSubmonoid_smul_sup : M • (N ⊔ P) = M • N ⊔ M • P := le_antisymm (smul_le.mpr fun m hm np hnp ↦ by - refine closure_induction (p := fun x _ ↦ _ • x ∈ _) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp) + refine closure_induction (p := (fun _ ↦ _ • · ∈ _)) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp) · rintro x (hx | hx) exacts [le_sup_left (a := M • N) (smul_mem_smul hm hx), le_sup_right (a := M • N) (smul_mem_smul hm hx)] @@ -493,9 +493,9 @@ variable {ι : Sort*} theorem smul_iSup (T : AddSubmonoid R) (S : ι → AddSubmonoid A) : (T • ⨆ i, S i) = ⨆ i, T • S i := le_antisymm (smul_le.mpr fun t ht s hs ↦ iSup_induction _ (C := (t • · ∈ _)) hs - (fun i s hs ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs) - (by simp_rw [smul_zero]; apply zero_mem) fun x y ↦ by simp_rw [smul_add]; apply add_mem) <| - iSup_le fun i ↦ smul_le_smul_right (le_iSup _ i) + (fun i s hs ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs) + (by simp_rw [smul_zero]; apply zero_mem) fun x y ↦ by simp_rw [smul_add]; apply add_mem) + (iSup_le fun i ↦ smul_le_smul_right <| le_iSup _ i) end SMul @@ -509,8 +509,6 @@ protected def mul : Mul (AddSubmonoid R) := ⟨fun M N => ⨆ s : M, N.map (AddMonoidHom.mul s.1)⟩ scoped[Pointwise] attribute [instance] AddSubmonoid.mul -example {R} [Semiring R] : Mul.toSMul (AddSubmonoid R) = AddSubmonoid.smul := rfl - theorem mul_mem_mul {M N : AddSubmonoid R} {m n : R} (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N := smul_mem_smul hm hn @@ -640,7 +638,7 @@ variable [NonUnitalSemiring R] /-- Semigroup structure on additive submonoids of a (possibly, non-unital) semiring. -/ protected def semigroup : Semigroup (AddSubmonoid R) where mul := (· * ·) - mul_assoc M N P := + mul_assoc _M _N _P := le_antisymm (mul_le.2 fun _mn hmn p hp => AddSubmonoid.mul_induction_on hmn (fun m hm n hn ↦ mul_assoc m n p ▸ mul_mem_mul hm <| mul_mem_mul hn hp) From 5e67fb1fbe23079af552ec47424d5adf3e8aa222 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sun, 27 Oct 2024 09:27:29 +0000 Subject: [PATCH 15/23] minigolfs --- Mathlib/Algebra/Algebra/Operations.lean | 9 ++++----- Mathlib/RingTheory/Ideal/Operations.lean | 7 ++----- 2 files changed, 6 insertions(+), 10 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean index fee60eadd7ee2..63c34d4941e2b 100644 --- a/Mathlib/Algebra/Algebra/Operations.lean +++ b/Mathlib/Algebra/Algebra/Operations.lean @@ -130,11 +130,10 @@ protected theorem mul_induction_on' {C : ∀ r, r ∈ M * N → Prop} (mem_mul_mem : ∀ m (hm : m ∈ M) n (hn : n ∈ N), C (m * n) (mul_mem_mul hm hn)) (add : ∀ x hx y hy, C x hx → C y hy → C (x + y) (add_mem hx hy)) {r : A} (hr : r ∈ M * N) : C r hr := by - refine Exists.elim ?_ fun (hr : r ∈ M * N) (hc : C r hr) => hc - exact - Submodule.mul_induction_on hr - (fun x hx y hy => ⟨_, mem_mul_mem _ hx _ hy⟩) - fun x y ⟨_, hx⟩ ⟨_, hy⟩ => ⟨_, add _ _ _ _ hx hy⟩ + refine Exists.elim ?_ fun (hr : r ∈ M * N) (hc : C r hr) ↦ hc + exact Submodule.mul_induction_on hr + (fun x hx y hy ↦ ⟨_, mem_mul_mem _ hx _ hy⟩) + fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩ variable (M) diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index 56b657b799be3..877f076858b22 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/Mathlib/RingTheory/Ideal/Operations.lean @@ -895,12 +895,10 @@ theorem radical_bot_of_noZeroDivisors {R : Type u} [CommSemiring R] [NoZeroDivis instance : IdemCommSemiring (Ideal R) := inferInstance -variable (R) - +variable (R) in theorem top_pow (n : ℕ) : (⊤ ^ n : Ideal R) = ⊤ := Nat.recOn n one_eq_top fun n ih => by rw [pow_succ, ih, top_mul] -variable {R} variable (I) lemma radical_pow : ∀ {n}, n ≠ 0 → radical (I ^ n) = radical I @@ -1250,8 +1248,7 @@ lemma span_smul_eq @[simp] theorem set_smul_top_eq_span (s : Set R) : s • ⊤ = Ideal.span s := - Eq.trans (span_smul_eq s ⊤).symm <| - Eq.trans (smul_eq_mul (Ideal R)) (Ideal.mul_top (.span s)) + (span_smul_eq s ⊤).symm.trans (Ideal.span s).mul_top end Submodule From fe39874d64b6329f958cdca82fd4de20ddd06117 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Sun, 27 Oct 2024 10:19:30 +0000 Subject: [PATCH 16/23] get rid of large-import --- Mathlib/LinearAlgebra/TensorProduct/Quotient.lean | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean index 5bf265cb6fa82..0e102c8c44cab 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean @@ -5,7 +5,7 @@ Authors: Antoine Chambert-Loir, Jujian Zhang -/ import Mathlib.RingTheory.Ideal.Operations -import Mathlib.LinearAlgebra.TensorProduct.RightExactness +import Mathlib.LinearAlgebra.TensorProduct.Basic import Mathlib.LinearAlgebra.Quotient import Mathlib.LinearAlgebra.Prod import Mathlib.RingTheory.Ideal.Quotient @@ -156,12 +156,11 @@ variable (M) in quotienting that module by the corresponding submodule. -/ noncomputable def quotTensorEquivQuotSMul (I : Ideal R) : ((R ⧸ I) ⊗[R] M) ≃ₗ[R] M ⧸ (I • (⊤ : Submodule R M)) := - (rTensor.equiv M (LinearMap.exact_subtype_mkQ I) I.mkQ_surjective).symm.trans <| - Submodule.Quotient.equiv _ _ (TensorProduct.lid R M) <| - Eq.trans (LinearMap.range_comp _ _).symm <| - Eq.trans ((Submodule.topEquiv.lTensor I).range_comp _).symm <| Eq.symm <| - (Submodule.smul_eq_map₂.trans <| map₂_eq_range_lift_comp_mapIncl _ _ _).trans <| - congrArg _ (TensorProduct.ext' (fun _ _ => rfl)) + quotientTensorEquiv M I ≪≫ₗ + (Submodule.Quotient.equiv _ _ (TensorProduct.lid R M) <| by + erw [← LinearMap.range_comp, ← (Submodule.topEquiv.lTensor I).range_comp, + Submodule.smul_eq_map₂, map₂_eq_range_lift_comp_mapIncl] + exact congr_arg _ (TensorProduct.ext' fun _ _ ↦ rfl)) variable (M) in /-- Right tensoring a module with a quotient of the ring is the same as From 9f9c59d42bac808124f6310d7643411cb7ed74aa Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 28 Oct 2024 06:51:19 -0400 Subject: [PATCH 17/23] reduce diff --- Mathlib/LinearAlgebra/TensorProduct/Quotient.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean index 0e102c8c44cab..f062d829070e5 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean @@ -59,12 +59,12 @@ noncomputable def quotientTensorQuotientEquiv (m : Submodule R M) (n : Submodule ext y simp only [LinearMap.compr₂_apply, LinearMap.flip_apply, mk_apply, Submodule.mkQ_apply, LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero] - exact Submodule.mem_sup_right ⟨y ⊗ₜ ⟨x, hx⟩, rfl⟩) fun x hx => by - ext y - simp only [LinearMap.coe_comp, Function.comp_apply, Submodule.mkQ_apply, - LinearMap.flip_apply, Submodule.liftQ_apply, LinearMap.compr₂_apply, mk_apply, - LinearMap.zero_comp, LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero] - exact Submodule.mem_sup_left ⟨⟨x, hx⟩ ⊗ₜ y, rfl⟩) + refine Submodule.mem_sup_right ⟨y ⊗ₜ ⟨x, hx⟩, rfl⟩) fun x hx => ?_ + ext y + simp only [LinearMap.coe_comp, Function.comp_apply, Submodule.mkQ_apply, LinearMap.flip_apply, + Submodule.liftQ_apply, LinearMap.compr₂_apply, mk_apply, LinearMap.zero_comp, + LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero] + exact Submodule.mem_sup_left ⟨⟨x, hx⟩ ⊗ₜ y, rfl⟩) (Submodule.liftQ _ (map (Submodule.mkQ _) (Submodule.mkQ _)) fun x hx => by rw [Submodule.mem_sup] at hx rcases hx with ⟨_, ⟨a, rfl⟩, _, ⟨b, rfl⟩, rfl⟩ From 97f5e9a7846dd4ad70694c66425f71a3bc816f13 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 28 Oct 2024 11:00:40 +0000 Subject: [PATCH 18/23] revert --- Mathlib/LinearAlgebra/TensorProduct/Quotient.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean index f062d829070e5..f45adcd29a065 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean @@ -59,7 +59,7 @@ noncomputable def quotientTensorQuotientEquiv (m : Submodule R M) (n : Submodule ext y simp only [LinearMap.compr₂_apply, LinearMap.flip_apply, mk_apply, Submodule.mkQ_apply, LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero] - refine Submodule.mem_sup_right ⟨y ⊗ₜ ⟨x, hx⟩, rfl⟩) fun x hx => ?_ + exact Submodule.mem_sup_right ⟨y ⊗ₜ ⟨x, hx⟩, rfl⟩) fun x hx => by ext y simp only [LinearMap.coe_comp, Function.comp_apply, Submodule.mkQ_apply, LinearMap.flip_apply, Submodule.liftQ_apply, LinearMap.compr₂_apply, mk_apply, LinearMap.zero_comp, From e5fd5d60e8c01b2ca87642525c65ab7a1c3e004f Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 30 Oct 2024 00:23:30 +0100 Subject: [PATCH 19/23] generalize to SMul (Submodule R A) (Submodule R M) --- Mathlib/Algebra/Algebra/Operations.lean | 178 ++++++++++++++++++----- Mathlib/RingTheory/Ideal/Operations.lean | 100 +------------ 2 files changed, 147 insertions(+), 131 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean index 63c34d4941e2b..68c18f0bec104 100644 --- a/Mathlib/Algebra/Algebra/Operations.lean +++ b/Mathlib/Algebra/Algebra/Operations.lean @@ -47,7 +47,7 @@ multiplication of submodules, division of submodules, submodule semiring -/ -universe uι u v +universe uι u v w open Algebra Set MulOpposite @@ -97,24 +97,146 @@ theorem one_le {P : Submodule R A} : (1 : Submodule R A) ≤ P ↔ (1 : A) ∈ P -- 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] +variable {M : Type*} [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] + +instance : SMul (Submodule R A) (Submodule R M) where + smul A' M' := + { __ := A'.toAddSubmonoid • M'.toAddSubmonoid + smul_mem' := fun r m hm ↦ AddSubmonoid.smul_induction_on hm + (fun a ha m hm ↦ by rw [← smul_assoc]; exact AddSubmonoid.smul_mem_smul (A'.smul_mem r ha) hm) + fun m₁ m₂ h₁ h₂ ↦ by rw [smul_add]; exact (A'.1 • M'.1).add_mem h₁ h₂ } + +section + +variable {I J : Submodule R A} {N P : Submodule R M} + +theorem smul_toAddSubmonoid : (I • N).toAddSubmonoid = I.toAddSubmonoid • N.toAddSubmonoid := rfl + +theorem smul_mem_smul {r} {n} (hr : r ∈ I) (hn : n ∈ N) : r • n ∈ I • N := + AddSubmonoid.smul_mem_smul hr hn + +theorem smul_le : I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P := + AddSubmonoid.smul_le + +@[simp, norm_cast] +lemma coe_set_smul : (I : Set A) • N = I • N := + set_smul_eq_of_le _ _ _ + (fun _ _ hr hx ↦ smul_mem_smul hr hx) + (smul_le.mpr fun _ hr _ hx ↦ mem_set_smul_of_mem_mem hr hx) + +@[elab_as_elim] +theorem smul_induction_on {p : M → Prop} {x} (H : x ∈ I • N) (smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n)) + (add : ∀ x y, p x → p y → p (x + y)) : p x := + AddSubmonoid.smul_induction_on H smul add + +/-- Dependent version of `Submodule.smul_induction_on`. -/ +@[elab_as_elim] +theorem smul_induction_on' {x : M} (hx : x ∈ I • N) {p : ∀ x, x ∈ I • N → Prop} + (smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) (smul_mem_smul hr hn)) + (add : ∀ x hx y hy, p x hx → p y hy → p (x + y) (add_mem ‹_› ‹_›)) : p x hx := by + refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H + exact smul_induction_on hx (fun a ha x hx ↦ ⟨_, smul _ ha _ hx⟩) + fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩ + +theorem smul_mono (hij : I ≤ J) (hnp : N ≤ P) : I • N ≤ J • P := + AddSubmonoid.smul_le_smul hij hnp + +theorem smul_mono_left (h : I ≤ J) : I • N ≤ J • N := + smul_mono h le_rfl + +instance : CovariantClass (Submodule R A) (Submodule R M) HSMul.hSMul LE.le := + ⟨fun _ _ => smul_mono le_rfl⟩ + +@[deprecated smul_mono_right (since := "2024-03-31")] +protected theorem smul_mono_right (h : N ≤ P) : I • N ≤ I • P := + _root_.smul_mono_right I h + +variable (I J N P) + +@[simp] +theorem smul_bot : I • (⊥ : Submodule R M) = ⊥ := + toAddSubmonoid_injective <| AddSubmonoid.addSubmonoid_smul_bot _ + +@[simp] +theorem bot_smul : (⊥ : Submodule R A) • N = ⊥ := + le_bot_iff.mp <| smul_le.mpr <| by rintro _ rfl _ _; rw [zero_smul]; exact zero_mem _ + +theorem smul_sup : I • (N ⊔ P) = I • N ⊔ I • P := + toAddSubmonoid_injective <| by + simp only [smul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.addSubmonoid_smul_sup] + +theorem sup_smul : (I ⊔ J) • N = I • N ⊔ J • N := + le_antisymm (smul_le.mpr fun mn hmn p hp ↦ by + obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn + rw [add_smul]; exact add_mem_sup (smul_mem_smul hm hp) <| smul_mem_smul hn hp) + (sup_le (smul_mono_left le_sup_left) <| smul_mono_left le_sup_right) + +protected theorem smul_assoc {B} [Semiring B] [Module R B] [Module A B] [Module B M] + [IsScalarTower R A B] [IsScalarTower R B M] [IsScalarTower A B M] + (I : Submodule R A) (J : Submodule R B) (N : Submodule R M) : + (I • J) • N = I • J • N := + le_antisymm + (smul_le.2 fun _ hrsij t htn ↦ smul_induction_on hrsij + (fun r hr s hs ↦ smul_assoc r s t ▸ smul_mem_smul hr (smul_mem_smul hs htn)) + fun x y ↦ (add_smul x y t).symm ▸ add_mem) + (smul_le.2 fun r hr _ hsn ↦ smul_induction_on hsn + (fun j hj n hn ↦ (smul_assoc r j n).symm ▸ smul_mem_smul (smul_mem_smul hr hj) hn) + fun m₁ m₂ ↦ (smul_add r m₁ m₂) ▸ add_mem) + +@[deprecated smul_inf_le (since := "2024-03-31")] +protected theorem smul_inf_le (M₁ M₂ : Submodule R M) : + I • (M₁ ⊓ M₂) ≤ I • M₁ ⊓ I • M₂ := smul_inf_le _ _ _ + +theorem smul_iSup {ι : Sort*} {I : Submodule R A} {t : ι → Submodule R M} : + I • (⨆ i, t i)= ⨆ i, I • t i := + toAddSubmonoid_injective <| by + simp only [smul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.smul_iSup] + +theorem iSup_smul {ι : Sort*} {t : ι → Submodule R A} {N : Submodule R M} : + (⨆ i, t i) • N = ⨆ i, t i • N := + le_antisymm (smul_le.mpr fun t ht s hs ↦ iSup_induction _ (C := (· • s ∈ _)) ht + (fun i t ht ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs) + (by simp_rw [zero_smul]; apply zero_mem) fun x y ↦ by simp_rw [add_smul]; apply add_mem) + (iSup_le fun i ↦ Submodule.smul_mono_left <| le_iSup _ i) + +@[deprecated smul_iInf_le (since := "2024-03-31")] +protected theorem smul_iInf_le {ι : Sort*} {I : Submodule R A} {t : ι → Submodule R M} : + I • iInf t ≤ ⨅ i, I • t i := + smul_iInf_le + +theorem mem_of_span_top_of_smul_mem (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (x : M) + (H : ∀ r : s, (r : R) • x ∈ M') : x ∈ M' := by + suffices LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M' by + rw [← LinearMap.toSpanSingleton_one R M x] + exact this (LinearMap.mem_range_self _ 1) + rw [LinearMap.range_eq_map, ← hs, map_le_iff_le_comap, Ideal.span, span_le] + exact fun r hr ↦ H ⟨r, hr⟩ + +protected theorem one_smul : (1 : Submodule R A) • N = N := by + refine le_antisymm (smul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_ + · obtain ⟨r, rfl⟩ := hr + rw [LinearMap.toSpanSingleton_apply, smul_one_smul]; exact N.smul_mem r hm + · rw [← one_smul A m]; exact smul_mem_smul (one_le.mp le_rfl) hm + +theorem smul_subset_smul : (↑I : Set A) • (↑N : Set M) ⊆ (↑(I • N) : Set M) := + AddSubmonoid.smul_subset_smul + +end + variable [IsScalarTower R A A] /-- Multiplication of sub-R-modules of an R-module A that is also a semiring. The submodule `M * N` consists of finite sums of elements `m * n` for `m ∈ M` and `n ∈ N`. -/ instance mul : Mul (Submodule R A) where - mul M N := - { __ := M.toAddSubmonoid * N.toAddSubmonoid - smul_mem' := fun r a ha ↦ AddSubmonoid.mul_induction_on ha - (fun m h n h' ↦ by rw [← smul_mul_assoc]; exact AddSubmonoid.mul_mem_mul (M.smul_mem r h) h') - fun a₁ a₂ h₁ h₂ ↦ by rw [smul_add]; apply (M.1 * N.1).add_mem h₁ h₂ } + mul := (· • ·) variable (S T : Set A) {M N P Q : Submodule R A} {m n : A} theorem mul_mem_mul (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N := - AddSubmonoid.mul_mem_mul hm hn + smul_mem_smul hm hn theorem mul_le : M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P := - AddSubmonoid.mul_le + smul_le theorem mul_toAddSubmonoid (M N : Submodule R A) : (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid := rfl @@ -122,59 +244,51 @@ theorem mul_toAddSubmonoid (M N : Submodule R A) : @[elab_as_elim] protected theorem mul_induction_on {C : A → Prop} {r : A} (hr : r ∈ M * N) (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)) (ha : ∀ x y, C x → C y → C (x + y)) : C r := - AddSubmonoid.mul_induction_on hr hm ha + smul_induction_on hr hm ha /-- A dependent version of `mul_induction_on`. -/ @[elab_as_elim] protected theorem mul_induction_on' {C : ∀ r, r ∈ M * N → Prop} (mem_mul_mem : ∀ m (hm : m ∈ M) n (hn : n ∈ N), C (m * n) (mul_mem_mul hm hn)) (add : ∀ x hx y hy, C x hx → C y hy → C (x + y) (add_mem hx hy)) {r : A} (hr : r ∈ M * N) : - C r hr := by - refine Exists.elim ?_ fun (hr : r ∈ M * N) (hc : C r hr) ↦ hc - exact Submodule.mul_induction_on hr - (fun x hx y hy ↦ ⟨_, mem_mul_mem _ hx _ hy⟩) - fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩ + C r hr := + smul_induction_on' hr mem_mul_mem add variable (M) @[simp] theorem mul_bot : M * ⊥ = ⊥ := - toAddSubmonoid_injective (AddSubmonoid.mul_bot _) + smul_bot _ @[simp] theorem bot_mul : ⊥ * M = ⊥ := - toAddSubmonoid_injective (AddSubmonoid.bot_mul _) + bot_smul _ -protected theorem one_mul : (1 : Submodule R A) * M = M := by - refine le_antisymm (mul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_ - · obtain ⟨r, rfl⟩ := hr - rw [LinearMap.toSpanSingleton_apply, smul_one_mul]; exact M.smul_mem r hm - · rw [← one_mul m]; exact mul_mem_mul (one_le.mp le_rfl) hm +protected theorem one_mul : (1 : Submodule R A) * M = M := + Submodule.one_smul _ variable {M} @[mono] theorem mul_le_mul (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q := - AddSubmonoid.mul_le_mul hmp hnq + smul_mono hmp hnq theorem mul_le_mul_left (h : M ≤ N) : M * P ≤ N * P := - AddSubmonoid.mul_le_mul_left h + smul_mono_left h theorem mul_le_mul_right (h : N ≤ P) : M * N ≤ M * P := - AddSubmonoid.mul_le_mul_right h + smul_mono_right _ h variable (M N P) theorem mul_sup : M * (N ⊔ P) = M * N ⊔ M * P := - toAddSubmonoid_injective <| by - simp only [mul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.mul_sup] + smul_sup _ _ _ theorem sup_mul : (M ⊔ N) * P = M * P ⊔ N * P := - toAddSubmonoid_injective <| by - simp only [mul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.sup_mul] + sup_smul _ _ _ theorem mul_subset_mul : (↑M : Set A) * (↑N : Set A) ⊆ (↑(M * N) : Set A) := - AddSubmonoid.mul_subset_mul + smul_subset_smul _ _ lemma restrictScalars_mul {A B C} [Semiring A] [Semiring B] [Semiring C] [SMul A B] [Module A C] [Module B C] [IsScalarTower A C C] [IsScalarTower B C C] @@ -185,12 +299,10 @@ lemma restrictScalars_mul {A B C} [Semiring A] [Semiring B] [Semiring C] variable {ι : Sort uι} theorem iSup_mul (s : ι → Submodule R A) (t : Submodule R A) : (⨆ i, s i) * t = ⨆ i, s i * t := - toAddSubmonoid_injective <| by - simp only [mul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.iSup_mul] + iSup_smul theorem mul_iSup (t : Submodule R A) (s : ι → Submodule R A) : (t * ⨆ i, s i) = ⨆ i, t * s i := - toAddSubmonoid_injective <| by - simp only [mul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.mul_iSup] + smul_iSup /-- Sub-`R`-modules of an `R`-module form an idempotent semiring. -/ instance : NonUnitalSemiring (Submodule R A) where diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index 877f076858b22..fc18ac14dc4c5 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/Mathlib/RingTheory/Ideal/Operations.lean @@ -28,124 +28,28 @@ section Semiring variable [Semiring R] [AddCommMonoid M] [Module R M] -instance : SMul (Ideal R) (Submodule R M) where - smul I N := - { __ := I.toAddSubmonoid • N.toAddSubmonoid - smul_mem' := fun r m hm ↦ AddSubmonoid.smul_induction_on hm - (fun m hm n ↦ by rw [smul_smul]; exact AddSubmonoid.smul_mem_smul <| I.smul_mem _ hm) - fun m₁ m₂ h₁ h₂ ↦ by rw [smul_add]; exact (I.1 • N.1).add_mem h₁ h₂ } - /-- This duplicates the global `smul_eq_mul`, but doesn't have to unfold anywhere near as much to apply. -/ protected theorem _root_.Ideal.smul_eq_mul (I J : Ideal R) : I • J = I * J := rfl -variable {I J : Ideal R} {N P : Submodule R M} - -theorem smul_toAddSubmonoid : (I • N).toAddSubmonoid = I.toAddSubmonoid • N.toAddSubmonoid := rfl - -theorem smul_mem_smul {r} {n} (hr : r ∈ I) (hn : n ∈ N) : r • n ∈ I • N := - AddSubmonoid.smul_mem_smul hr hn - -theorem smul_le : I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P := - AddSubmonoid.smul_le - -@[simp, norm_cast] -lemma coe_set_smul : (I : Set R) • N = I • N := - set_smul_eq_of_le _ _ _ - (fun _ _ hr hx ↦ smul_mem_smul hr hx) - (smul_le.mpr fun _ hr _ hx ↦ mem_set_smul_of_mem_mem hr hx) - -@[elab_as_elim] -theorem smul_induction_on {p : M → Prop} {x} (H : x ∈ I • N) (smul : ∀ r ∈ I, ∀ n ∈ N, p (r • n)) - (add : ∀ x y, p x → p y → p (x + y)) : p x := - AddSubmonoid.smul_induction_on H smul add - -/-- Dependent version of `Submodule.smul_induction_on`. -/ -@[elab_as_elim] -theorem smul_induction_on' {x : M} (hx : x ∈ I • N) {p : ∀ x, x ∈ I • N → Prop} - (smul : ∀ (r : R) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) (smul_mem_smul hr hn)) - (add : ∀ x hx y hy, p x hx → p y hy → p (x + y) (add_mem ‹_› ‹_›)) : p x hx := by - refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H - exact smul_induction_on hx (fun a ha x hx ↦ ⟨_, smul _ ha _ hx⟩) - fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩ +variable {I : Ideal R} {N : Submodule R M} theorem smul_le_right : I • N ≤ N := smul_le.2 fun r _ _ ↦ N.smul_mem r -theorem smul_mono (hij : I ≤ J) (hnp : N ≤ P) : I • N ≤ J • P := - AddSubmonoid.smul_le_smul hij hnp - -theorem smul_mono_left (h : I ≤ J) : I • N ≤ J • N := - smul_mono h le_rfl - -instance : CovariantClass (Ideal R) (Submodule R M) HSMul.hSMul LE.le := - ⟨fun _ _ => smul_mono le_rfl⟩ - -@[deprecated smul_mono_right (since := "2024-03-31")] -protected theorem smul_mono_right (h : N ≤ P) : I • N ≤ I • P := - _root_.smul_mono_right I h - theorem map_le_smul_top (I : Ideal R) (f : R →ₗ[R] M) : Submodule.map f I ≤ I • (⊤ : Submodule R M) := by rintro _ ⟨y, hy, rfl⟩ rw [← mul_one y, ← smul_eq_mul, f.map_smul] exact smul_mem_smul hy mem_top -variable (I J N P) - -@[simp] -theorem smul_bot : I • (⊥ : Submodule R M) = ⊥ := - toAddSubmonoid_injective <| AddSubmonoid.addSubmonoid_smul_bot _ - -@[simp] -theorem bot_smul : (⊥ : Ideal R) • N = ⊥ := - le_bot_iff.mp <| smul_le.mpr <| by rintro _ rfl _ _; rw [zero_smul]; exact zero_mem _ +variable (I N) @[simp] theorem top_smul : (⊤ : Ideal R) • N = N := le_antisymm smul_le_right fun r hri => one_smul R r ▸ smul_mem_smul mem_top hri -theorem smul_sup : I • (N ⊔ P) = I • N ⊔ I • P := - toAddSubmonoid_injective <| by - simp only [smul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.addSubmonoid_smul_sup] - -theorem sup_smul : (I ⊔ J) • N = I • N ⊔ J • N := - le_antisymm (smul_le.mpr fun mn hmn p hp ↦ by - obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn - rw [add_smul]; exact add_mem_sup (smul_mem_smul hm hp) <| smul_mem_smul hn hp) - (sup_le (smul_mono_left le_sup_left) <| smul_mono_left le_sup_right) - -protected theorem smul_assoc : (I • J) • N = I • J • N := - le_antisymm - (smul_le.2 fun _ hrsij t htn ↦ smul_induction_on hrsij - (fun r hr s hs ↦ smul_assoc r s t ▸ smul_mem_smul hr (smul_mem_smul hs htn)) - fun x y ↦ (add_smul x y t).symm ▸ add_mem) - (smul_le.2 fun r hr _ hsn ↦ smul_induction_on hsn - (fun j hj n hn ↦ (smul_assoc r j n).symm ▸ smul_mem_smul (smul_mem_smul hr hj) hn) - fun m₁ m₂ ↦ (smul_add r m₁ m₂) ▸ add_mem) - -@[deprecated smul_inf_le (since := "2024-03-31")] -protected theorem smul_inf_le (M₁ M₂ : Submodule R M) : - I • (M₁ ⊓ M₂) ≤ I • M₁ ⊓ I • M₂ := smul_inf_le _ _ _ - -theorem smul_iSup {ι : Sort*} {I : Ideal R} {t : ι → Submodule R M} : I • iSup t = ⨆ i, I • t i := - toAddSubmonoid_injective <| by - simp only [smul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.smul_iSup] - -@[deprecated smul_iInf_le (since := "2024-03-31")] -protected theorem smul_iInf_le {ι : Sort*} {I : Ideal R} {t : ι → Submodule R M} : - I • iInf t ≤ ⨅ i, I • t i := - smul_iInf_le - -theorem mem_of_span_top_of_smul_mem (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (x : M) - (H : ∀ r : s, (r : R) • x ∈ M') : x ∈ M' := by - suffices LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M' by - rw [← LinearMap.toSpanSingleton_one R M x] - exact this (LinearMap.mem_range_self _ 1) - rw [LinearMap.range_eq_map, ← hs, map_le_iff_le_comap, Ideal.span, span_le] - exact fun r hr ↦ H ⟨r, hr⟩ - variable {M' : Type w} [AddCommMonoid M'] [Module R M'] @[simp] From 46cd3766034f8c8ca9be78044b0a8e1cf3383e68 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 30 Oct 2024 01:04:29 +0100 Subject: [PATCH 20/23] fix --- Mathlib/RingTheory/Ideal/Cotangent.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index 77ace6699c812..73208774bf9c2 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -196,6 +196,7 @@ def mapCotangent (I₁ : Ideal A) (I₂ : Ideal B) (f : A →ₐ[R] B) (h : I₁ ((I₂ • ⊤ : Submodule B I₂).restrictScalars R) ?_ ?_ · exact f.toLinearMap.restrict (p := I₁.restrictScalars R) (q := I₂.restrictScalars R) h · intro x hx + rw [Submodule.restrictScalars_mem] at hx refine Submodule.smul_induction_on hx ?_ (fun _ _ ↦ add_mem) rintro a ha ⟨b, hb⟩ - simp only [SetLike.mk_smul_mk, smul_eq_mul, Submodule.mem_comap, Submodule.restrictScalars_mem] From 8cabc5f24a567ff0a1c48d0388ca06a968c03580 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 30 Oct 2024 01:13:03 +0100 Subject: [PATCH 21/23] fix --- Mathlib/RingTheory/Kaehler/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Kaehler/Basic.lean b/Mathlib/RingTheory/Kaehler/Basic.lean index 4029cd726541a..17a028c8f4d6c 100644 --- a/Mathlib/RingTheory/Kaehler/Basic.lean +++ b/Mathlib/RingTheory/Kaehler/Basic.lean @@ -259,7 +259,7 @@ def Derivation.liftKaehlerDifferential (D : Derivation R S M) : Ω[S⁄R] →ₗ · exact D.tensorProductTo.comp ((KaehlerDifferential.ideal R S).subtype.restrictScalars S) · intro x hx rw [LinearMap.mem_ker] - refine Submodule.smul_induction_on hx ?_ ?_ + refine Submodule.smul_induction_on ((Submodule.restrictScalars_mem _ _ _).mp hx) ?_ ?_ · rintro x hx y - rw [RingHom.mem_ker] at hx dsimp From 5f8fc87b5bbbfce2a3a8affd9441f1fa55f03d12 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 30 Oct 2024 04:43:39 -0400 Subject: [PATCH 22/23] minor --- Mathlib/Algebra/Algebra/Operations.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean index 68c18f0bec104..b974162ca59e6 100644 --- a/Mathlib/Algebra/Algebra/Operations.lean +++ b/Mathlib/Algebra/Algebra/Operations.lean @@ -47,7 +47,7 @@ multiplication of submodules, division of submodules, submodule semiring -/ -universe uι u v w +universe uι u v open Algebra Set MulOpposite From d3c5b98d02e9f6a73275f2288b493dc1e001270d Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Tue, 3 Dec 2024 16:26:33 +0000 Subject: [PATCH 23/23] move lemma --- Mathlib/Algebra/Algebra/Operations.lean | 8 -------- Mathlib/RingTheory/Ideal/Operations.lean | 8 ++++++++ 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean index 9dd904eb0ab4a..24dddc1deceec 100644 --- a/Mathlib/Algebra/Algebra/Operations.lean +++ b/Mathlib/Algebra/Algebra/Operations.lean @@ -200,14 +200,6 @@ protected theorem smul_iInf_le {ι : Sort*} {I : Submodule R A} {t : ι → Subm I • iInf t ≤ ⨅ i, I • t i := smul_iInf_le -theorem mem_of_span_top_of_smul_mem (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (x : M) - (H : ∀ r : s, (r : R) • x ∈ M') : x ∈ M' := by - suffices LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M' by - rw [← LinearMap.toSpanSingleton_one R M x] - exact this (LinearMap.mem_range_self _ 1) - rw [LinearMap.range_eq_map, ← hs, map_le_iff_le_comap, Ideal.span, span_le] - exact fun r hr ↦ H ⟨r, hr⟩ - protected theorem one_smul : (1 : Submodule R A) • N = N := by refine le_antisymm (smul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_ · obtain ⟨r, rfl⟩ := hr diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index 2cb35d043fbf8..cb663d99cc855 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/Mathlib/RingTheory/Ideal/Operations.lean @@ -78,6 +78,14 @@ variable (I N) theorem top_smul : (⊤ : Ideal R) • N = N := le_antisymm smul_le_right fun r hri => one_smul R r ▸ smul_mem_smul mem_top hri +theorem mem_of_span_top_of_smul_mem (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (x : M) + (H : ∀ r : s, (r : R) • x ∈ M') : x ∈ M' := by + suffices LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M' by + rw [← LinearMap.toSpanSingleton_one R M x] + exact this (LinearMap.mem_range_self _ 1) + rw [LinearMap.range_eq_map, ← hs, map_le_iff_le_comap, Ideal.span, span_le] + exact fun r hr ↦ H ⟨r, hr⟩ + variable {M' : Type w} [AddCommMonoid M'] [Module R M'] @[simp]