feat(group_theory/submonoid): add bundled submonoids and various lemmas (#1623)

* WIP -- removing  and everything is broken

* test

* test

* tidy

* fixed localization

* starting on coset

* WIP

* submonoid.lean now compiles but no to_additive stuff

* submonoid.lean compiles

* putting is_submonoid back

* docstrings

* terrible docstrings up to line 370

* finished docstrings

* more to_additive stuff

* WIP -- removing  and everything is broken

* test

* test

* tidy

* fixed localization

* starting on coset

* WIP

* submonoid.lean now compiles but no to_additive stuff

* submonoid.lean compiles

* putting is_submonoid back

* docstrings

* terrible docstrings up to line 370

* finished docstrings

* more to_additive stuff

* WIP quotient monoids

* quotient monoids WIP

* quotient_monoid w/o ideals.lean all compiles

* removing lemma

* adjunction

* some tidying

* remove pointless equiv

* completion compiles (very slowly)

* add lemma

* tidying

* more tidying

* mul -> smul oops

* might now compile

* tidied! I think

* fix

* breaking/adding stuff & switching branch

* add Inf relation

* removing sorrys

* nearly updated quotient_monoid

* updated quotient_monoid

* resurrecting computability

* tidied congruence.lean, added some docstrings

* extending setoids instead, WIP

* starting Galois insertion

* a few more bits of to_additive and docs

* no battery

* up to line 800

* congruence'll compile when data.setoid exists now

* more updates modulo existence of data.setoid

* rearranging stuff

* docstrings

* starting additive docstrings

* using newer additive docstring format in submonoid

* docstrings, tidying

* fixes and to_additive stuff, all WIP

* temporary congruence fixes

* slightly better approach to kernels, general chaos

* aahh

* more mess

* deleting doomed inductive congruence closure

* many fixes and better char pred isoms

* docstrings for group_theory.submonoid

* removing everything but bundled submonoids/lemmas

* removing things etc

* removing random empty folder

* tidy

* adding lemma back

* tidying

* responding to PR comments

* change 2 defs to lemmas

* @[simp] group_power.lean lemmas

* responding to commute.lean comments

* Remove unnecessary add_semiconj_by.eq

* Change prod.submonoid to submonoid.prod

* replacing a / at the end of docstring

Sorry - don't make commits on your phone when your laptop's playing up :/

* removing some not very useful to_additives

* fix pi_instances namespaces

* remove unnecessary prefix

* change extensionality to ext

not sure this is necessary because surely merging will change this automatically, but Travis told me to, and I really want it to compile, and I am not at my laptop

Author: 101damnations

src/algebra/commute.lean

@@ -31,7 +31,7 @@ rather than just `rw [hb.pow_left 5]`.
 Most of the proofs come from the properties of `semiconj_by`.
 -/
 
-/-- Two elements commute, if `a * b = b * a`. -/
+/-- Two elements commute iff `a * b = b * a`. -/
 def commute {S : Type*} [has_mul S] (a b : S) : Prop := semiconj_by a b b
 
 open_locale smul
@@ -225,12 +225,14 @@ section centralizer
 
 variables {S : Type*} [has_mul S]
 
-/-- Centralizer of an element `a : S` is the set of elements that commute with `a`. -/
+/-- Centralizer of an element `a : S` as the set of elements that commute with `a`; for `S` a
+    monoid, `submonoid.centralizer` is the centralizer as a submonoid. -/
 def centralizer (a : S) : set S := { x | commute a x }
 
 @[simp] theorem mem_centralizer {a b : S} : b ∈ centralizer a ↔ commute a b := iff.rfl
 
-/-- Centralizer of a set `T` is the set of elements that commute with all `a ∈ T`. -/
+/-- Centralizer of a set `T` as the set of elements of `S` that commute with all `a ∈ T`; for
+    `S` a monoid, `submonoid.set.centralizer` is the set centralizer as a submonoid. -/
 protected def set.centralizer (s : set S) : set S := { x | ∀ a ∈ s, commute a x }
 
 @[simp] protected theorem set.mem_centralizer (s : set S) {x : S} :
@@ -260,9 +262,22 @@ instance centralizer.is_submonoid : is_submonoid (centralizer a) :=
 { one_mem := commute.one_right a,
   mul_mem := λ _ _, commute.mul_right }
 
+/-- Centralizer of an element `a` of a monoid is the submonoid of elements that commute with `a`. -/
+def submonoid.centralizer : submonoid M :=
+{ carrier := centralizer a,
+  one_mem' := commute.one_right a,
+  mul_mem' := λ _ _, commute.mul_right }
+
 instance set.centralizer.is_submonoid : is_submonoid s.centralizer :=
 by rw s.centralizer_eq; apply_instance
 
+/-- Centralizer of a subset `T` of a monoid is the submonoid of elements that commute with
+    all `a ∈ T`. -/
+def submonoid.set.centralizer : submonoid M :=
+{ carrier := s.centralizer,
+  one_mem' := λ _ _, commute.one_right _,
+  mul_mem' := λ _ _ h1 h2 a h, commute.mul_right (h1 a h) $ h2 a h }
+
 @[simp] theorem monoid.centralizer_closure : (monoid.closure s).centralizer = s.centralizer :=
 set.subset.antisymm
   (set.centralizer_decreasing monoid.subset_closure)
@@ -310,9 +325,19 @@ instance centralizer.is_add_submonoid : is_add_submonoid (centralizer a) :=
 { zero_mem := commute.zero_right a,
   add_mem := λ _ _, commute.add_right }
 
+def centralizer.add_submonoid : add_submonoid A :=
+{ carrier := centralizer a,
+  zero_mem' := commute.zero_right a,
+  add_mem' := λ _ _, commute.add_right }
+
 instance set.centralizer.is_add_submonoid : is_add_submonoid s.centralizer :=
 by rw s.centralizer_eq; apply_instance
 
+def set.centralizer.add_submonoid : add_submonoid A :=
+{ carrier := s.centralizer,
+  zero_mem' := λ _ _, commute.zero_right _,
+  add_mem' := λ _ _ h1 h2 a h, commute.add_right (h1 a h) $ h2 a h }
+
 @[simp] lemma add_monoid.centralizer_closure : (add_monoid.closure s).centralizer = s.centralizer :=
 set.subset.antisymm
   (set.centralizer_decreasing add_monoid.subset_closure)

src/algebra/group/hom.lean

@@ -315,6 +315,13 @@ def comp (hnp : N →* P) (hmn : M →* N) : M →* P :=
   map_one' := by simp,
   map_mul' := by simp }
 
+@[simp, to_additive] lemma comp_apply (g : N →* P) (f : M →* N) (x : M) :
+  g.comp f x = g (f x) := rfl
+
+/-- Composition of monoid homomorphisms is associative. -/
+@[to_additive] lemma comp_assoc {Q : Type*} [monoid Q] (f : M →* N) (g : N →* P) (h : P →* Q) :
+  (h.comp g).comp f = h.comp (g.comp f) := rfl
+
 omit mP
 variables [mM] [mN]
 
@@ -360,6 +367,15 @@ eq_inv_of_mul_eq_one $ by rw [←f.map_mul, inv_mul_self, f.map_one]
 theorem map_mul_inv {G H} [group G] [group H] (f : G →* H) (g h : G) :
   f (g * h⁻¹) = (f g) * (f h)⁻¹ := by rw [f.map_mul, f.map_inv]
 
+/-- A group homomorphism is injective iff its kernel is trivial. -/
+@[to_additive]
+lemma injective_iff {G H} [group G] [group H] (f : G →* H) :
+  function.injective f ↔ (∀ a, f a = 1 → a = 1) :=
+⟨λ h _, by rw ← f.map_one; exact @h _ _,
+  λ h x y hxy, by rw [← inv_inv (f x), inv_eq_iff_mul_eq_one, ← f.map_inv,
+      ← f.map_mul] at hxy;
+    simpa using inv_eq_of_mul_eq_one (h _ hxy)⟩
+
 include mM
 /-- Makes a group homomomorphism from a proof that the map preserves multiplication. -/
 @[to_additive]

src/algebra/group/units.lean

@@ -85,6 +85,18 @@ instance [has_repr α] : has_repr (units α) := ⟨repr ∘ val⟩
 @[simp] theorem mul_right_inj (a : units α) {b c : α} : b * a = c * a ↔ b = c :=
 ⟨λ h, by simpa only [mul_inv_cancel_right] using congr_arg (* ↑(a⁻¹ : units α)) h, congr_arg _⟩
 
+theorem eq_mul_inv_iff_mul_eq {a b : α} : a = b * ↑c⁻¹ ↔ a * c = b :=
+⟨λ h, by rw [h, inv_mul_cancel_right], λ h, by rw [← h, mul_inv_cancel_right]⟩
+
+theorem eq_inv_mul_iff_mul_eq {a c : α} : a = ↑b⁻¹ * c ↔ ↑b * a = c :=
+⟨λ h, by rw [h, mul_inv_cancel_left], λ h, by rw [← h, inv_mul_cancel_left]⟩
+
+theorem inv_mul_eq_iff_eq_mul {b c : α} : ↑a⁻¹ * b = c ↔ b = a * c :=
+⟨λ h, by rw [← h, mul_inv_cancel_left], λ h, by rw [h, inv_mul_cancel_left]⟩
+
+theorem mul_inv_eq_iff_eq_mul {a c : α} : a * ↑b⁻¹ = c ↔ a = c * b :=
+⟨λ h, by rw [← h, inv_mul_cancel_right], λ h, by rw [h, mul_inv_cancel_right]⟩
+
 end units
 
 theorem nat.units_eq_one (u : units ℕ) : u = 1 :=

src/algebra/group_power.lean

@@ -124,6 +124,24 @@ theorem map_smul (a : α) : ∀(n : ℕ), f (n • a) = n • (f a)
 
 end is_add_monoid_hom
 
+namespace monoid_hom
+variables {β : Type v} [monoid α] [monoid β] (f : α →* β)
+
+@[simp] theorem map_pow (a : α) : ∀(n : ℕ), f (a ^ n) = (f a) ^ n
+| 0            := f.map_one
+| (nat.succ n) := by rw [pow_succ, f.map_mul, map_pow n]; refl
+
+end monoid_hom
+
+namespace add_monoid_hom
+variables {β : Type*} [add_monoid α] [add_monoid β] (f : α →+ β)
+
+@[simp] theorem map_smul (a : α) : ∀(n : ℕ), f (n • a) = n • (f a)
+| 0            := f.map_zero
+| (nat.succ n) := by rw [succ_smul, f.map_add, map_smul n]; refl
+
+end add_monoid_hom
+
 @[simp] theorem nat.pow_eq_pow (p q : ℕ) :
   @has_pow.pow _ _ monoid.has_pow p q = p ^ q :=
 by induction q with q ih; [refl, rw [nat.pow_succ, pow_succ, mul_comm, ih]]
@@ -340,6 +358,24 @@ theorem map_gsmul (a : α) (n : ℤ) : f (gsmul n a) = gsmul n (f a) :=
 
 end is_add_group_hom
 
+namespace monoid_hom
+variables {β : Type v} [group α] [group β] (f : α →* β)
+
+@[simp] theorem map_gpow (a : α) (n : ℤ) : f (a ^ n) = f a ^ n :=
+by cases n; [exact f.map_pow _ _,
+  exact (f.map_inv _).trans (congr_arg _ $ f.map_pow _ _)]
+
+end monoid_hom
+
+namespace add_monoid_hom
+variables {β : Type v} [add_group α] [add_group β] (f : α →+ β)
+
+@[simp] theorem map_gsmul (a : α) (n : ℤ) : f (gsmul n a) = gsmul n (f a) :=
+by cases n; [exact f.map_smul _ _,
+  exact (f.map_neg _).trans (congr_arg _ $ f.map_smul _ _)]
+
+end add_monoid_hom
+local infix ` •ℤ `:70 := gsmul
 open_locale smul
 
 section comm_monoid
@@ -406,6 +442,10 @@ theorem is_semiring_hom.map_pow {β} [semiring α] [semiring β]
 by induction n with n ih; [exact is_semiring_hom.map_one f,
   rw [pow_succ, pow_succ, is_semiring_hom.map_mul f, ih]]
 
+@[simp] lemma ring_hom.map_pow {β} [semiring α] [semiring β] (f : α →+* β) (a) :
+  ∀ n : ℕ, f (a ^ n) = (f a) ^ n :=
+monoid_hom.map_pow f.to_monoid_hom a
+
 theorem neg_one_pow_eq_or {R} [ring R] : ∀ n : ℕ, (-1 : R)^n = 1 ∨ (-1 : R)^n = -1
 | 0     := or.inl rfl
 | (n+1) := (neg_one_pow_eq_or n).swap.imp

src/algebra/pi_instances.lean

@@ -241,6 +241,16 @@ lemma fst.is_monoid_hom [monoid α] [monoid β] : is_monoid_hom (prod.fst : α 
 lemma snd.is_monoid_hom [monoid α] [monoid β] : is_monoid_hom (prod.snd : α × β → β) :=
 { map_mul := λ _ _, rfl, map_one := rfl }
 
+/-- Given monoids `α, β`, the natural projection homomorphism from `α × β` to `α`. -/
+@[to_additive prod.add_monoid_hom.fst "Given add_monoids `α, β`, the natural projection homomorphism from `α × β` to `α`."]
+def monoid_hom.fst [monoid α] [monoid β] : α × β →* α :=
+⟨λ x, x.1, rfl, λ _ _, prod.fst_mul⟩
+
+/-- Given monoids `α, β`, the natural projection homomorphism from `α × β` to `β`.-/
+@[to_additive prod.add_monoid_hom.snd "Given add_monoids `α, β`, the natural projection homomorphism from `α × β` to `β`."]
+def monoid_hom.snd [monoid α] [monoid β] : α × β →* β :=
+⟨λ x, x.2, rfl, λ _ _, prod.snd_mul⟩
+
 @[to_additive is_add_group_hom]
 lemma fst.is_group_hom [group α] [group β] : is_group_hom (prod.fst : α × β → α) :=
 { map_mul := λ _ _, rfl }
@@ -370,6 +380,18 @@ end substructures
 
 end prod
 
+namespace submonoid
+
+/-- Given submonoids `s, t` of monoids `α, β` respectively, `s × t` as a submonoid of `α × β`. -/
+@[to_additive prod "Given `add_submonoids` `s, t` of `add_monoids` `α, β` respectively, `s × t` as an `add_submonoid` of `α × β`."]
+def prod {α : Type*} {β : Type*} [monoid α] [monoid β] (s : submonoid α) (t : submonoid β) :
+  submonoid (α × β) :=
+{ carrier := (s : set α).prod t,
+  one_mem' := ⟨s.one_mem, t.one_mem⟩,
+  mul_mem' := λ _ _ h1 h2, ⟨s.mul_mem h1.1 h2.1, t.mul_mem h1.2 h2.2⟩ }
+
+end submonoid
+
 namespace finset
 
 @[to_additive prod_mk_sum]

src/algebra/ring.lean

@@ -396,6 +396,10 @@ def comp (hnp : β →+* γ) (hmn : α →+* β) : α →+* γ :=
   map_add' := λ x y, by simp,
   map_mul' := λ x y, by simp}
 
+/-- Composition of semiring homomorphisms is associative. -/
+lemma comp_assoc {δ} {rδ: semiring δ} (f : α →+* β) (g : β →+* γ) (h : γ →+* δ) :
+  (h.comp g).comp f = h.comp (g.comp f) := rfl
+
 @[simp] lemma coe_comp (hnp : β →+* γ) (hmn : α →+* β) : (hnp.comp hmn : α → γ) = hnp ∘ hmn := rfl
 
 @[simp] lemma comp_apply (hnp : β →+* γ) (hmn : α →+* β) (x : α) : (hnp.comp hmn : α → γ) x =
@@ -411,6 +415,10 @@ eq_neg_of_add_eq_zero $ by rw [←f.map_add, neg_add_self, f.map_zero]
 @[simp] theorem map_sub {α β} [ring α] [ring β] (f : α →+* β) (x y : α) :
   f (x - y) = (f x) - (f y) := by simp
 
+/-- A ring homomorphism is injective iff its kernel is trivial. -/
+theorem injective_iff {α β} [ring α] [ring β] (f : α →+* β) :
+  function.injective f ↔ (∀ a, f a = 0 → a = 0) :=
+add_monoid_hom.injective_iff f.to_add_monoid_hom
 include rα
 
 /-- Makes a ring homomorphism from a monoid homomorphism of rings which preserves addition. -/

src/data/equiv/algebra.lean

@@ -252,6 +252,11 @@ lemma map_mul (f : α ≃* β) :  ∀ x y : α, f (x * y) = f x * f y := f.map_m
 @[to_additive]
 instance (h : α ≃* β) : is_mul_hom h := ⟨h.map_mul⟩
 
+/-- Makes a multiplicative isomorphism from a bijection which preserves multiplication. -/
+@[to_additive]
+def mk' (f : α ≃ β) (h : ∀ x y, f (x * y) = f x * f y) : α ≃* β :=
+⟨f.1, f.2, f.3, f.4, h⟩
+
 /-- The identity map is a multiplicative isomorphism. -/
 @[refl, to_additive]
 def refl (α : Type*) [has_mul α] : α ≃* α :=
@@ -518,6 +523,12 @@ variables [semiring α] [semiring β]
 def to_ring_hom (e : α ≃+* β) : α →+* β :=
 { .. e.to_mul_equiv.to_monoid_hom, .. e.to_add_equiv.to_add_monoid_hom }
 
+/-- Reinterpret a ring equivalence as a monoid homomorphism. -/
+abbreviation to_monoid_hom (e : α ≃+* β) : α →* β := e.to_ring_hom.to_monoid_hom
+
+/-- Reinterpret a ring equivalence as an `add_monoid` homomorphism. -/
+abbreviation to_add_monoid_hom (e : α ≃+* β) : α →+ β := e.to_ring_hom.to_add_monoid_hom
+
 /-- Interpret an equivalence `f : α ≃ β` as a ring equivalence `α ≃+* β`. -/
 def of (e : α ≃ β) [is_semiring_hom e] : α ≃+* β :=
 { .. e, .. monoid_hom.of e, .. add_monoid_hom.of e }
@@ -536,6 +547,33 @@ equiv.symm_apply_apply (e.to_equiv)
 
 end semiring_hom
 
+end ring_equiv
+
+namespace mul_equiv
+
+/-- Gives an `is_semiring_hom` instance from a `mul_equiv` of semirings that preserves addition. -/
+protected lemma to_semiring_hom {R : Type*} {S : Type*} [semiring R] [semiring S]
+  (h : R ≃* S) (H : ∀ x y : R, h (x + y) = h x + h y) : is_semiring_hom h :=
+⟨add_equiv.map_zero $ add_equiv.mk' h.to_equiv H, h.map_one, H, h.5⟩
+
+/-- Gives a `ring_equiv` from a `mul_equiv` preserving addition.-/
+def to_ring_equiv {R : Type*} {S : Type*} [has_add R] [has_add S] [has_mul R] [has_mul S]
+  (h : R ≃* S) (H : ∀ x y : R, h (x + y) = h x + h y) : R ≃+* S :=
+{..h.to_equiv, ..h, ..add_equiv.mk' h.to_equiv H }
+
+end mul_equiv
+
+namespace add_equiv
+
+/-- Gives an `is_semiring_hom` instance from a `mul_equiv` of semirings that preserves addition. -/
+protected lemma to_semiring_hom {R : Type*} {S : Type*} [semiring R] [semiring S]
+  (h : R ≃+ S) (H : ∀ x y : R, h (x * y) = h x * h y) : is_semiring_hom h :=
+⟨h.map_zero, mul_equiv.map_one $ mul_equiv.mk' h.to_equiv H, h.5, H⟩
+
+end add_equiv
+
+namespace ring_equiv
+
 section ring_hom
 
 variables [ring α] [ring β]

src/group_theory/coset.lean

@@ -70,26 +70,26 @@ attribute [to_additive right_add_coset_zero] right_coset_one
 end coset_monoid
 
 section coset_submonoid
-open is_submonoid
-variables [monoid α] (s : set α) [is_submonoid s]
+open submonoid
+variables [monoid α] (s : submonoid α)
 
 @[to_additive mem_own_left_add_coset]
 lemma mem_own_left_coset (a : α) : a ∈ a *l s :=
 suffices a * 1 ∈ a *l s, by simpa,
 mem_left_coset a (one_mem s)
 
 @[to_additive mem_own_right_add_coset]
-lemma mem_own_right_coset (a : α) : a ∈ s *r a :=
-suffices 1 * a ∈ s *r a, by simpa,
+lemma mem_own_right_coset (a : α) : a ∈ (s : set α) *r a :=
+suffices 1 * a ∈ (s : set α) *r a, by simpa,
 mem_right_coset a (one_mem s)
 
 @[to_additive mem_left_add_coset_left_add_coset]
 lemma mem_left_coset_left_coset {a : α} (ha : a *l s = s) : a ∈ s :=
-by rw [←ha]; exact mem_own_left_coset s a
+by rw [←submonoid.mem_coe, ←ha]; exact mem_own_left_coset s a
 
 @[to_additive mem_right_add_coset_right_add_coset]
-lemma mem_right_coset_right_coset {a : α} (ha : s *r a = s) : a ∈ s :=
-by rw [←ha]; exact mem_own_right_coset s a
+lemma mem_right_coset_right_coset {a : α} (ha : (s : set α) *r a = s) : a ∈ s :=
+by rw [←submonoid.mem_coe, ←ha]; exact mem_own_right_coset s a
 
 end coset_submonoid
 
@@ -111,7 +111,7 @@ iff.intro
 end coset_group
 
 section coset_subgroup
-open is_submonoid
+open submonoid
 open is_subgroup
 variables [group α] (s : set α) [is_subgroup s]