feat(group_theory/submonoid/operations): add lemmas (#7219)

Some lemmas about the interaction between additive and multiplicative submonoids.

I provided the two version (from additive to multiplicative and the other way), I am not sure if `@[to_additive]` can automatize this.

src/group_theory/submonoid/operations.lean

@@ -93,13 +93,84 @@ def add_submonoid.of_submonoid {M : Type*} [add_zero_class M] (S : submonoid (mu
   zero_mem' := S.one_mem',
   add_mem' := S.mul_mem' }
 
+lemma submonoid.to_add_submonoid_coe {M : Type*} [mul_one_class M] (S : submonoid M) :
+  (S.to_add_submonoid : set (additive M)) = additive.to_mul ⁻¹' S :=
+rfl
+
+lemma add_submonoid.to_submonoid_coe {M : Type*} [add_zero_class M] (S : add_submonoid M) :
+  (S.to_submonoid : set (multiplicative M)) = multiplicative.to_add ⁻¹' S :=
+rfl
+
+lemma submonoid.of_add_submonoid_coe {M : Type*} [mul_one_class M]
+  (S : add_submonoid (additive M)) :
+  (submonoid.of_add_submonoid S : set M) = additive.of_mul ⁻¹' S :=
+rfl
+
+lemma add_submonoid.of_submonoid_coe {M : Type*} [add_zero_class M]
+  (S : submonoid (multiplicative M)) :
+  (add_submonoid.of_submonoid S : set M) = multiplicative.of_add ⁻¹' S :=
+rfl
+
 /-- Submonoids of monoid `M` are isomorphic to additive submonoids of `additive M`. -/
 def submonoid.add_submonoid_equiv (M : Type*) [mul_one_class M] :
-  submonoid M ≃ add_submonoid (additive M) :=
+  submonoid M ≃o add_submonoid (additive M) :=
 { to_fun := submonoid.to_add_submonoid,
   inv_fun := submonoid.of_add_submonoid,
   left_inv := λ x, by cases x; refl,
-  right_inv := λ x, by cases x; refl }
+  right_inv := λ x, by cases x; refl,
+  map_rel_iff' := λ a b, iff.rfl, }
+
+/-- Additive submonoids of an additive monoid `M` are isomorphic to
+multiplicative submonoids of `multiplicative M`. -/
+def add_submonoid.submonoid_equiv (M : Type*) [add_zero_class M] :
+  add_submonoid M ≃o submonoid (multiplicative M) :=
+{ to_fun := add_submonoid.to_submonoid,
+  inv_fun := add_submonoid.of_submonoid,
+  left_inv := λ x, by cases x; refl,
+  right_inv := λ x, by cases x; refl,
+  map_rel_iff' := λ a b, iff.rfl, }
+
+lemma submonoid.add_submonoid_equiv_coe (M : Type*) [add_zero_class M] :
+  ⇑(add_submonoid.submonoid_equiv M) = add_submonoid.to_submonoid := rfl
+
+lemma add_submonoid.submonoid_equiv_symm_coe (M : Type*) [add_zero_class M] :
+  ⇑(add_submonoid.submonoid_equiv M).symm = add_submonoid.of_submonoid := rfl
+
+lemma add_submonoid.submonoid_equiv_coe (M : Type*) [mul_one_class M] :
+  ⇑(submonoid.add_submonoid_equiv M) = submonoid.to_add_submonoid := rfl
+
+lemma submonoid.add_submonoid_equiv_symm_coe (M : Type*) [mul_one_class M] :
+  ⇑(submonoid.add_submonoid_equiv M).symm = submonoid.of_add_submonoid := rfl
+
+lemma submonoid.to_add_submonoid_mono {M : Type*} [mul_one_class M] :
+  monotone (submonoid.to_add_submonoid : submonoid M → add_submonoid (additive M)) :=
+λ a b hab, hab
+
+lemma add_submonoid.to_submonoid_mono {M : Type*} [add_zero_class M] :
+  monotone (add_submonoid.to_submonoid : add_submonoid M → submonoid (multiplicative M)) :=
+λ a b hab, hab
+
+lemma submonoid.of_add_submonoid_mono {M : Type*} [mul_one_class M] :
+  monotone (submonoid.of_add_submonoid : add_submonoid (additive M) → submonoid M) :=
+λ a b hab, hab
+
+lemma add_submonoid.of_submonoid_mono {M : Type*} [add_zero_class M] :
+  monotone (add_submonoid.of_submonoid : submonoid (multiplicative M) → add_submonoid M) :=
+λ a b hab, hab
+
+lemma submonoid.to_add_submonoid_closure {M : Type*} [monoid M] (S : set M) :
+  (submonoid.closure S).to_add_submonoid = add_submonoid.closure (additive.to_mul ⁻¹' S) :=
+le_antisymm
+  ((submonoid.add_submonoid_equiv M).to_galois_connection.l_le $
+    submonoid.closure_le.2 add_submonoid.subset_closure)
+  (add_submonoid.closure_le.2 submonoid.subset_closure)
+
+lemma add_submonoid.to_submonoid_closure {M : Type*} [add_monoid M] (S : set M) :
+  (add_submonoid.closure S).to_submonoid = submonoid.closure (multiplicative.to_add ⁻¹' S) :=
+le_antisymm
+  ((add_submonoid.submonoid_equiv M).to_galois_connection.l_le $
+    add_submonoid.closure_le.2 submonoid.subset_closure)
+  (submonoid.closure_le.2 add_submonoid.subset_closure)
 
 namespace submonoid