Pointwise instances on Subgroup and AddSubgroups #
This file provides the actions
which matches the action of Set.mulActionSet.
These actions are available in the Pointwise locale.
Implementation notes #
The pointwise section of this file is almost identical to
the file Mathlib.Algebra.Group.Submonoid.Pointwise.
Where possible, try to keep them in sync.
@[simp]
theorem
inv_coe_set
{G : Type u_2}
{S : Type u_4}
[InvolutiveInv G]
[SetLike S G]
[InvMemClass S G]
{H : S}
:
@[simp]
theorem
neg_coe_set
{G : Type u_2}
{S : Type u_4}
[InvolutiveNeg G]
[SetLike S G]
[NegMemClass S G]
{H : S}
:
@[simp]
theorem
smul_coe_set
{G : Type u_2}
{S : Type u_4}
[Group G]
[SetLike S G]
[SubgroupClass S G]
{s : S}
{a : G}
(ha : a ∈ s)
:
@[simp]
theorem
vadd_coe_set
{G : Type u_2}
{S : Type u_4}
[AddGroup G]
[SetLike S G]
[AddSubgroupClass S G]
{s : S}
{a : G}
(ha : a ∈ s)
:
@[simp]
theorem
op_smul_coe_set
{G : Type u_2}
{S : Type u_4}
[Group G]
[SetLike S G]
[SubgroupClass S G]
{s : S}
{a : G}
(ha : a ∈ s)
:
MulOpposite.op a • ↑s = ↑s
@[simp]
theorem
op_vadd_coe_set
{G : Type u_2}
{S : Type u_4}
[AddGroup G]
[SetLike S G]
[AddSubgroupClass S G]
{s : S}
{a : G}
(ha : a ∈ s)
:
AddOpposite.op a +ᵥ ↑s = ↑s
@[simp]
theorem
coe_div_coe
{G : Type u_2}
{S : Type u_4}
[SetLike S G]
[DivisionMonoid G]
[SubgroupClass S G]
(H : S)
:
@[simp]
theorem
coe_sub_coe
{G : Type u_2}
{S : Type u_4}
[SetLike S G]
[SubtractionMonoid G]
[AddSubgroupClass S G]
(H : S)
:
@[simp]
theorem
Set.mul_subgroupClosure
{G : Type u_2}
[Group G]
{s : Set G}
(hs : s.Nonempty)
:
s * ↑(Subgroup.closure s) = ↑(Subgroup.closure s)
@[simp]
theorem
Set.add_addSubgroupClosure
{G : Type u_2}
[AddGroup G]
{s : Set G}
(hs : s.Nonempty)
:
s + ↑(AddSubgroup.closure s) = ↑(AddSubgroup.closure s)
@[simp]
theorem
Set.subgroupClosure_mul
{G : Type u_2}
[Group G]
{s : Set G}
(hs : s.Nonempty)
:
↑(Subgroup.closure s) * s = ↑(Subgroup.closure s)
@[simp]
theorem
Set.addSubgroupClosure_add
{G : Type u_2}
[AddGroup G]
{s : Set G}
(hs : s.Nonempty)
:
↑(AddSubgroup.closure s) + s = ↑(AddSubgroup.closure s)
@[simp]
theorem
Set.pow_mul_subgroupClosure
{G : Type u_2}
[Group G]
{s : Set G}
(hs : s.Nonempty)
(n : ℕ)
:
s ^ n * ↑(Subgroup.closure s) = ↑(Subgroup.closure s)
@[simp]
theorem
Set.nsmul_add_addSubgroupClosure
{G : Type u_2}
[AddGroup G]
{s : Set G}
(hs : s.Nonempty)
(n : ℕ)
:
n • s + ↑(AddSubgroup.closure s) = ↑(AddSubgroup.closure s)
@[simp]
theorem
Set.subgroupClosure_mul_pow
{G : Type u_2}
[Group G]
{s : Set G}
(hs : s.Nonempty)
(n : ℕ)
:
↑(Subgroup.closure s) * s ^ n = ↑(Subgroup.closure s)
@[simp]
theorem
Set.addSubgroupClosure_add_nsmul
{G : Type u_2}
[AddGroup G]
{s : Set G}
(hs : s.Nonempty)
(n : ℕ)
:
↑(AddSubgroup.closure s) + n • s = ↑(AddSubgroup.closure s)
@[simp]
theorem
Subgroup.inv_subset_closure
{G : Type u_2}
[Group G]
(S : Set G)
:
S⁻¹ ⊆ ↑(Subgroup.closure S)
@[simp]
theorem
AddSubgroup.neg_subset_closure
{G : Type u_2}
[AddGroup G]
(S : Set G)
:
-S ⊆ ↑(AddSubgroup.closure S)
theorem
Subgroup.closure_toSubmonoid
{G : Type u_2}
[Group G]
(S : Set G)
:
(Subgroup.closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)
theorem
AddSubgroup.closure_toAddSubmonoid
{G : Type u_2}
[AddGroup G]
(S : Set G)
:
(AddSubgroup.closure S).toAddSubmonoid = AddSubmonoid.closure (S ∪ -S)
theorem
Subgroup.closure_induction_left
{G : Type u_2}
[Group G]
{s : Set G}
{p : (x : G) → x ∈ Subgroup.closure s → Prop}
(one : p 1 ⋯)
(mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x * y) ⋯)
(inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x⁻¹ * y) ⋯)
{x : G}
(h : x ∈ Subgroup.closure s)
:
p x h
For subgroups generated by a single element, see the simpler zpow_induction_left.
theorem
AddSubgroup.closure_induction_left
{G : Type u_2}
[AddGroup G]
{s : Set G}
{p : (x : G) → x ∈ AddSubgroup.closure s → Prop}
(one : p 0 ⋯)
(mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (x + y) ⋯)
(inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (-x + y) ⋯)
{x : G}
(h : x ∈ AddSubgroup.closure s)
:
p x h
For additive subgroups generated by a single element, see the simpler
zsmul_induction_left.
theorem
Subgroup.closure_induction_right
{G : Type u_2}
[Group G]
{s : Set G}
{p : (x : G) → x ∈ Subgroup.closure s → Prop}
(one : p 1 ⋯)
(mul_right : ∀ (x : G) (hx : x ∈ Subgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯)
(mul_inv_cancel : ∀ (x : G) (hx : x ∈ Subgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯)
{x : G}
(h : x ∈ Subgroup.closure s)
:
p x h
For subgroups generated by a single element, see the simpler zpow_induction_right.
theorem
AddSubgroup.closure_induction_right
{G : Type u_2}
[AddGroup G]
{s : Set G}
{p : (x : G) → x ∈ AddSubgroup.closure s → Prop}
(one : p 0 ⋯)
(mul_right : ∀ (x : G) (hx : x ∈ AddSubgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x + y) ⋯)
(mul_inv_cancel : ∀ (x : G) (hx : x ∈ AddSubgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x + -y) ⋯)
{x : G}
(h : x ∈ AddSubgroup.closure s)
:
p x h
For additive subgroups generated by a single element, see the simpler
zsmul_induction_right.
@[simp]
@[simp]
@[simp]
theorem
Subgroup.closure_singleton_inv
{G : Type u_2}
[Group G]
(x : G)
:
Subgroup.closure {x⁻¹} = Subgroup.closure {x}
@[simp]
theorem
AddSubgroup.closure_singleton_neg
{G : Type u_2}
[AddGroup G]
(x : G)
:
AddSubgroup.closure {-x} = AddSubgroup.closure {x}
theorem
Subgroup.closure_induction''
{G : Type u_2}
[Group G]
{s : Set G}
{p : (g : G) → g ∈ Subgroup.closure s → Prop}
(mem : ∀ (x : G) (hx : x ∈ s), p x ⋯)
(inv_mem : ∀ (x : G) (hx : x ∈ s), p x⁻¹ ⋯)
(one : p 1 ⋯)
(mul : ∀ (x y : G) (hx : x ∈ Subgroup.closure s) (hy : y ∈ Subgroup.closure s), p x hx → p y hy → p (x * y) ⋯)
{x : G}
(h : x ∈ Subgroup.closure s)
:
p x h
An induction principle for closure membership. If p holds for 1 and all elements of
k and their inverse, and is preserved under multiplication, then p holds for all elements of
the closure of k.
theorem
AddSubgroup.closure_induction''
{G : Type u_2}
[AddGroup G]
{s : Set G}
{p : (g : G) → g ∈ AddSubgroup.closure s → Prop}
(mem : ∀ (x : G) (hx : x ∈ s), p x ⋯)
(inv_mem : ∀ (x : G) (hx : x ∈ s), p (-x) ⋯)
(one : p 0 ⋯)
(mul : ∀ (x y : G) (hx : x ∈ AddSubgroup.closure s) (hy : y ∈ AddSubgroup.closure s), p x hx → p y hy → p (x + y) ⋯)
{x : G}
(h : x ∈ AddSubgroup.closure s)
:
p x h
An induction principle for additive closure membership. If p holds for 0 and all
elements of k and their negation, and is preserved under addition, then p holds for all
elements of the additive closure of k.
theorem
Subgroup.iSup_induction
{G : Type u_2}
[Group G]
{ι : Sort u_5}
(S : ι → Subgroup G)
{C : G → Prop}
{x : G}
(hx : x ∈ ⨆ (i : ι), S i)
(mem : ∀ (i : ι), ∀ x ∈ S i, C x)
(one : C 1)
(mul : ∀ (x y : G), C x → C y → C (x * y))
:
C x
An induction principle for elements of ⨆ i, S i.
If C holds for 1 and all elements of S i for all i, and is preserved under multiplication,
then it holds for all elements of the supremum of S.
theorem
AddSubgroup.iSup_induction
{G : Type u_2}
[AddGroup G]
{ι : Sort u_5}
(S : ι → AddSubgroup G)
{C : G → Prop}
{x : G}
(hx : x ∈ ⨆ (i : ι), S i)
(mem : ∀ (i : ι), ∀ x ∈ S i, C x)
(one : C 0)
(mul : ∀ (x y : G), C x → C y → C (x + y))
:
C x
An induction principle for elements of ⨆ i, S i.
If C holds for 0 and all elements of S i for all i, and is preserved under addition,
then it holds for all elements of the supremum of S.
theorem
Subgroup.iSup_induction'
{G : Type u_2}
[Group G]
{ι : Sort u_5}
(S : ι → Subgroup G)
{C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop}
(hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯)
(h1 : C 1 ⋯)
(hmul : ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), C x hx → C y hy → C (x * y) ⋯)
{x : G}
(hx : x ∈ ⨆ (i : ι), S i)
:
C x hx
A dependent version of Subgroup.iSup_induction.
theorem
AddSubgroup.iSup_induction'
{G : Type u_2}
[AddGroup G]
{ι : Sort u_5}
(S : ι → AddSubgroup G)
{C : (x : G) → x ∈ ⨆ (i : ι), S i → Prop}
(hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯)
(h1 : C 0 ⋯)
(hmul : ∀ (x y : G) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), C x hx → C y hy → C (x + y) ⋯)
{x : G}
(hx : x ∈ ⨆ (i : ι), S i)
:
C x hx
A dependent version of AddSubgroup.iSup_induction.
theorem
Subgroup.closure_mul_le
{G : Type u_2}
[Group G]
(S T : Set G)
:
Subgroup.closure (S * T) ≤ Subgroup.closure S ⊔ Subgroup.closure T
theorem
AddSubgroup.closure_add_le
{G : Type u_2}
[AddGroup G]
(S T : Set G)
:
AddSubgroup.closure (S + T) ≤ AddSubgroup.closure S ⊔ AddSubgroup.closure T
theorem
Subgroup.sup_eq_closure_mul
{G : Type u_2}
[Group G]
(H K : Subgroup G)
:
H ⊔ K = Subgroup.closure (↑H * ↑K)
theorem
AddSubgroup.sup_eq_closure_add
{G : Type u_2}
[AddGroup G]
(H K : AddSubgroup G)
:
H ⊔ K = AddSubgroup.closure (↑H + ↑K)
theorem
AddSubgroup.set_add_normal_comm
{G : Type u_2}
[AddGroup G]
(s : Set G)
(N : AddSubgroup G)
[hN : N.Normal]
:
The carrier of H ⊔ N is just ↑H + ↑N (pointwise set addition)
when N is normal.
The carrier of N ⊔ H is just ↑N + ↑H (pointwise set addition)
when N is normal.
instance
AddSubgroup.sup_normal
{G : Type u_2}
[AddGroup G]
(H K : AddSubgroup G)
[hH : H.Normal]
[hK : K.Normal]
:
(H ⊔ K).Normal
Equations
- ⋯ = ⋯
Pointwise action #
def
Subgroup.pointwiseMulAction
{α : Type u_1}
{G : Type u_2}
[Group G]
[Monoid α]
[MulDistribMulAction α G]
:
The action on a subgroup corresponding to applying the action to every element.
This is available as an instance in the Pointwise locale.
Equations
- Subgroup.pointwiseMulAction = MulAction.mk ⋯ ⋯
Instances For
theorem
Subgroup.pointwise_smul_def
{α : Type u_1}
{G : Type u_2}
[Group G]
[Monoid α]
[MulDistribMulAction α G]
{a : α}
(S : Subgroup G)
:
a • S = Subgroup.map ((MulDistribMulAction.toMonoidEnd α G) a) S
instance
Subgroup.instCovariantClassHSMulLe
{α : Type u_1}
{G : Type u_2}
[Group G]
[Monoid α]
[MulDistribMulAction α G]
:
CovariantClass α (Subgroup G) HSMul.hSMul LE.le
Equations
- ⋯ = ⋯
theorem
Subgroup.smul_closure
{α : Type u_1}
{G : Type u_2}
[Group G]
[Monoid α]
[MulDistribMulAction α G]
(a : α)
(s : Set G)
:
a • Subgroup.closure s = Subgroup.closure (a • s)
instance
Subgroup.pointwise_isCentralScalar
{α : Type u_1}
{G : Type u_2}
[Group G]
[Monoid α]
[MulDistribMulAction α G]
[MulDistribMulAction αᵐᵒᵖ G]
[IsCentralScalar α G]
:
IsCentralScalar α (Subgroup G)
Equations
- ⋯ = ⋯
def
Subgroup.equivSMul
{α : Type u_1}
{G : Type u_2}
[Group G]
[Group α]
[MulDistribMulAction α G]
(a : α)
(H : Subgroup G)
:
Applying a MulDistribMulAction results in an isomorphic subgroup
Equations
- Subgroup.equivSMul a H = (MulDistribMulAction.toMulEquiv G a).subgroupMap H
Instances For
@[simp]
theorem
Subgroup.equivSMul_symm_apply_coe
{α : Type u_1}
{G : Type u_2}
[Group G]
[Group α]
[MulDistribMulAction α G]
(a : α)
(H : Subgroup G)
(y : ↑(⇑↑(MulDistribMulAction.toMulEquiv G a) '' ↑H.toSubmonoid))
:
↑((Subgroup.equivSMul a H).symm y) = a⁻¹ • ↑y
@[simp]
theorem
Subgroup.equivSMul_apply_coe
{α : Type u_1}
{G : Type u_2}
[Group G]
[Group α]
[MulDistribMulAction α G]
(a : α)
(H : Subgroup G)
(x : ↑↑H.toSubmonoid)
:
↑((Subgroup.equivSMul a H) x) = a • ↑x
@[simp]
theorem
Subgroup.smul_mem_pointwise_smul_iff₀
{α : Type u_1}
{G : Type u_2}
[Group G]
[GroupWithZero α]
[MulDistribMulAction α G]
{a : α}
(ha : a ≠ 0)
(S : Subgroup G)
(x : G)
:
theorem
Subgroup.mem_pointwise_smul_iff_inv_smul_mem₀
{α : Type u_1}
{G : Type u_2}
[Group G]
[GroupWithZero α]
[MulDistribMulAction α G]
{a : α}
(ha : a ≠ 0)
(S : Subgroup G)
(x : G)
:
theorem
Subgroup.mem_inv_pointwise_smul_iff₀
{α : Type u_1}
{G : Type u_2}
[Group G]
[GroupWithZero α]
[MulDistribMulAction α G]
{a : α}
(ha : a ≠ 0)
(S : Subgroup G)
(x : G)
:
@[simp]
theorem
Subgroup.pointwise_smul_le_pointwise_smul_iff₀
{α : Type u_1}
{G : Type u_2}
[Group G]
[GroupWithZero α]
[MulDistribMulAction α G]
{a : α}
(ha : a ≠ 0)
{S T : Subgroup G}
:
theorem
Subgroup.pointwise_smul_le_iff₀
{α : Type u_1}
{G : Type u_2}
[Group G]
[GroupWithZero α]
[MulDistribMulAction α G]
{a : α}
(ha : a ≠ 0)
{S T : Subgroup G}
:
theorem
Subgroup.le_pointwise_smul_iff₀
{α : Type u_1}
{G : Type u_2}
[Group G]
[GroupWithZero α]
[MulDistribMulAction α G]
{a : α}
(ha : a ≠ 0)
{S T : Subgroup G}
:
def
AddSubgroup.pointwiseMulAction
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
:
MulAction α (AddSubgroup A)
The action on an additive subgroup corresponding to applying the action to every element.
This is available as an instance in the Pointwise locale.
Equations
- AddSubgroup.pointwiseMulAction = MulAction.mk ⋯ ⋯
Instances For
theorem
AddSubgroup.pointwise_smul_def
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
{a : α}
(S : AddSubgroup A)
:
a • S = AddSubgroup.map ((DistribMulAction.toAddMonoidEnd α A) a) S
@[simp]
theorem
AddSubgroup.coe_pointwise_smul
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
(a : α)
(S : AddSubgroup A)
:
@[simp]
theorem
AddSubgroup.pointwise_smul_toAddSubmonoid
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
(a : α)
(S : AddSubgroup A)
:
theorem
AddSubgroup.smul_mem_pointwise_smul
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
(m : A)
(a : α)
(S : AddSubgroup A)
:
theorem
AddSubgroup.mem_smul_pointwise_iff_exists
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
(m : A)
(a : α)
(S : AddSubgroup A)
:
instance
AddSubgroup.pointwise_isCentralScalar
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Monoid α]
[DistribMulAction α A]
[DistribMulAction αᵐᵒᵖ A]
[IsCentralScalar α A]
:
IsCentralScalar α (AddSubgroup A)
Equations
- ⋯ = ⋯
@[simp]
theorem
AddSubgroup.smul_mem_pointwise_smul_iff
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Group α]
[DistribMulAction α A]
{a : α}
{S : AddSubgroup A}
{x : A}
:
theorem
AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Group α]
[DistribMulAction α A]
{a : α}
{S : AddSubgroup A}
{x : A}
:
theorem
AddSubgroup.mem_inv_pointwise_smul_iff
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Group α]
[DistribMulAction α A]
{a : α}
{S : AddSubgroup A}
{x : A}
:
@[simp]
theorem
AddSubgroup.pointwise_smul_le_pointwise_smul_iff
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Group α]
[DistribMulAction α A]
{a : α}
{S T : AddSubgroup A}
:
theorem
AddSubgroup.pointwise_smul_le_iff
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Group α]
[DistribMulAction α A]
{a : α}
{S T : AddSubgroup A}
:
theorem
AddSubgroup.le_pointwise_smul_iff
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[Group α]
[DistribMulAction α A]
{a : α}
{S T : AddSubgroup A}
:
@[simp]
theorem
AddSubgroup.smul_mem_pointwise_smul_iff₀
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[GroupWithZero α]
[DistribMulAction α A]
{a : α}
(ha : a ≠ 0)
(S : AddSubgroup A)
(x : A)
:
theorem
AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem₀
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[GroupWithZero α]
[DistribMulAction α A]
{a : α}
(ha : a ≠ 0)
(S : AddSubgroup A)
(x : A)
:
theorem
AddSubgroup.mem_inv_pointwise_smul_iff₀
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[GroupWithZero α]
[DistribMulAction α A]
{a : α}
(ha : a ≠ 0)
(S : AddSubgroup A)
(x : A)
:
@[simp]
theorem
AddSubgroup.pointwise_smul_le_pointwise_smul_iff₀
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[GroupWithZero α]
[DistribMulAction α A]
{a : α}
(ha : a ≠ 0)
{S T : AddSubgroup A}
:
theorem
AddSubgroup.pointwise_smul_le_iff₀
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[GroupWithZero α]
[DistribMulAction α A]
{a : α}
(ha : a ≠ 0)
{S T : AddSubgroup A}
:
theorem
AddSubgroup.le_pointwise_smul_iff₀
{α : Type u_1}
{A : Type u_3}
[AddGroup A]
[GroupWithZero α]
[DistribMulAction α A]
{a : α}
(ha : a ≠ 0)
{S T : AddSubgroup A}
:
For additive subgroups S and T of a ring, the product of S and T as submonoids
is automatically a subgroup, which we define as the product of S and T as subgroups.
Equations
- AddSubgroup.mul = { mul := fun (M N : AddSubgroup R) => let __spread.0 := M.toAddSubmonoid * N.toAddSubmonoid; { toAddSubmonoid := __spread.0, neg_mem' := ⋯ } }
Instances For
theorem
AddSubgroup.mul_toAddSubmonoid
{R : Type u_5}
[NonUnitalNonAssocRing R]
(M N : AddSubgroup R)
: