chore(algebra/module/submodule): missing is_central_scalar instance (#…

…10720)
leanprover-community · Dec 13, 2021 · 4b07949 · 4b07949
1 parent 41def6a
commit 4b07949
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/src/algebra/module/submodule.lean b/src/algebra/module/submodule.lean
@@ -161,6 +161,12 @@ instance [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M] :
 instance [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M] : is_scalar_tower S R p :=
 p.to_sub_mul_action.is_scalar_tower
 
+instance
+  [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M]
+  [has_scalar Sᵐᵒᵖ R] [has_scalar Sᵐᵒᵖ M] [is_scalar_tower Sᵐᵒᵖ R M]
+  [is_central_scalar S M] : is_central_scalar S p :=
+p.to_sub_mul_action.is_central_scalar
+
 protected lemma nonempty : (p : set M).nonempty := ⟨0, p.zero_mem⟩
 
 @[simp] lemma mk_eq_zero {x} (h : x ∈ p) : (⟨x, h⟩ : p) = 0 ↔ x = 0 := subtype.ext_iff_val

diff --git a/src/group_theory/group_action/sub_mul_action.lean b/src/group_theory/group_action/sub_mul_action.lean
@@ -124,6 +124,10 @@ instance : is_scalar_tower S R p :=
   g • x ∈ p ↔ x ∈ p :=
 ⟨λ h, inv_smul_smul g x ▸ p.smul_of_tower_mem g⁻¹ h, p.smul_of_tower_mem g⟩
 
+instance [has_scalar Sᵐᵒᵖ R] [has_scalar Sᵐᵒᵖ M] [is_scalar_tower Sᵐᵒᵖ R M]
+  [is_central_scalar S M] : is_central_scalar S p :=
+{ op_smul_eq_smul := λ r x, subtype.ext $ op_smul_eq_smul r x }
+
 end
 
 section