From 018c7289bec1e67b69fa8b4ec13a9d6257e89f19 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 18 Feb 2022 18:09:38 +0000 Subject: [PATCH] refactor(ring_theory/fractional_ideal): rename lemmas for dot notation, add coe_pow (#12080) This replaces `fractional_ideal.fractional_mul` with `is_fractional.mul` and likewise for the other operations. The bundling was a distraction for the content of the lemmas anyway. --- src/ring_theory/fractional_ideal.lean | 94 ++++++++++++++------------- 1 file changed, 49 insertions(+), 45 deletions(-) diff --git a/src/ring_theory/fractional_ideal.lean b/src/ring_theory/fractional_ideal.lean index 922b2539647f4..17a4614a6a85b 100644 --- a/src/ring_theory/fractional_ideal.lean +++ b/src/ring_theory/fractional_ideal.lean @@ -316,13 +316,9 @@ lemma eq_zero_iff {I : fractional_ideal S P} : I = 0 ↔ (∀ x ∈ I, x = (0 : ⟨ (λ h x hx, by simpa [h, mem_zero_iff] using hx), (λ h, le_bot_iff.mp (λ x hx, (mem_zero_iff S).mpr (h x hx))) ⟩ -lemma fractional_sup (I J : fractional_ideal S P) : is_fractional S (I ⊔ J : submodule R P) := -begin - rcases I.is_fractional with ⟨aI, haI, hI⟩, - rcases J.is_fractional with ⟨aJ, haJ, hJ⟩, - use aI * aJ, - use S.mul_mem haI haJ, - intros b hb, +lemma _root_.is_fractional.sup {I J : submodule R P} : + is_fractional S I → is_fractional S J → is_fractional S (I ⊔ J) +| ⟨aI, haI, hI⟩ ⟨aJ, haJ, hJ⟩ := ⟨aI * aJ, S.mul_mem haI haJ, λ b hb, begin rcases mem_sup.mp hb with ⟨bI, hbI, bJ, hbJ, rfl⟩, rw smul_add, apply is_integer_add, @@ -330,24 +326,21 @@ begin exact is_integer_smul (hI bI hbI), }, { rw mul_smul, exact is_integer_smul (hJ bJ hbJ) } -end +end⟩ -lemma fractional_inf (I J : fractional_ideal S P) : is_fractional S (I ⊓ J : submodule R P) := -begin - rcases I.is_fractional with ⟨aI, haI, hI⟩, - use aI, - use haI, - intros b hb, +lemma _root_.is_fractional.inf_right {I : submodule R P} : + is_fractional S I → ∀ J, is_fractional S (I ⊓ J) +| ⟨aI, haI, hI⟩ J := ⟨aI, haI, λ b hb, begin rcases mem_inf.mp hb with ⟨hbI, hbJ⟩, exact hI b hbI -end +end⟩ -instance : has_inf (fractional_ideal S P) := ⟨λ I J, ⟨I ⊓ J, fractional_inf I J⟩⟩ +instance : has_inf (fractional_ideal S P) := ⟨λ I J, ⟨I ⊓ J, I.is_fractional.inf_right J⟩⟩ @[simp, norm_cast] lemma coe_inf (I J : fractional_ideal S P) : ↑(I ⊓ J) = (I ⊓ J : submodule R P) := rfl -instance : has_sup (fractional_ideal S P) := ⟨λ I J, ⟨I ⊔ J, fractional_sup I J⟩⟩ +instance : has_sup (fractional_ideal S P) := ⟨λ I J, ⟨I ⊔ J, I.is_fractional.sup J.is_fractional⟩⟩ @[norm_cast] lemma coe_sup (I J : fractional_ideal S P) : ↑(I ⊔ J) = (I ⊔ J : submodule R P) := rfl @@ -374,13 +367,9 @@ lemma coe_add (I J : fractional_ideal S P) : (↑(I + J) : submodule R P) = I + lemma coe_ideal_sup (I J : ideal R) : ↑(I ⊔ J) = (I + J : fractional_ideal S P) := coe_to_submodule_injective $ coe_submodule_sup _ _ _ -lemma fractional_mul (I J : fractional_ideal S P) : is_fractional S (I * J : submodule R P) := -begin - rcases I with ⟨I, aI, haI, hI⟩, - rcases J with ⟨J, aJ, haJ, hJ⟩, - use aI * aJ, - use S.mul_mem haI haJ, - intros b hb, +lemma _root_.is_fractional.mul {I J : submodule R P} : + is_fractional S I → is_fractional S J → is_fractional S (I * J : submodule R P) +| ⟨aI, haI, hI⟩ ⟨aJ, haJ, hJ⟩ := ⟨aI * aJ, S.mul_mem haI haJ, λ b hb, begin apply submodule.mul_induction_on hb, { intros m hm n hn, obtain ⟨n', hn'⟩ := hJ n hn, @@ -390,7 +379,12 @@ begin { intros x y hx hy, rw smul_add, apply is_integer_add hx hy }, -end +end⟩ + +lemma _root_.is_fractional.pow {I : submodule R P} (h : is_fractional S I) : + ∀ n : ℕ, is_fractional S (I ^ n : submodule R P) +| 0 := is_fractional_of_le_one _ (pow_zero _).le +| (n + 1) := (pow_succ I n).symm ▸ h.mul (_root_.is_fractional.pow n) /-- `fractional_ideal.mul` is the product of two fractional ideals, used to define the `has_mul` instance. @@ -402,7 +396,7 @@ so by making definitions irreducible, we hope to avoid deep unfolds. -/ @[irreducible] def mul (I J : fractional_ideal S P) : fractional_ideal S P := -⟨I * J, fractional_mul I J⟩ +⟨I * J, I.is_fractional.mul J.is_fractional⟩ local attribute [semireducible] mul @@ -430,6 +424,11 @@ lemma mul_le {I J K : fractional_ideal S P} : I * J ≤ K ↔ (∀ (i ∈ I) (j ∈ J), i * j ∈ K) := submodule.mul_le +instance : has_pow (fractional_ideal S P) ℕ := ⟨λ I n, ⟨I^n, I.is_fractional.pow n⟩⟩ + +@[simp, norm_cast] +lemma coe_pow (I : fractional_ideal S P) (n : ℕ) : ↑(I ^ n) = (I ^ n : submodule R P) := rfl + @[elab_as_eliminator] protected theorem mul_induction_on {I J : fractional_ideal S P} {C : P → Prop} {r : P} (hr : r ∈ I * J) @@ -437,8 +436,15 @@ submodule.mul_le (ha : ∀ x y, C x → C y → C (x + y)) : C r := submodule.mul_induction_on hr hm ha +-- There is no `function.injective.comm_semiring_pow` so we need to do this in three parts to keep +-- our custom power operator. instance : comm_semiring (fractional_ideal S P) := -function.injective.comm_semiring _ subtype.coe_injective coe_zero coe_one coe_add coe_mul +{ ..(function.injective.monoid_pow _ subtype.coe_injective + coe_one coe_mul coe_pow : monoid (fractional_ideal S P)), + ..(function.injective.comm_semigroup _ subtype.coe_injective + coe_mul : comm_semigroup (fractional_ideal S P)), + ..(function.injective.non_unital_non_assoc_semiring _ subtype.coe_injective + coe_zero coe_add coe_mul : non_unital_non_assoc_semiring (fractional_ideal S P)) } section order @@ -519,22 +525,19 @@ end order variables {P' : Type*} [comm_ring P'] [algebra R P'] [loc' : is_localization S P'] variables {P'' : Type*} [comm_ring P''] [algebra R P''] [loc'' : is_localization S P''] -lemma fractional_map (g : P →ₐ[R] P') (I : fractional_ideal S P) : - is_fractional S (submodule.map g.to_linear_map I) := -begin - rcases I with ⟨I, a, a_nonzero, hI⟩, - use [a, a_nonzero], - intros b hb, +lemma _root_.is_fractional.map (g : P →ₐ[R] P') {I : submodule R P} : + is_fractional S I → is_fractional S (submodule.map g.to_linear_map I) +| ⟨a, a_nonzero, hI⟩ := ⟨a, a_nonzero, λ b hb, begin obtain ⟨b', b'_mem, hb'⟩ := submodule.mem_map.mp hb, obtain ⟨x, hx⟩ := hI b' b'_mem, use x, erw [←g.commutes, hx, g.map_smul, hb'] -end +end⟩ /-- `I.map g` is the pushforward of the fractional ideal `I` along the algebra morphism `g` -/ def map (g : P →ₐ[R] P') : fractional_ideal S P → fractional_ideal S P' := -λ I, ⟨submodule.map g.to_linear_map I, fractional_map g I⟩ +λ I, ⟨submodule.map g.to_linear_map I, I.is_fractional.map g⟩ @[simp, norm_cast] lemma coe_map (g : P →ₐ[R] P') (I : fractional_ideal S P) : ↑(map g I) = submodule.map g.to_linear_map I := rfl @@ -803,11 +806,9 @@ variables [is_domain R₁] include frac -lemma fractional_div_of_nonzero {I J : fractional_ideal R₁⁰ K} (h : J ≠ 0) : - is_fractional R₁⁰ (I / J : submodule R₁ K) := -begin - rcases I with ⟨I, aI, haI, hI⟩, - rcases J with ⟨J, aJ, haJ, hJ⟩, +lemma _root_.is_fractional.div_of_nonzero {I J : submodule R₁ K} : + is_fractional R₁⁰ I → is_fractional R₁⁰ J → J ≠ 0 → is_fractional R₁⁰ (I / J) +| ⟨aI, haI, hI⟩ ⟨aJ, haJ, hJ⟩ h := begin obtain ⟨y, mem_J, not_mem_zero⟩ := set_like.exists_of_lt (by simpa only using bot_lt_iff_ne_bot.mpr h), obtain ⟨y', hy'⟩ := hJ y mem_J, @@ -820,12 +821,18 @@ begin have y_zero := (mul_eq_zero.mp this).resolve_left (mt ((algebra_map R₁ K).injective_iff.1 (is_fraction_ring.injective _ _) _) (mem_non_zero_divisors_iff_ne_zero.mp haJ)), - exact not_mem_zero ((mem_zero_iff R₁⁰).mpr y_zero) }, + apply not_mem_zero, + simpa only using (mem_zero_iff R₁⁰).mpr y_zero, }, intros b hb, convert hI _ (hb _ (submodule.smul_mem _ aJ mem_J)) using 1, rw [← hy', mul_comm b, ← algebra.smul_def, mul_smul] end +lemma fractional_div_of_nonzero {I J : fractional_ideal R₁⁰ K} (h : J ≠ 0) : + is_fractional R₁⁰ (I / J : submodule R₁ K) := +I.is_fractional.div_of_nonzero J.is_fractional $ λ H, h $ + coe_to_submodule_injective $ H.trans coe_zero.symm + noncomputable instance fractional_ideal_has_div : has_div (fractional_ideal R₁⁰ K) := ⟨ λ I J, if h : J = 0 then 0 else ⟨I / J, fractional_div_of_nonzero h⟩ ⟩ @@ -842,10 +849,7 @@ dif_neg h @[simp] lemma coe_div {I J : fractional_ideal R₁⁰ K} (hJ : J ≠ 0) : (↑(I / J) : submodule R₁ K) = ↑I / (↑J : submodule R₁ K) := -begin - unfold has_div.div, - simp only [dif_neg hJ, coe_mk, val_eq_coe], -end +congr_arg _ (dif_neg hJ) lemma mem_div_iff_of_nonzero {I J : fractional_ideal R₁⁰ K} (h : J ≠ 0) {x} : x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I :=