feat(ring_theory): Fractional ideals (#2062)

* Some WIP work on fractional ideals

* Fill in the `sorry`

* A lot of instances for fractional_ideal

* Show that an invertible fractional ideal `I` has inverse `1 : I`

* Cleanup and documentation

* Move `has_div submodule` to algebra_operations

* More cleanup and documentation

* Explain the `non_zero_divisors R` in the `quotient` section

* whitespace

Co-Authored-By: Scott Morrison <scott@tqft.net>

* `has_inv` instance for `fractional_ideal`

* `set.univ.image` -> `set.range`

* Fix: `mem_div_iff.mpr` should be `mem_div_iff.mp`
(but both reduce to reflexivity anyway)

* Add `mem_div_iff_smul_subset`

Since that is how the definition of `I / J` is traditionally done,
but it is not as convenient to work with, I didn't change the definition
but added a lemma stating the two are equivalent

* whitespace again

(it got broken because I merged changes incorrectly)

* Fix unused argument to `inv_nonzero`

Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/ring_theory/algebra_operations.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 
-Multiplication of submodules of an algebra.
+Multiplication and division of submodules of an algebra.
 -/
 
 import ring_theory.algebra algebra.pointwise
@@ -222,6 +222,35 @@ begin
     exact subset_span ⟨a, set.mem_singleton a, m, hm, rfl⟩ }
 end
 
+section quotient
+
+local attribute [instance] set.smul_set_action
+
+/-- The elements of `I / J` are the `x` such that `x • J ⊆ I`.
+
+In fact, we define `x ∈ I / J` to be `∀ y ∈ J, x * y ∈ I` (see `mem_div_iff_forall_mul_mem`),
+which is equivalent to `x • J ⊆ I` (see `mem_div_iff_smul_subset`), but nicer to use in proofs.
+
+This is the general form of the ideal quotient, traditionally written $I : J$.
+-/
+instance : has_div (submodule R A) :=
+⟨ λ I J, {
+  carrier := { x | ∀ y ∈ J, x * y ∈ I },
+  zero    := λ y hy, by { rw zero_mul, apply submodule.zero },
+  add     := λ a b ha hb y hy, by { rw add_mul, exact submodule.add _ (ha _ hy) (hb _ hy) },
+  smul    := λ r x hx y hy, by { rw algebra.smul_mul_assoc, exact submodule.smul _ _ (hx _ hy) } } ⟩
+
+lemma mem_div_iff_forall_mul_mem {x : A} {I J : submodule R A} :
+  x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I :=
+iff.refl _
+
+lemma mem_div_iff_smul_subset {x : A} {I J : submodule R A} : x ∈ I / J ↔ x • (J : set A) ⊆ I :=
+⟨ λ h y ⟨y', hy', y_eq_xy'⟩, by { rw y_eq_xy', apply h, assumption },
+  λ h y hy, h (set.smul_mem_smul_set _ hy)⟩
+
+lemma le_div_iff {I J K : submodule R A} : I ≤ J / K ↔ ∀ (x ∈ I) (z ∈ K), x * z ∈ J := iff.refl _
+end quotient
+
 end comm_ring
 
 end submodule