feat(group_theory/*/pointwise): Copy set lemmas about pointwise actio…

…ns to subgroups and submonoids (#9359)

This is pretty much just a copy-and-paste job. At least the proofs themselves don't need copying. The set lemmas being copied here are:

https://github.com/leanprover-community/mathlib/blob/a9cd8c259d59b0bdbe931a6f8e6084f800bd7162/src/algebra/pointwise.lean#L607-L680

I skipped the `preimage_smul` lemma for now because I couldn't think of a useful statement using `map`.

src/group_theory/subgroup/pointwise.lean

@@ -6,7 +6,7 @@ Authors: Eric Wieser
 import group_theory.subgroup.basic
 import group_theory.submonoid.pointwise
 
-/-! # Pointwise instances on `subgroup`s
+/-! # Pointwise instances on `subgroup` and `add_subgroup`s
 
 This file provides the actions
 
@@ -16,12 +16,18 @@ This file provides the actions
 which matches the action of `mul_action_set`.
 
 These actions are available in the `pointwise` locale.
+
+## Implementation notes
+
+This file is almost identical to `group_theory/submonoid/pointwise.lean`. Where possible, try to
+keep them in sync.
 -/
 
 variables {α : Type*} {G : Type*} {A : Type*} [group G] [add_group A]
 
 namespace subgroup
 
+section monoid
 variables [monoid α] [mul_distrib_mul_action α G]
 
 /-- The action on a subgroup corresponding to applying the action to every element.
@@ -44,13 +50,73 @@ open_locale pointwise
 lemma smul_mem_pointwise_smul (m : G) (a : α) (S : subgroup G) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set G))
 
+end monoid
+
+section group
+variables [group α] [mul_distrib_mul_action α G]
+
+open_locale pointwise
+
+@[simp] lemma smul_mem_pointwise_smul_iff {a : α} {S : subgroup G} {x : G} :
+  a • x ∈ a • S ↔ x ∈ S :=
+smul_mem_smul_set_iff
+
+lemma mem_pointwise_smul_iff_inv_smul_mem {a : α} {S : subgroup G} {x : G} :
+  x ∈ a • S ↔ a⁻¹ • x ∈ S :=
+mem_smul_set_iff_inv_smul_mem
+
+lemma mem_inv_pointwise_smul_iff {a : α} {S : subgroup G} {x : G} : x ∈ a⁻¹ • S ↔ a • x ∈ S :=
+mem_inv_smul_set_iff
+
+@[simp] lemma pointwise_smul_le_pointwise_smul_iff {a : α} {S T : subgroup G} :
+  a • S ≤ a • T ↔ S ≤ T :=
+set_smul_subset_set_smul_iff
+
+lemma pointwise_smul_subset_iff {a : α} {S T : subgroup G} : a • S ≤ T ↔ S ≤ a⁻¹ • T :=
+set_smul_subset_iff
+
+lemma subset_pointwise_smul_iff {a : α} {S T : subgroup G} : S ≤ a • T ↔ a⁻¹ • S ≤ T :=
+subset_set_smul_iff
+
+end group
+
+section group_with_zero
+variables [group_with_zero α] [mul_distrib_mul_action α G]
+
+open_locale pointwise
+
+@[simp] lemma smul_mem_pointwise_smul_iff' {a : α} (ha : a ≠ 0) (S : subgroup G)
+  (x : G) : a • x ∈ a • S ↔ x ∈ S :=
+smul_mem_smul_set_iff' ha (S : set G) x
+
+lemma mem_pointwise_smul_iff_inv_smul_mem' {a : α} (ha : a ≠ 0) (S : subgroup G) (x : G) :
+  x ∈ a • S ↔ a⁻¹ • x ∈ S :=
+mem_smul_set_iff_inv_smul_mem' ha (S : set G) x
+
+lemma mem_inv_pointwise_smul_iff' {a : α} (ha : a ≠ 0) (S : subgroup G) (x : G) :
+  x ∈ a⁻¹ • S ↔ a • x ∈ S :=
+mem_inv_smul_set_iff' ha (S : set G) x
+
+@[simp] lemma pointwise_smul_le_pointwise_smul_iff' {a : α} (ha : a ≠ 0) {S T : subgroup G} :
+  a • S ≤ a • T ↔ S ≤ T :=
+set_smul_subset_set_smul_iff' ha
+
+lemma pointwise_smul_le_iff' {a : α} (ha : a ≠ 0) {S T : subgroup G} : a • S ≤ T ↔ S ≤ a⁻¹ • T :=
+set_smul_subset_iff' ha
+
+lemma le_pointwise_smul_iff' {a : α} (ha : a ≠ 0) {S T : subgroup G} : S ≤ a • T ↔ a⁻¹ • S ≤ T :=
+subset_set_smul_iff' ha
+
+end group_with_zero
+
 end subgroup
 
 namespace add_subgroup
 
+section monoid
 variables [monoid α] [distrib_mul_action α A]
 
-/-- The action on a additive subgroup corresponding to applying the action to every element.
+/-- The action on an additive subgroup corresponding to applying the action to every element.
 
 This is available as an instance in the `pointwise` locale. -/
 protected def pointwise_mul_action : mul_action α (add_subgroup A) :=
@@ -70,4 +136,65 @@ open_locale pointwise
 lemma smul_mem_pointwise_smul (m : A) (a : α) (S : add_subgroup A) : m ∈ S → a • m ∈ a • S :=
 (set.smul_mem_smul_set : _ → _ ∈ a • (S : set A))
 
+end monoid
+
+section group
+variables [group α] [distrib_mul_action α A]
+
+open_locale pointwise
+
+@[simp] lemma smul_mem_pointwise_smul_iff {a : α} {S : add_subgroup A} {x : A} :
+  a • x ∈ a • S ↔ x ∈ S :=
+smul_mem_smul_set_iff
+
+lemma mem_pointwise_smul_iff_inv_smul_mem {a : α} {S : add_subgroup A} {x : A} :
+  x ∈ a • S ↔ a⁻¹ • x ∈ S :=
+mem_smul_set_iff_inv_smul_mem
+
+lemma mem_inv_pointwise_smul_iff {a : α} {S : add_subgroup A} {x : A} : x ∈ a⁻¹ • S ↔ a • x ∈ S :=
+mem_inv_smul_set_iff
+
+@[simp] lemma pointwise_smul_le_pointwise_smul_iff {a : α} {S T : add_subgroup A} :
+  a • S ≤ a • T ↔ S ≤ T :=
+set_smul_subset_set_smul_iff
+
+lemma pointwise_smul_le_iff {a : α} {S T : add_subgroup A} : a • S ≤ T ↔ S ≤ a⁻¹ • T :=
+set_smul_subset_iff
+
+lemma le_pointwise_smul_iff {a : α} {S T : add_subgroup A} : S ≤ a • T ↔ a⁻¹ • S ≤ T :=
+subset_set_smul_iff
+
+end group
+
+section group_with_zero
+variables [group_with_zero α] [distrib_mul_action α A]
+
+open_locale pointwise
+
+@[simp] lemma smul_mem_pointwise_smul_iff' {a : α} (ha : a ≠ 0) (S : add_subgroup A)
+  (x : A) : a • x ∈ a • S ↔ x ∈ S :=
+smul_mem_smul_set_iff' ha (S : set A) x
+
+lemma mem_pointwise_smul_iff_inv_smul_mem' {a : α} (ha : a ≠ 0) (S : add_subgroup A) (x : A) :
+  x ∈ a • S ↔ a⁻¹ • x ∈ S :=
+mem_smul_set_iff_inv_smul_mem' ha (S : set A) x
+
+lemma mem_inv_pointwise_smul_iff' {a : α} (ha : a ≠ 0) (S : add_subgroup A) (x : A) :
+  x ∈ a⁻¹ • S ↔ a • x ∈ S :=
+mem_inv_smul_set_iff' ha (S : set A) x
+
+@[simp] lemma pointwise_smul_le_pointwise_smul_iff' {a : α} (ha : a ≠ 0) {S T : add_subgroup A} :
+  a • S ≤ a • T ↔ S ≤ T :=
+set_smul_subset_set_smul_iff' ha
+
+lemma pointwise_smul_le_iff' {a : α} (ha : a ≠ 0) {S T : add_subgroup A} :
+  a • S ≤ T ↔ S ≤ a⁻¹ • T :=
+set_smul_subset_iff' ha
+
+lemma le_pointwise_smul_iff' {a : α} (ha : a ≠ 0) {S T : add_subgroup A} :
+  S ≤ a • T ↔ a⁻¹ • S ≤ T :=
+subset_set_smul_iff' ha
+
+end group_with_zero
+
 end add_subgroup

src/group_theory/submonoid/pointwise.lean

@@ -17,19 +17,26 @@ which matches the action of `mul_action_set`.
 
 These actions are available in the `pointwise` locale.
 
+## Implementation notes
+
+Most of the lemmas in this file are direct copies of lemmas from `algebra/pointwise.lean`.
+While the statements of these lemmas are defeq, we repeat them here due to them not being
+syntactically equal. Before adding new lemmas here, consider if they would also apply to the action
+on `set`s.
+
 -/
 
-section
-variables {M' : Type*} {α β : Type*}
+variables {α : Type*} {M : Type*} {A : Type*} [monoid M] [add_monoid A]
 
 namespace submonoid
 
-variables [monoid α] [monoid M'] [mul_distrib_mul_action α M']
+section monoid
+variables [monoid α] [mul_distrib_mul_action α M]
 
 /-- The action on a submonoid corresponding to applying the action to every element.
 
 This is available as an instance in the `pointwise` locale. -/
-protected def pointwise_mul_action : mul_action α (submonoid M') :=
+protected def pointwise_mul_action : mul_action α (submonoid M) :=
 { smul := λ a S, S.map (mul_distrib_mul_action.to_monoid_End _ _ a),
   one_smul := λ S, (congr_arg (λ f, S.map f) (monoid_hom.map_one _)).trans S.map_id,
   mul_smul := λ a₁ a₂ S,
@@ -38,21 +45,81 @@ protected def pointwise_mul_action : mul_action α (submonoid M') :=
 localized "attribute [instance] submonoid.pointwise_mul_action" in pointwise
 open_locale pointwise
 
-@[simp] lemma coe_pointwise_smul (a : α) (S : submonoid M') : ↑(a • S) = a • (S : set M') := rfl
+@[simp] lemma coe_pointwise_smul (a : α) (S : submonoid M) : ↑(a • S) = a • (S : set M) := rfl
+
+lemma smul_mem_pointwise_smul (m : M) (a : α) (S : submonoid M) : m ∈ S → a • m ∈ a • S :=
+(set.smul_mem_smul_set : _ → _ ∈ a • (S : set M))
+
+end monoid
+
+section group
+variables [group α] [mul_distrib_mul_action α M]
+
+open_locale pointwise
+
+@[simp] lemma smul_mem_pointwise_smul_iff {a : α} {S : submonoid M} {x : M} :
+  a • x ∈ a • S ↔ x ∈ S :=
+smul_mem_smul_set_iff
+
+lemma mem_pointwise_smul_iff_inv_smul_mem {a : α} {S : submonoid M} {x : M} :
+  x ∈ a • S ↔ a⁻¹ • x ∈ S :=
+mem_smul_set_iff_inv_smul_mem
+
+lemma mem_inv_pointwise_smul_iff {a : α} {S : submonoid M} {x : M} : x ∈ a⁻¹ • S ↔ a • x ∈ S :=
+mem_inv_smul_set_iff
+
+@[simp] lemma pointwise_smul_le_pointwise_smul_iff {a : α} {S T : submonoid M} :
+  a • S ≤ a • T ↔ S ≤ T :=
+set_smul_subset_set_smul_iff
+
+lemma pointwise_smul_subset_iff {a : α} {S T : submonoid M} : a • S ≤ T ↔ S ≤ a⁻¹ • T :=
+set_smul_subset_iff
+
+lemma subset_pointwise_smul_iff {a : α} {S T : submonoid M} : S ≤ a • T ↔ a⁻¹ • S ≤ T :=
+subset_set_smul_iff
+
+end group
+
+section group_with_zero
+variables [group_with_zero α] [mul_distrib_mul_action α M]
+
+open_locale pointwise
+
+@[simp] lemma smul_mem_pointwise_smul_iff' {a : α} (ha : a ≠ 0) (S : submonoid M)
+  (x : M) : a • x ∈ a • S ↔ x ∈ S :=
+smul_mem_smul_set_iff' ha (S : set M) x
+
+lemma mem_pointwise_smul_iff_inv_smul_mem' {a : α} (ha : a ≠ 0) (S : submonoid M) (x : M) :
+  x ∈ a • S ↔ a⁻¹ • x ∈ S :=
+mem_smul_set_iff_inv_smul_mem' ha (S : set M) x
+
+lemma mem_inv_pointwise_smul_iff' {a : α} (ha : a ≠ 0) (S : submonoid M) (x : M) :
+  x ∈ a⁻¹ • S ↔ a • x ∈ S :=
+mem_inv_smul_set_iff' ha (S : set M) x
+
+@[simp] lemma pointwise_smul_le_pointwise_smul_iff' {a : α} (ha : a ≠ 0) {S T : submonoid M} :
+  a • S ≤ a • T ↔ S ≤ T :=
+set_smul_subset_set_smul_iff' ha
+
+lemma pointwise_smul_le_iff' {a : α} (ha : a ≠ 0) {S T : submonoid M} : a • S ≤ T ↔ S ≤ a⁻¹ • T :=
+set_smul_subset_iff' ha
+
+lemma le_pointwise_smul_iff' {a : α} (ha : a ≠ 0) {S T : submonoid M} : S ≤ a • T ↔ a⁻¹ • S ≤ T :=
+subset_set_smul_iff' ha
 
-lemma smul_mem_pointwise_smul (m : M') (a : α) (S : submonoid M') : m ∈ S → a • m ∈ a • S :=
-(set.smul_mem_smul_set : _ → _ ∈ a • (S : set M'))
+end group_with_zero
 
 end submonoid
 
 namespace add_submonoid
 
-variables [monoid α] [add_monoid M'] [distrib_mul_action α M']
+section monoid
+variables [monoid α] [distrib_mul_action α A]
 
 /-- The action on an additive submonoid corresponding to applying the action to every element.
 
 This is available as an instance in the `pointwise` locale. -/
-protected def pointwise_mul_action : mul_action α (add_submonoid M') :=
+protected def pointwise_mul_action : mul_action α (add_submonoid A) :=
 { smul := λ a S, S.map (distrib_mul_action.to_add_monoid_End _ _ a),
   one_smul := λ S, (congr_arg (λ f, S.map f) (monoid_hom.map_one _)).trans S.map_id,
   mul_smul := λ a₁ a₂ S,
@@ -61,11 +128,70 @@ protected def pointwise_mul_action : mul_action α (add_submonoid M') :=
 localized "attribute [instance] add_submonoid.pointwise_mul_action" in pointwise
 open_locale pointwise
 
-@[simp] lemma coe_pointwise_smul (a : α) (S : add_submonoid M') : ↑(a • S) = a • (S : set M') := rfl
+@[simp] lemma coe_pointwise_smul (a : α) (S : add_submonoid A) : ↑(a • S) = a • (S : set A) := rfl
 
-lemma smul_mem_pointwise_smul (m : M') (a : α) (S : add_submonoid M') : m ∈ S → a • m ∈ a • S :=
-(set.smul_mem_smul_set : _ → _ ∈ a • (S : set M'))
+lemma smul_mem_pointwise_smul (m : A) (a : α) (S : add_submonoid A) : m ∈ S → a • m ∈ a • S :=
+(set.smul_mem_smul_set : _ → _ ∈ a • (S : set A))
 
-end add_submonoid
+end monoid
+
+section group
+variables [group α] [distrib_mul_action α A]
+
+open_locale pointwise
+
+@[simp] lemma smul_mem_pointwise_smul_iff {a : α} {S : add_submonoid A} {x : A} :
+  a • x ∈ a • S ↔ x ∈ S :=
+smul_mem_smul_set_iff
+
+lemma mem_pointwise_smul_iff_inv_smul_mem {a : α} {S : add_submonoid A} {x : A} :
+  x ∈ a • S ↔ a⁻¹ • x ∈ S :=
+mem_smul_set_iff_inv_smul_mem
+
+lemma mem_inv_pointwise_smul_iff {a : α} {S : add_submonoid A} {x : A} : x ∈ a⁻¹ • S ↔ a • x ∈ S :=
+mem_inv_smul_set_iff
+
+@[simp] lemma pointwise_smul_le_pointwise_smul_iff {a : α} {S T : add_submonoid A} :
+  a • S ≤ a • T ↔ S ≤ T :=
+set_smul_subset_set_smul_iff
+
+lemma pointwise_smul_le_iff {a : α} {S T : add_submonoid A} : a • S ≤ T ↔ S ≤ a⁻¹ • T :=
+set_smul_subset_iff
+
+lemma le_pointwise_smul_iff {a : α} {S T : add_submonoid A} : S ≤ a • T ↔ a⁻¹ • S ≤ T :=
+subset_set_smul_iff
+
+end group
 
-end
+section group_with_zero
+variables [group_with_zero α] [distrib_mul_action α A]
+
+open_locale pointwise
+
+@[simp] lemma smul_mem_pointwise_smul_iff' {a : α} (ha : a ≠ 0) (S : add_submonoid A)
+  (x : A) : a • x ∈ a • S ↔ x ∈ S :=
+smul_mem_smul_set_iff' ha (S : set A) x
+
+lemma mem_pointwise_smul_iff_inv_smul_mem' {a : α} (ha : a ≠ 0) (S : add_submonoid A) (x : A) :
+  x ∈ a • S ↔ a⁻¹ • x ∈ S :=
+mem_smul_set_iff_inv_smul_mem' ha (S : set A) x
+
+lemma mem_inv_pointwise_smul_iff' {a : α} (ha : a ≠ 0) (S : add_submonoid A) (x : A) :
+  x ∈ a⁻¹ • S ↔ a • x ∈ S :=
+mem_inv_smul_set_iff' ha (S : set A) x
+
+@[simp] lemma pointwise_smul_le_pointwise_smul_iff' {a : α} (ha : a ≠ 0) {S T : add_submonoid A} :
+  a • S ≤ a • T ↔ S ≤ T :=
+set_smul_subset_set_smul_iff' ha
+
+lemma pointwise_smul_le_iff' {a : α} (ha : a ≠ 0) {S T : add_submonoid A} :
+  a • S ≤ T ↔ S ≤ a⁻¹ • T :=
+set_smul_subset_iff' ha
+
+lemma le_pointwise_smul_iff' {a : α} (ha : a ≠ 0) {S T : add_submonoid A} :
+  S ≤ a • T ↔ a⁻¹ • S ≤ T :=
+subset_set_smul_iff' ha
+
+end group_with_zero
+
+end add_submonoid