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) : Subgroup G

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

Equations

• M.mulSupport = { toSubmonoid := M ⊓ M⁻¹, inv_mem' := ⋯ }

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

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

Equations

• M.support = { toAddSubmonoid := M ⊓ -M, neg_mem' := ⋯ }

@[simp]

theorem AddSubmonoid.coe_support {G : Type u_1} [AddGroup G] (M : AddSubmonoid G) : ↑M.support = ↑M ∩ -↑M

@[simp]

theorem Submonoid.coe_mulSupport {G : Type u_1} [Group G] (M : Submonoid G) : ↑M.mulSupport = ↑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) : Prop

A submonoid is pointed if it has zero support.

Equations

• M.IsMulPointed = ∀ x ∈ M, x⁻¹ ∈ M → x = 1

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

A submonoid is pointed if it has zero support.

Equations

• M.IsPointed = ∀ x ∈ M, -x ∈ M → x = 0

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

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

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) : Prop

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

Equations

• M.IsMulSpanning = ∀ (a : G), a ∈ M ∨ a⁻¹ ∈ M

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

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

Equations

• M.IsSpanning = ∀ (a : G), a ∈ M ∨ -a ∈ M

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) : M.IsSpanning

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) : N.IsSpanning

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