Documentation

Mathlib.Algebra.Group.Submonoid.Support

Supports of submonoids #

Let G be an (additive) group, and let M be a submonoid of G. The support of M is M ∩ -M, the largest subgroup of G contained in M. A submonoid C is pointed, or a positive cone, if it has zero support. A submonoid C is spanning if the subgroup it generates is G itself.

The names for these concepts are taken from the theory of convex cones.

Main definitions #

AddSubmonoid.support: the support of a submonoid.
AddSubmonoid.IsPointed: typeclass for submonoids with zero support.
AddSubmonoid.IsSpanning: typeclass for submonoids generating the whole group.

def Submonoid.mulSupport {G : Type u_1} [Group G] (M : Submonoid G) :

The support of a submonoid M of a group G is M ∩ M⁻¹, the largest subgroup of G contained in M.

Instances For

def AddSubmonoid.support {G : Type u_1} [AddGroup G] (M : AddSubmonoid G) :

The support of a submonoid M of a group G is M ∩ -M, the largest subgroup of G contained in M.

Instances For

@[simp]

theorem Submonoid.coe_mulSupport {G : Type u_1} [Group G] (M : Submonoid G) :

↑M.mulSupport = ↑M ∩ (↑M)⁻¹

@[simp]

theorem AddSubmonoid.coe_support {G : Type u_1} [AddGroup G] (M : AddSubmonoid G) :

↑M.support = ↑M ∩ -↑M

@[simp]

theorem Submonoid.mem_mulSupport {G : Type u_1} [Group G] {M : Submonoid G} {x : G} :

x ∈ M.mulSupport ↔ x ∈ M ∧ x⁻¹ ∈ M

@[simp]

theorem AddSubmonoid.mem_support {G : Type u_1} [AddGroup G] {M : AddSubmonoid G} {x : G} :

x ∈ M.support ↔ x ∈ M ∧ -x ∈ M

@[simp]

theorem Submonoid.mulSupport_toSubmonoid {G : Type u_1} [Group G] (M : Submonoid G) :

M.mulSupport.toSubmonoid = M ⊓ M⁻¹

@[simp]

theorem AddSubmonoid.support_toAddSubmonoid {G : Type u_1} [AddGroup G] (M : AddSubmonoid G) :

M.support.toAddSubmonoid = M ⊓ -M

theorem Subgroup.gc_toSubmonoid_mulSupport {G : Type u_1} [Group G] :

GaloisConnection toSubmonoid Submonoid.mulSupport

theorem AddSubgroup.gc_toAddSubmonoid_support {G : Type u_1} [AddGroup G] :

GaloisConnection toAddSubmonoid AddSubmonoid.support

def Submonoid.IsMulPointed {G : Type u_1} [Group G] (M : Submonoid G) :

A submonoid is pointed if it has zero support.

Instances For

def AddSubmonoid.IsPointed {G : Type u_1} [AddGroup G] (M : AddSubmonoid G) :

A submonoid is pointed if it has zero support.

Instances For

theorem Submonoid.IsMulPointed.mk {G : Type u_1} [Group G] {M : Submonoid G} (h : ∀ x ∈ M, x⁻¹ ∈ M → x = 1) :

theorem AddSubmonoid.IsPointed.mk {G : Type u_1} [AddGroup G] {M : AddSubmonoid G} (h : ∀ x ∈ M, -x ∈ M → x = 0) :

theorem Submonoid.IsMulPointed.eq_one_of_mem_of_inv_mem {G : Type u_1} [Group G] {M : Submonoid G} (hM : M.IsMulPointed) {x : G} (hx₁ : x ∈ M) (hx₂ : x⁻¹ ∈ M) :

x = 1

theorem AddSubmonoid.IsPointed.eq_zero_of_mem_of_neg_mem {G : Type u_1} [AddGroup G] {M : AddSubmonoid G} (hM : M.IsPointed) {x : G} (hx₁ : x ∈ M) (hx₂ : -x ∈ M) :

x = 0

