From 4b07949617985410c885d84d777a68d5115b1841 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 13 Dec 2021 00:12:11 +0000 Subject: [PATCH] chore(algebra/module/submodule): missing is_central_scalar instance (#10720) --- src/algebra/module/submodule.lean | 6 ++++++ src/group_theory/group_action/sub_mul_action.lean | 4 ++++ 2 files changed, 10 insertions(+) diff --git a/src/algebra/module/submodule.lean b/src/algebra/module/submodule.lean index c3a100ff2db49..093b0fa09b012 100644 --- 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 index 1527c908ef04e..357f5b1b10538 100644 --- 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