Documentation

Mathlib.Algebra.Group.Submonoid.Pointwise

Pointwise instances on `Submonoid`s and `AddSubmonoid`s #

This file provides:

Submonoid.inv
AddSubmonoid.neg

and the actions

Submonoid.pointwiseMulAction
AddSubmonoid.pointwiseAddAction

which matches the action of Set.mulActionSet.

Implementation notes #

Most of the lemmas in this file are direct copies of lemmas from Mathlib.Algebra.Group.Pointwise.Set.Basic and Mathlib.Algebra.Group.Action.Pointwise.Set.Basic. 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 Sets.

@[simp]

theorem coe_mul_coe {M : Type u_3} {S : Type u_6} [Monoid M] [SetLike S M] [SubmonoidClass S M] (H : S) :

↑H * ↑H = ↑H

@[simp]

theorem coe_add_coe {M : Type u_3} {S : Type u_6} [AddMonoid M] [SetLike S M] [AddSubmonoidClass S M] (H : S) :

↑H + ↑H = ↑H

@[simp]

theorem coe_set_pow {M : Type u_3} {S : Type u_6} [Monoid M] [SetLike S M] [SubmonoidClass S M] {n : ℕ} (hn : n ≠ 0) (H : S) :

↑H ^ n = ↑H

@[simp]

theorem coe_set_nsmul {M : Type u_3} {S : Type u_6} [AddMonoid M] [SetLike S M] [AddSubmonoidClass S M] {n : ℕ} (hn : n ≠ 0) (H : S) :

n • ↑H = ↑H

Some lemmas about pointwise multiplication and submonoids. Ideally we put these in GroupTheory.Submonoid.Basic, but currently we cannot because that file is imported by this.

theorem Submonoid.mul_subset {M : Type u_3} [Monoid M] {s t : Set M} {S : Submonoid M} (hs : s ⊆ ↑S) (ht : t ⊆ ↑S) :

s * t ⊆ ↑S

theorem AddSubmonoid.add_subset {M : Type u_3} [AddMonoid M] {s t : Set M} {S : AddSubmonoid M} (hs : s ⊆ ↑S) (ht : t ⊆ ↑S) :

s + t ⊆ ↑S

theorem Submonoid.mul_subset_closure {M : Type u_3} [Monoid M] {s t u : Set M} (hs : s ⊆ u) (ht : t ⊆ u) :

s * t ⊆ ↑(closure u)

theorem AddSubmonoid.add_subset_closure {M : Type u_3} [AddMonoid M] {s t u : Set M} (hs : s ⊆ u) (ht : t ⊆ u) :

s + t ⊆ ↑(closure u)

theorem Submonoid.coe_mul_self_eq {M : Type u_3} [Monoid M] (s : Submonoid M) :

↑s * ↑s = ↑s

theorem AddSubmonoid.coe_add_self_eq {M : Type u_3} [AddMonoid M] (s : AddSubmonoid M) :

↑s + ↑s = ↑s

theorem Submonoid.closure_mul_le {M : Type u_3} [Monoid M] (S T : Set M) :

closure (S * T) ≤ closure S ⊔ closure T

theorem AddSubmonoid.closure_add_le {M : Type u_3} [AddMonoid M] (S T : Set M) :

closure (S + T) ≤ closure S ⊔ closure T

theorem Submonoid.closure_pow_le {M : Type u_3} [Monoid M] {s : Set M} {n : ℕ} :

n ≠ 0 → closure (s ^ n) ≤ closure s

theorem AddSubmonoid.closure_nsmul_le {M : Type u_3} [AddMonoid M] {s : Set M} {n : ℕ} :

n ≠ 0 → closure (n • s) ≤ closure s

theorem Submonoid.closure_pow {M : Type u_3} [Monoid M] {s : Set M} {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) :

closure (s ^ n) = closure s