theorem Submonoid.IsMulPointed.eq_one_of_mem_of_inv_mem₂ {G : Type u_1} [Group G] {M : Submonoid G} (hM : M.IsMulPointed) {x : G} (hx₁ : x ∈ M) (hx₂ : x⁻¹ ∈ M) :

x = 1

Alias of Submonoid.IsMulPointed.eq_one_of_mem_of_inv_mem.

theorem AddSubmonoid.IsPointed.eq_zero_of_mem_of_neg_mem₂ {G : Type u_1} [AddGroup G] {M : AddSubmonoid G} (hM : M.IsPointed) {x : G} (hx₁ : x ∈ M) (hx₂ : -x ∈ M) :

x = 0

theorem isMulPointed_iff_mulSupport_eq_bot {G : Type u_1} [Group G] {M : Submonoid G} :

M.IsMulPointed ↔ M.mulSupport = ⊥

theorem isPointed_iff_support_eq_bot {G : Type u_1} [AddGroup G] {M : AddSubmonoid G} :

M.IsPointed ↔ M.support = ⊥

@[simp]

theorem Submonoid.IsMulPointed.mulSupport_eq_bot {G : Type u_1} [Group G] {M : Submonoid G} :

M.IsMulPointed → M.mulSupport = ⊥

Alias of the forward direction of isMulPointed_iff_mulSupport_eq_bot.

@[simp]

theorem AddSubmonoid.IsPointed.support_eq_bot {G : Type u_1} [AddGroup G] {M : AddSubmonoid G} :

M.IsPointed → M.support = ⊥

theorem Submonoid.IsMulPointed.of_mulSupport_eq_bot {G : Type u_1} [Group G] {M : Submonoid G} :

M.mulSupport = ⊥ → M.IsMulPointed

Alias of the reverse direction of isMulPointed_iff_mulSupport_eq_bot.

theorem AddSubmonoid.IsPointed.of_support_eq_bot {G : Type u_1} [AddGroup G] {M : AddSubmonoid G} :

M.support = ⊥ → M.IsPointed

def Submonoid.IsMulSpanning {G : Type u_1} [Group G] (M : Submonoid G) :

A submonoid M of a group G is spanning if M generates G as a subgroup.

Instances For

def AddSubmonoid.IsSpanning {G : Type u_1} [AddGroup G] (M : AddSubmonoid G) :

A submonoid M of a group G is spanning if M generates G as a subgroup.

Instances For

theorem Submonoid.IsMulSpanning.mk {G : Type u_1} [Group G] {M : Submonoid G} (h : ∀ (a : G), a ∈ M ∨ a⁻¹ ∈ M) :

M.IsMulSpanning

theorem AddSubmonoid.IsSpanning.mk {G : Type u_1} [AddGroup G] {M : AddSubmonoid G} (h : ∀ (a : G), a ∈ M ∨ -a ∈ M) :

theorem Submonoid.IsMulSpanning.mem_or_inv_mem {G : Type u_1} [Group G] {M : Submonoid G} (hM : M.IsMulSpanning) (a : G) :

a ∈ M ∨ a⁻¹ ∈ M

theorem AddSubmonoid.IsSpanning.mem_or_neg_mem {G : Type u_1} [AddGroup G] {M : AddSubmonoid G} (hM : M.IsSpanning) (a : G) :

a ∈ M ∨ -a ∈ M

theorem Submonoid.IsMulSpanning.of_le {G : Type u_1} [Group G] {M N : Submonoid G} (hM : M.IsMulSpanning) (h : M ≤ N) :

N.IsMulSpanning

theorem AddSubmonoid.IsSpanning.of_le {G : Type u_1} [AddGroup G] {M N : AddSubmonoid G} (hM : M.IsSpanning) (h : M ≤ N) :

theorem Submonoid.IsMulSpanning.maximal_isMulPointed {G : Type u_1} [Group G] {M : Submonoid G} (hMp : M.IsMulPointed) (hMs : M.IsMulSpanning) :

Maximal IsMulPointed M

theorem AddSubmonoid.IsSpanning.maximal_isPointed {G : Type u_1} [AddGroup G] {M : AddSubmonoid G} (hMp : M.IsPointed) (hMs : M.IsSpanning) :

Maximal IsPointed M