refactor(ring_theory/fractional_ideal): rename lemmas for dot notatio…

…n, 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

@@ -316,38 +316,31 @@ 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,
   { rw [mul_smul, smul_comm],
     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,15 +424,27 @@ 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)
   (hm : ∀ (i ∈ I) (j ∈ J), C (i * j))
   (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 :=