feat(ring_theory/congruence): add the complete_lattice instance

src/ring_theory/congruence.lean

@@ -29,10 +29,7 @@ Most of the time you likely want to use the `ideal.quotient` API that is built o
 ## TODO
 
 * Use this for `ring_quot` too.
-* Copy across more API from `con` and `add_con` in `group_theory/congruence.lean`, such as:
-  * The `complete_lattice` structure.
-  * The `con_gen_eq` lemma, stating that
-    `ring_con_gen r = Inf {s : ring_con M | ∀ x y, r x y → s x y}`.
+* Copy across more API from `con` and `add_con` in `group_theory/congruence.lean`
 -/
 
 /-- A congruence relation on a type with an addition and multiplication is an equivalence relation
@@ -89,6 +86,14 @@ protected lemma mul {w x y z} : c w x → c y z → c (w * y) (x * z) := c.mul'
 
 instance : inhabited (ring_con R) := ⟨ring_con_gen empty_relation⟩
 
+/-- The map sending a congruence relation to its underlying binary relation is injective. -/
+lemma ext' {c d : ring_con R} (H : c.r = d.r) : c = d :=
+by { rcases c with ⟨⟨⟩⟩, rcases d with ⟨⟨⟩⟩, cases H, congr, }
+
+/-- Extensionality rule for congruence relations. -/
+lemma ext {c d : ring_con R} (H : ∀ x y, c x y ↔ d x y) : c = d :=
+ext' $ by ext; apply H
+
 end basic
 
 section quotient
@@ -271,4 +276,167 @@ def mk' [non_assoc_semiring R] (c : ring_con R) : R →+* c.quotient :=
 
 end quotient
 