theorem AddSubmonoid.closure_nsmul {M : Type u_3} [AddMonoid M] {s : Set M} {n : ℕ} (hs : 0 ∈ s) (hn : n ≠ 0) :

closure (n • s) = closure s

theorem Submonoid.sup_eq_closure_mul {M : Type u_3} [Monoid M] (H K : Submonoid M) :

H ⊔ K = closure (↑H * ↑K)

theorem AddSubmonoid.sup_eq_closure_add {M : Type u_3} [AddMonoid M] (H K : AddSubmonoid M) :

H ⊔ K = closure (↑H + ↑K)

theorem Submonoid.pow_smul_mem_closure_smul {M : Type u_3} [Monoid M] {N : Type u_7} [CommMonoid N] [MulAction M N] [IsScalarTower M N N] (r : M) (s : Set N) {x : N} (hx : x ∈ closure s) :

∃ (n : ℕ), r ^ n • x ∈ closure (r • s)

theorem AddSubmonoid.nsmul_vadd_mem_closure_vadd {M : Type u_3} [AddMonoid M] {N : Type u_7} [AddCommMonoid N] [AddAction M N] [VAddAssocClass M N N] (r : M) (s : Set N) {x : N} (hx : x ∈ closure s) :

∃ (n : ℕ), n • r +ᵥ x ∈ closure (r +ᵥ s)

def Submonoid.inv {G : Type u_2} [Group G] :

Inv (Submonoid G)

The submonoid with every element inverted.

Equations

Submonoid.inv = { inv := fun (S : Submonoid G) => { carrier := (↑S)⁻¹, mul_mem' := ⋯, one_mem' := ⋯ } }

Instances For

def AddSubmonoid.neg {G : Type u_2} [AddGroup G] :

Neg (AddSubmonoid G)

The additive submonoid with every element negated.

Equations

AddSubmonoid.neg = { neg := fun (S : AddSubmonoid G) => { carrier := -↑S, add_mem' := ⋯, zero_mem' := ⋯ } }

Instances For

@[simp]

theorem Submonoid.coe_inv {G : Type u_2} [Group G] (S : Submonoid G) :

↑S⁻¹ = (↑S)⁻¹

@[simp]

theorem AddSubmonoid.coe_neg {G : Type u_2} [AddGroup G] (S : AddSubmonoid G) :

↑(-S) = -↑S

@[simp]

theorem Submonoid.mem_inv {G : Type u_2} [Group G] {g : G} {S : Submonoid G} :

g ∈ S⁻¹ ↔ g⁻¹ ∈ S

@[simp]

theorem AddSubmonoid.mem_neg {G : Type u_2} [AddGroup G] {g : G} {S : AddSubmonoid G} :

g ∈ -S ↔ -g ∈ S

def Submonoid.involutiveInv {G : Type u_2} [Group G] :

InvolutiveInv (Submonoid G)

Inversion is involutive on submonoids.

Equations

Submonoid.involutiveInv = Function.Injective.involutiveInv SetLike.coe ⋯ ⋯

Instances For

def AddSubmonoid.involutiveNeg {G : Type u_2} [AddGroup G] :

InvolutiveNeg (AddSubmonoid G)

Inversion is involutive on additive submonoids.

Equations

AddSubmonoid.involutiveNeg = Function.Injective.involutiveNeg SetLike.coe ⋯ ⋯

Instances For

@[simp]

theorem Submonoid.inv_le_inv {G : Type u_2} [Group G] (S T : Submonoid G) :

S⁻¹ ≤ T⁻¹ ↔ S ≤ T

@[simp]

theorem AddSubmonoid.neg_le_neg {G : Type u_2} [AddGroup G] (S T : AddSubmonoid G) :

-S ≤ -T ↔ S ≤ T

theorem Submonoid.inv_le {G : Type u_2} [Group G] (S T : Submonoid G) :

S⁻¹ ≤ T ↔ S ≤ T⁻¹

theorem AddSubmonoid.neg_le {G : Type u_2} [AddGroup G] (S T : AddSubmonoid G) :

