feat(group_theory/sub{monoid,group}): pointwise actions on `add_sub{m…

…onoid,group}`s and `sub{monoid,group,module,semiring,ring,algebra}`s (#8945)

This adds the pointwise actions characterized by `↑(m • S) = (m • ↑S : set R)` on:
* `submonoid`
* `subgroup`
* `add_submonoid`
* `add_subgroup`
* `submodule` ([Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lost.20instance/near/249467913))
* `subsemiring`
* `subring`
* `subalgebra`

within the locale `pointwise` (which must be open to state the RHS of the characterization above anyway).

src/algebra/algebra/operations.lean

@@ -220,7 +220,7 @@ instance : semiring (submodule R A) :=
   mul_zero      := mul_bot,
   left_distrib  := mul_sup,
   right_distrib := sup_mul,
-  ..submodule.add_comm_monoid_submodule,
+  ..submodule.pointwise_add_comm_monoid,
   ..submodule.has_one,
   ..submodule.has_mul }
 

src/algebra/algebra/subalgebra.lean

@@ -30,8 +30,9 @@ add_decl_doc subalgebra.to_subsemiring
 
 namespace subalgebra
 
-variables {R' : Type u'} {R : Type u} {A : Type v} {B : Type w}
-variables [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B]
+variables {R' : Type u'} {R : Type u} {A : Type v} {B : Type w} {C : Type w}
+variables [comm_semiring R]
+variables [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [algebra R C]
 include R
 
 instance : set_like (subalgebra R A) A :=
@@ -320,6 +321,13 @@ lemma map_injective {S₁ S₂ : subalgebra R A} (f : A →ₐ[R] B)
   (hf : function.injective f) (ih : S₁.map f = S₂.map f) : S₁ = S₂ :=
 ext $ set.ext_iff.1 $ set.image_injective.2 hf $ set.ext $ set_like.ext_iff.mp ih
 
+@[simp] lemma map_id (S : subalgebra R A) : S.map (alg_hom.id R A) = S :=
+set_like.coe_injective $ set.image_id _
+
+lemma map_map (S : subalgebra R A) (g : B →ₐ[R] C) (f : A →ₐ[R] B) :
+  (S.map f).map g = S.map (g.comp f) :=
+set_like.coe_injective $ set.image_image _ _ _
+
 lemma mem_map {S : subalgebra R A} {f : A →ₐ[R] B} {y : B} :
   y ∈ map S f ↔ ∃ x ∈ S, f x = y :=
 subsemiring.mem_map
@@ -804,6 +812,39 @@ def under {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A]
 
 end actions
 
+section pointwise
+variables {R' : Type*} [semiring R'] [mul_semiring_action R' A] [smul_comm_class R' R A]
+
+/-- The action on a subalgebra 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 R' (subalgebra R A) :=
+{ smul := λ a S, S.map (mul_semiring_action.to_alg_hom _ _ a),
+  one_smul := λ S,
+    (congr_arg (λ f, S.map f) (alg_hom.ext $ by exact one_smul R')).trans S.map_id,
+  mul_smul := λ a₁ a₂ S,
+    (congr_arg (λ f, S.map f) (alg_hom.ext $ by exact mul_smul _ _)).trans (S.map_map _ _).symm }
+
+localized "attribute [instance] subalgebra.pointwise_mul_action" in pointwise
+open_locale pointwise
+
+@[simp] lemma coe_pointwise_smul (m : R') (S : subalgebra R A) : ↑(m • S) = m • (S : set A) := rfl
+
+@[simp] lemma pointwise_smul_to_subsemiring (m : R') (S : subalgebra R A) :
+  (m • S).to_subsemiring = m • S.to_subsemiring := rfl
+
+@[simp] lemma pointwise_smul_to_submodule (m : R') (S : subalgebra R A) :
+  (m • S).to_submodule = m • S.to_submodule := rfl
+
+@[simp] lemma pointwise_smul_to_subring {R' R A : Type*} [semiring R'] [comm_ring R] [ring A]
+  [mul_semiring_action R' A] [algebra R A] [smul_comm_class R' R A] (m : R') (S : subalgebra R A) :
+  (m • S).to_subring = m • S.to_subring := rfl
+
+lemma smul_mem_pointwise_smul (m : R') (r : A) (S : subalgebra R A) : r ∈ S → m • r ∈ m • S :=
+(set.smul_mem_smul_set : _ → _ ∈ m • (S : set A))
+
+end pointwise
+
 end subalgebra
 
 section nat

src/algebra/group_ring_action.lean

@@ -7,6 +7,7 @@ Authors: Kenny Lau
 import group_theory.group_action.group
 import data.equiv.ring
 import ring_theory.subring
+import algebra.pointwise
 
 /-!
 # Group action on rings
@@ -106,6 +107,65 @@ H.to_subsemiring.mul_semiring_action
 
 end
 
+section pointwise
+
+namespace subsemiring
+variables [mul_semiring_action M R]
+
+/-- The action on a subsemiring 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 M (subsemiring R) :=
+{ smul := λ a S, S.map (mul_semiring_action.to_ring_hom _ _ a),
+  one_smul := λ S,
+    (congr_arg (λ f, S.map f) (ring_hom.ext $ by exact one_smul M)).trans S.map_id,
+  mul_smul := λ a₁ a₂ S,
+    (congr_arg (λ f, S.map f) (ring_hom.ext $ by exact mul_smul _ _)).trans (S.map_map _ _).symm }
+
+localized "attribute [instance] subsemiring.pointwise_mul_action" in pointwise
+open_locale pointwise
+
+@[simp] lemma coe_pointwise_smul (m : M) (S : subsemiring R) : ↑(m • S) = m • (S : set R) := rfl
+
+@[simp] lemma pointwise_smul_to_add_submonoid (m : M) (S : subsemiring R) :
+  (m • S).to_add_submonoid = m • S.to_add_submonoid := rfl
+
+lemma smul_mem_pointwise_smul (m : M) (r : R) (S : subsemiring R) : r ∈ S → m • r ∈ m • S :=
+(set.smul_mem_smul_set : _ → _ ∈ m • (S : set R))
+
+end subsemiring
+
+namespace subring
+variables {R' : Type*} [ring R'] [mul_semiring_action M R']
+
+/-- The action on a subring 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 M (subring R') :=
+{ smul := λ a S, S.map (mul_semiring_action.to_ring_hom _ _ a),
+  one_smul := λ S,
+    (congr_arg (λ f, S.map f) (ring_hom.ext $ by exact one_smul M)).trans S.map_id,
+  mul_smul := λ a₁ a₂ S,
+    (congr_arg (λ f, S.map f) (ring_hom.ext $ by exact mul_smul _ _)).trans (S.map_map _ _).symm }
+
+localized "attribute [instance] subring.pointwise_mul_action" in pointwise
+open_locale pointwise
+
+@[simp] lemma coe_pointwise_smul (m : M) (S : subring R') : ↑(m • S) = m • (S : set R') := rfl
+
+@[simp] lemma pointwise_smul_to_add_subgroup (m : M) (S : subring R') :
+  (m • S).to_add_subgroup = m • S.to_add_subgroup := rfl
+
+@[simp] lemma pointwise_smul_to_subsemiring (m : M) (S : subring R') :
+  (m • S).to_subsemiring = m • S.to_subsemiring := rfl
+
+lemma smul_mem_pointwise_smul (m : M) (r : R') (S : subring R') : r ∈ S → m • r ∈ m • S :=
+(set.smul_mem_smul_set : _ → _ ∈ m • (S : set R'))
+
+end subring
+
+end pointwise
+
 section simp_lemmas
 
 variables {M G A R F}

src/group_theory/group_action/defs.lean

@@ -468,9 +468,14 @@ variable {A}
 @[simp] lemma mul_distrib_mul_action.to_monoid_hom_apply (r : M) (x : A) :
   mul_distrib_mul_action.to_monoid_hom A r x = r • x := rfl
 
-@[simp] lemma mul_distrib_mul_action.to_monoid_hom_one :
-  mul_distrib_mul_action.to_monoid_hom A (1:M) = monoid_hom.id _ :=
-by { ext, rw [mul_distrib_mul_action.to_monoid_hom_apply, one_smul, monoid_hom.id_apply] }
+variables (M A)
+
+/-- Each element of the monoid defines a monoid homomorphism. -/
+@[simps]
+def mul_distrib_mul_action.to_monoid_End : M →* monoid.End A :=
+{ to_fun := mul_distrib_mul_action.to_monoid_hom A,
+  map_one' := monoid_hom.ext $ one_smul M,
+  map_mul' := λ x y, monoid_hom.ext $ mul_smul x y }
 
 end
 

src/group_theory/subgroup.lean

@@ -2319,6 +2319,65 @@ end subgroup
 
 end actions
 
+/-! ### Pointwise instances on `subgroup`s -/
+
+section
+variables {α : Type*}
+
+namespace subgroup
+
+variables [monoid α] [mul_distrib_mul_action α G]
+
+/-- The action on a 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 α (subgroup G) :=
+{ 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,
+    (congr_arg (λ f, S.map f) (monoid_hom.map_mul _ _ _)).trans (S.map_map _ _).symm,}
+
+localized "attribute [instance] subgroup.pointwise_mul_action" in pointwise
+open_locale pointwise
+
+@[simp] lemma coe_pointwise_smul (a : α) (S : subgroup G) : ↑(a • S) = a • (S : set G) := rfl
+
+@[simp] lemma pointwise_smul_to_submonoid (a : α) (S : subgroup G) :
+  (a • S).to_submonoid = a • S.to_submonoid := rfl
+
+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 subgroup
+
+namespace add_subgroup
+
+variables [monoid α] [distrib_mul_action α A]
+
+/-- The action on a 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) :=
+{ 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,
+    (congr_arg (λ f, S.map f) (monoid_hom.map_mul _ _ _)).trans (S.map_map _ _).symm,}
+
+localized "attribute [instance] add_subgroup.pointwise_mul_action" in pointwise
+open_locale pointwise
+
+@[simp] lemma coe_pointwise_smul (a : α) (S : add_subgroup A) : ↑(a • S) = a • (S : set A) := rfl
+
+@[simp] lemma pointwise_smul_to_add_submonoid (a : α) (S : add_subgroup A) :
+  (a • S).to_add_submonoid = a • S.to_add_submonoid := rfl
+
+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 add_subgroup
+
+end
+
 /-! ### Saturated subgroups -/
 
 section saturated

src/group_theory/submonoid/operations.lean

@@ -9,6 +9,7 @@ import group_theory.submonoid.basic
 import data.equiv.mul_add
 import algebra.group.prod
 import algebra.group.inj_surj
+import algebra.pointwise
 
 /-!
 # Operations on `submonoid`s
@@ -828,6 +829,7 @@ def submonoid_equiv_map (e : M ≃* N) (S : submonoid M) : S ≃* S.map e.to_mon
 
 end mul_equiv
 
+section actions
 /-! ### Actions by `submonoid`s
 
 These instances tranfer the action by an element `m : M` of a monoid `M` written as `m • a` onto the
@@ -836,7 +838,6 @@ action by an element `s : S` of a submonoid `S : submonoid M` such that `s • a
 These instances work particularly well in conjunction with `monoid.to_mul_action`, enabling
 `s • m` as an alias for `↑s * m`.
 -/
-section actions
 
 namespace submonoid
 
@@ -885,4 +886,57 @@ instance [mul_action M' α] [has_faithful_scalar M' α] (S : submonoid M') :
 
 end submonoid
 
+/-! ### Pointwise instances on `submonoid`s and `add_submonoid`s -/
+
+section
+variables {M' : Type*} {α β : Type*}
+
+namespace submonoid
+
+variables [monoid α] [monoid M'] [mul_distrib_mul_action α M']
+
+/-- The action on a 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 α (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,
+    (congr_arg (λ f, S.map f) (monoid_hom.map_mul _ _ _)).trans (S.map_map _ _).symm,}
+
+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
+
+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 submonoid
+
+namespace add_submonoid
+
+variables [monoid α] [add_monoid M'] [distrib_mul_action α M']
+
+/-- The action on a 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') :=
+{ 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,
+    (congr_arg (λ f, S.map f) (monoid_hom.map_mul _ _ _)).trans (S.map_map _ _).symm,}
+
+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
+
+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'))
+
+end add_submonoid
+
+end
+
 end actions

src/linear_algebra/basic.lean

@@ -694,7 +694,7 @@ lemma subtype_comp_of_le (p q : submodule R M) (h : p ≤ q) :
 by { ext ⟨b, hb⟩, refl }
 
 
-instance add_comm_monoid_submodule : add_comm_monoid (submodule R M) :=
+instance pointwise_add_comm_monoid : add_comm_monoid (submodule R M) :=
 { add := (⊔),
   add_assoc := λ _ _ _, sup_assoc,
   zero := ⊥,
@@ -948,6 +948,65 @@ ext $ λ x, ⟨by rintro ⟨⟨_, h₁⟩, h₂, rfl⟩; exact ⟨h₁, h₂⟩,
 lemma eq_zero_of_bot_submodule : ∀(b : (⊥ : submodule R M)), b = 0
 | ⟨b', hb⟩ := subtype.eq $ show b' = 0, from (mem_bot R).1 hb
 
+
+section
+variables {α : Type*} [monoid α] [distrib_mul_action α M] [smul_comm_class α R M]
+
+/-- The action on a submodule corresponding to applying the action to every element.
+
+This is available as an instance in the `pointwise` locale. -/
+protected def pointwise_distrib_mul_action : distrib_mul_action α (submodule R M) :=
+{ smul := λ a S, S.map (distrib_mul_action.to_linear_map _ _ a),
+  one_smul := λ S,
+    (congr_arg (λ f, S.map f) (linear_map.ext $ by exact one_smul α)).trans S.map_id,
+  mul_smul := λ a₁ a₂ S,
+    (congr_arg (λ f, S.map f) (linear_map.ext $ by exact mul_smul _ _)).trans (S.map_comp _ _),
+  smul_zero := λ a, map_bot _,
+  smul_add := λ a S₁ S₂, map_sup _ _ _ }
+
+localized "attribute [instance] submodule.pointwise_distrib_mul_action" in pointwise
+open_locale pointwise
+
+@[simp] lemma coe_pointwise_smul (a : α) (S : submodule R M) : ↑(a • S) = a • (S : set M) := rfl
+
+@[simp] lemma pointwise_smul_to_add_submonoid (a : α) (S : submodule R M) :
+  (a • S).to_add_submonoid = a • S.to_add_submonoid := rfl
+
+@[simp] lemma pointwise_smul_to_add_subgroup {R M : Type*}
+  [ring R] [add_comm_group M] [distrib_mul_action α M] [module R M] [smul_comm_class α R M]
+  (a : α) (S : submodule R M) :
+  (a • S).to_add_subgroup = a • S.to_add_subgroup := rfl
+
+lemma smul_mem_pointwise_smul (m : M) (a : α) (S : submodule R M) : m ∈ S → a • m ∈ a • S :=
+(set.smul_mem_smul_set : _ → _ ∈ a • (S : set M))
+
+@[simp] lemma smul_le_self_of_tower {α : Type*}
+  [semiring α] [module α R] [module α M] [smul_comm_class α R M] [is_scalar_tower α R M]
+  (a : α) (S : submodule R M) : a • S ≤ S :=
+begin
+  rintro y ⟨x, hx, rfl⟩,
+  exact smul_of_tower_mem _ a hx,
+end
+
+end
+
+section
+variables {α : Type*} [semiring α] [module α M] [smul_comm_class α R M]
+/-- The action on a submodule corresponding to applying the action to every element.
+
+This is available as an instance in the `pointwise` locale.
+
+This is a stronger version of `submodule.pointwise_distrib_mul_action`. Note that `add_smul` does
+not hold so this cannot be stated as a `module`. -/
+protected def pointwise_mul_action_with_zero : mul_action_with_zero α (submodule R M) :=
+{ zero_smul := λ S,
+    (congr_arg (λ f, S.map f) (linear_map.ext $ by exact zero_smul α)).trans S.map_zero,
+  .. submodule.pointwise_distrib_mul_action }
+
+localized "attribute [instance] submodule.pointwise_mul_action_with_zero" in pointwise
+
+end
+
 section
 variables (R)