+/-! ### Lattice structure
+
+The API in this section is copied from `group_theory/congruence.lean`
+-/
+
+section lattice
+variables [has_add R] [has_mul R]
+
+/-- For congruence relations `c, d` on a type `M` with multiplication and addition, `c ≤ d` iff
+`∀ x y ∈ M`, `x` is related to `y` by `d` if `x` is related to `y` by `c`. -/
+instance : has_le (ring_con R) := ⟨λ c d, ∀ ⦃x y⦄, c x y → d x y⟩
+
+/-- Definition of `≤` for congruence relations. -/
+theorem le_def {c d : ring_con R} : c ≤ d ↔ ∀ {x y}, c x y → d x y := iff.rfl
+
+/-- The infimum of a set of congruence relations on a given type with multiplication and
+addition. -/
+instance : has_Inf (ring_con R) :=
+⟨λ S,
+  { r := λ x y, ∀ c : ring_con R, c ∈ S → c x y,
+    iseqv := ⟨λ x c hc, c.refl x, λ _ _ h c hc, c.symm $ h c hc,
+              λ _ _ _ h1 h2 c hc, c.trans (h1 c hc) $ h2 c hc⟩,
+    add' := λ _ _ _ _ h1 h2 c hc, c.add (h1 c hc) $ h2 c hc,
+    mul' := λ _ _ _ _ h1 h2 c hc, c.mul (h1 c hc) $ h2 c hc }⟩
+
+/-- The infimum of a set of congruence relations is the same as the infimum of the set's image
+    under the map to the underlying equivalence relation. -/
+lemma Inf_to_setoid (S : set (ring_con R)) : (Inf S).to_setoid = Inf (to_setoid '' S) :=
+setoid.ext' $ λ x y, ⟨λ h r ⟨c, hS, hr⟩, by rw ←hr; exact h c hS,
+  λ h c hS, h c.to_setoid ⟨c, hS, rfl⟩⟩
+
+/-- The infimum of a set of congruence relations is the same as the infimum of the set's image
+    under the map to the underlying binary relation. -/
+lemma Inf_def (S : set (ring_con R)) :
+  ⇑(Inf S) = Inf (@set.image (ring_con R) (R → R → Prop) coe_fn S) :=
+by { ext, simp only [Inf_image, infi_apply, infi_Prop_eq], refl }
+
+instance : partial_order (ring_con R) :=
+{ le := (≤),
+  lt := λ c d, c ≤ d ∧ ¬d ≤ c,
+  le_refl := λ c _ _, id,
+  le_trans := λ c1 c2 c3 h1 h2 x y h, h2 $ h1 h,
+  lt_iff_le_not_le := λ _ _, iff.rfl,
+  le_antisymm := λ c d hc hd, ext $ λ x y, ⟨λ h, hc h, λ h, hd h⟩ }
+
+/-- The complete lattice of congruence relations on a given type with multiplication and
+addition. -/
+instance : complete_lattice (ring_con R) :=
+{ inf := λ c d,
+  { to_setoid := (c.to_setoid ⊓ d.to_setoid),
+    mul' := λ _ _ _ _ h1 h2, ⟨c.mul h1.1 h2.1, d.mul h1.2 h2.2⟩,
+    add' := λ _ _ _ _ h1 h2, ⟨c.add h1.1 h2.1, d.add h1.2 h2.2⟩ },
+  inf_le_left := λ _ _ _ _ h, h.1,
+  inf_le_right := λ _ _ _ _ h, h.2,
+  le_inf := λ _ _ _ hb hc _ _ h, ⟨hb h, hc h⟩,
+  top := { mul' := λ _ _ _ _ _ _, trivial,
+           add' := λ _ _ _ _ _ _, trivial,
+           ..(⊤ : setoid R) },
+  le_top := λ _ _ _ h, trivial,
+  bot := { mul' := λ _ _ _ _, congr_arg2 _,
+           add' := λ _ _ _ _, congr_arg2 _,
+           ..(⊥ : setoid R) },
+  bot_le := λ c x y h, h ▸ c.refl x,
+  .. complete_lattice_of_Inf (ring_con R) $ assume s,
+    ⟨λ r hr x y h, (h : ∀ r ∈ s, (r : ring_con R) x y) r hr, λ r hr x y h r' hr', hr hr' h⟩ }
+
+/-- The infimum of two congruence relations equals the infimum of the underlying binary
+operations. -/
+lemma inf_def {c d : ring_con R} : (c ⊓ d).r = c.r ⊓ d.r := rfl
+
+/-- Definition of the infimum of two congruence relations. -/
+theorem inf_iff_and {c d : ring_con R} {x y} : (c ⊓ d) x y ↔ c x y ∧ d x y := iff.rfl
+
+/-- The inductively defined smallest congruence relation containing a binary relation `r` equals
+    the infimum of the set of congruence relations containing `r`. -/
+theorem ring_con_gen_eq (r : R → R → Prop) :
+  ring_con_gen r = Inf {s : ring_con R | ∀ x y, r x y → s x y} :=
+le_antisymm
+  (λ x y H, ring_con_gen.rel.rec_on H
+    (λ _ _ h _ hs, hs _ _ h)
+    (ring_con.refl _)
+    (λ _ _ _, ring_con.symm _)
+    (λ _ _ _ _ _, ring_con.trans _)
+    (λ w x y z _ _ h1 h2 c hc, c.add (h1 c hc) $ h2 c hc)
+    (λ w x y z _ _ h1 h2 c hc, c.mul (h1 c hc) $ h2 c hc))
+  (Inf_le (λ _ _, ring_con_gen.rel.of _ _))
+
+/-- The smallest congruence relation containing a binary relation `r` is contained in any
+    congruence relation containing `r`. -/
+theorem ring_con_gen_le {r : R → R → Prop} {c : ring_con R}
+  (h : ∀ x y, r x y → @setoid.r _ c.to_setoid x y) :
+  ring_con_gen r ≤ c :=
+by rw ring_con_gen_eq; exact Inf_le h
+
+/-- Given binary relations `r, s` with `r` contained in `s`, the smallest congruence relation
+    containing `s` contains the smallest congruence relation containing `r`. -/
+theorem ring_con_gen_mono {r s : R → R → Prop} (h : ∀ x y, r x y → s x y) :
+  ring_con_gen r ≤ ring_con_gen s :=
+ring_con_gen_le $ λ x y hr, ring_con_gen.rel.of _ _ $ h x y hr
+
+/-- Congruence relations equal the smallest congruence relation in which they are contained. -/
+lemma ring_con_gen_of_ring_con (c : ring_con R) : ring_con_gen c = c :=
+le_antisymm (by rw ring_con_gen_eq; exact Inf_le (λ _ _, id)) ring_con_gen.rel.of
+
+/-- The map sending a binary relation to the smallest congruence relation in which it is
+    contained is idempotent. -/
+lemma ring_con_gen_idem (r : R → R → Prop) :
+  ring_con_gen (ring_con_gen r) = ring_con_gen r :=
+ring_con_gen_of_ring_con _
+
+/-- The supremum of congruence relations `c, d` equals the smallest congruence relation containing
+    the binary relation '`x` is related to `y` by `c` or `d`'. -/
+lemma sup_eq_ring_con_gen (c d : ring_con R) :
+  c ⊔ d = ring_con_gen (λ x y, c x y ∨ d x y) :=
+begin
+  rw ring_con_gen_eq,
+  apply congr_arg Inf,
+  simp only [le_def, or_imp_distrib, ← forall_and_distrib]
+end
+
+/-- The supremum of two congruence relations equals the smallest congruence relation containing
+    the supremum of the underlying binary operations. -/
+lemma sup_def {c d : ring_con R} : c ⊔ d = ring_con_gen (c.r ⊔ d.r) :=
+by rw sup_eq_ring_con_gen; refl
+
+/-- The supremum of a set of congruence relations `S` equals the smallest congruence relation
+    containing the binary relation 'there exists `c ∈ S` such that `x` is related to `y` by
+    `c`'. -/
+lemma Sup_eq_ring_con_gen (S : set (ring_con R)) :
+  Sup S = ring_con_gen (λ x y, ∃ c : ring_con R, c ∈ S ∧ c x y) :=
+begin
+  rw ring_con_gen_eq,
+  apply congr_arg Inf,
+  ext,
+  exact ⟨λ h _ _ ⟨r, hr⟩, h hr.1 hr.2,
+         λ h r hS _ _ hr, h _ _ ⟨r, hS, hr⟩⟩,
+end
+
+/-- The supremum of a set of congruence relations is the same as the smallest congruence relation
+    containing the supremum of the set's image under the map to the underlying binary relation. -/
+lemma Sup_def {S : set (ring_con R)} :
+  Sup S = ring_con_gen (Sup (@set.image (ring_con R) (R → R → Prop) coe_fn S)) :=
+begin
+  rw [Sup_eq_ring_con_gen, Sup_image],
+  congr' with x y,
+  simp only [Sup_image, supr_apply, supr_Prop_eq, exists_prop, rel_eq_coe]
+end
+
+variables (R)
+
+/-- There is a Galois insertion of congruence relations on a type with multiplication and addition
+`R` into binary relations on `R`. -/
+protected def gi :
+  @galois_insertion (R → R → Prop) (ring_con R) _ _ ring_con_gen coe_fn :=
+{ choice := λ r h, ring_con_gen r,
+  gc := λ r c,
+    ⟨λ H _ _ h, H $ ring_con_gen.rel.of _ _ h,
+     λ H, ring_con_gen_of_ring_con c ▸ ring_con_gen_mono H⟩,
+  le_l_u := λ x, (ring_con_gen_of_ring_con x).symm ▸ le_refl x,
+  choice_eq := λ _ _, rfl }
+
+end lattice
+
 end ring_con