-S ≤ T ↔ S ≤ -T

def Submonoid.invOrderIso {G : Type u_2} [Group G] :

Submonoid G ≃o Submonoid G

Pointwise inversion of submonoids as an order isomorphism.

Equations

Submonoid.invOrderIso = { toEquiv := Equiv.inv (Submonoid G), map_rel_iff' := ⋯ }

Instances For

def AddSubmonoid.negOrderIso {G : Type u_2} [AddGroup G] :

AddSubmonoid G ≃o AddSubmonoid G

Pointwise negation of additive submonoids as an order isomorphism

Equations

AddSubmonoid.negOrderIso = { toEquiv := Equiv.neg (AddSubmonoid G), map_rel_iff' := ⋯ }

Instances For

@[simp]

theorem Submonoid.coe_invOrderIso_symm_apply {G : Type u_2} [Group G] (a✝ : Submonoid G) :

↑((RelIso.symm invOrderIso) a✝) = (↑a✝)⁻¹

@[simp]

theorem Submonoid.coe_invOrderIso_apply {G : Type u_2} [Group G] (a✝ : Submonoid G) :

↑(invOrderIso a✝) = (↑a✝)⁻¹

@[simp]

theorem AddSubmonoid.coe_negOrderIso_symm_apply {G : Type u_2} [AddGroup G] (a✝ : AddSubmonoid G) :

↑((RelIso.symm negOrderIso) a✝) = -↑a✝

@[simp]

theorem AddSubmonoid.coe_negOrderIso_apply {G : Type u_2} [AddGroup G] (a✝ : AddSubmonoid G) :

↑(negOrderIso a✝) = -↑a✝

theorem Submonoid.closure_inv {G : Type u_2} [Group G] (s : Set G) :

closure s⁻¹ = (closure s)⁻¹

theorem AddSubmonoid.closure_neg {G : Type u_2} [AddGroup G] (s : Set G) :

closure (-s) = -closure s

theorem Submonoid.mem_closure_inv {G : Type u_2} [Group G] (s : Set G) (x : G) :

x ∈ closure s⁻¹ ↔ x⁻¹ ∈ closure s

theorem AddSubmonoid.mem_closure_neg {G : Type u_2} [AddGroup G] (s : Set G) (x : G) :

x ∈ closure (-s) ↔ -x ∈ closure s

@[simp]

theorem Submonoid.inv_inf {G : Type u_2} [Group G] (S T : Submonoid G) :

(S ⊓ T)⁻¹ = S⁻¹ ⊓ T⁻¹

@[simp]

theorem AddSubmonoid.neg_inf {G : Type u_2} [AddGroup G] (S T : AddSubmonoid G) :

-(S ⊓ T) = -S ⊓ -T

@[simp]

theorem Submonoid.inv_sup {G : Type u_2} [Group G] (S T : Submonoid G) :

(S ⊔ T)⁻¹ = S⁻¹ ⊔ T⁻¹

@[simp]

theorem AddSubmonoid.neg_sup {G : Type u_2} [AddGroup G] (S T : AddSubmonoid G) :

-(S ⊔ T) = -S ⊔ -T

@[simp]

theorem Submonoid.inv_bot {G : Type u_2} [Group G] :

@[simp]

theorem AddSubmonoid.neg_bot {G : Type u_2} [AddGroup G] :

@[simp]

theorem Submonoid.inv_top {G : Type u_2} [Group G] :

@[simp]

theorem AddSubmonoid.neg_top {G : Type u_2} [AddGroup G] :

@[simp]

theorem Submonoid.inv_iInf {G : Type u_2} [Group G] {ι : Sort u_7} (S : ι → Submonoid G) :

(⨅ (i : ι), S i)⁻¹ = ⨅ (i : ι), (S i)⁻¹

@[simp]

theorem AddSubmonoid.neg_iInf {G : Type u_2} [AddGroup G] {ι : Sort u_7} (S : ι → AddSubmonoid G) :

-⨅ (i : ι), S i = ⨅ (i : ι), -S i

@[simp]

theorem Submonoid.inv_iSup {G : Type u_2} [Group G] {ι : Sort u_7} (S : ι → Submonoid G) :

(⨆ (i : ι), S i)⁻¹ = ⨆ (i : ι), (S i)⁻¹

@[simp]

theorem AddSubmonoid.neg_iSup {G : Type u_2} [AddGroup G] {ι : Sort u_7} (S : ι → AddSubmonoid G) :

-⨆ (i : ι), S i = ⨆ (i : ι), -S i

def Submonoid.pointwiseMulAction {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] :

MulAction α (Submonoid M)

The action on a submonoid corresponding to applying the action to every element.

This is available as an instance in the Pointwise locale.

Equations

Submonoid.pointwiseMulAction = { smul := fun (a : α) (S : Submonoid M) => Submonoid.map ((MulDistribMulAction.toMonoidEnd α M) a) S, one_smul := ⋯, mul_smul := ⋯ }

Instances For

@[simp]

theorem Submonoid.coe_pointwise_smul {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (a : α) (S : Submonoid M) :

↑(a • S) = a • ↑S

theorem Submonoid.smul_mem_pointwise_smul {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (m : M) (a : α) (S : Submonoid M) :

m ∈ S → a • m ∈ a • S

instance Submonoid.instCovariantClassHSMulLe {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] :

CovariantClass α (Submonoid M) HSMul.hSMul LE.le

theorem Submonoid.mem_smul_pointwise_iff_exists {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (m : M) (a : α) (S : Submonoid M) :

m ∈ a • S ↔ ∃ s ∈ S, a • s = m

@[simp]

theorem Submonoid.smul_bot {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (a : α) :

a • ⊥ = ⊥

theorem Submonoid.smul_sup {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (a : α) (S T : Submonoid M) :

a • (S ⊔ T) = a • S ⊔ a • T

theorem Submonoid.smul_closure {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] (a : α) (s : Set M) :

a • closure s = closure (a • s)

theorem Submonoid.pointwise_isCentralScalar {α : Type u_1} {M : Type u_3} [Monoid M] [Monoid α] [MulDistribMulAction α M] [MulDistribMulAction αᵐᵒᵖ M] [IsCentralScalar α M] :

IsCentralScalar α (Submonoid M)

@[simp]

theorem Submonoid.smul_mem_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S : Submonoid M} {x : M} :

a • x ∈ a • S ↔ x ∈ S

theorem Submonoid.mem_pointwise_smul_iff_inv_smul_mem {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S : Submonoid M} {x : M} :

x ∈ a • S ↔ a⁻¹ • x ∈ S

theorem Submonoid.mem_inv_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S : Submonoid M} {x : M} :

x ∈ a⁻¹ • S ↔ a • x ∈ S

@[simp]

theorem Submonoid.pointwise_smul_le_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S T : Submonoid M} :

a • S ≤ a • T ↔ S ≤ T

theorem Submonoid.pointwise_smul_subset_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S T : Submonoid M} :

a • S ≤ T ↔ S ≤ a⁻¹ • T

theorem Submonoid.subset_pointwise_smul_iff {α : Type u_1} {M : Type u_3} [Monoid M] [Group α] [MulDistribMulAction α M] {a : α} {S T : Submonoid M} :

S ≤ a • T ↔ a⁻¹ • S ≤ T

theorem Set.IsPWO.submonoid_closure {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α] {s : Set α} (hpos : ∀ x ∈ s, 1 ≤ x) (h : s.IsPWO) :

(↑(Submonoid.closure s)).IsPWO

theorem Set.IsPWO.addSubmonoid_closure {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] {s : Set α} (hpos : ∀ x ∈ s, 0 ≤ x) (h : s.IsPWO) :

(↑(AddSubmonoid.closure s)).IsPWO