feat(ring_theory): Fractional ideals

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