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 M ∪ -M = G.

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

Main definitions

• AddSubmonoid.support: the support of a submonoid.
• AddSubmonoid.IsPointed: a submonoid with zero support.
• AddSubmonoid.IsSpanning: a submonoid satisfying M ∪ -M = G.

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

The support of a submonoid is the largest subgroup it contains.

theorem AddSubgroup.gc_toAddSubmonoid_support {G : Type u_1} [AddGroup G] : GaloisConnection toAddSubmonoid AddSubmonoid.support

The support of a submonoid is the largest subgroup it contains.

def Subgroup.gciToSubmonoidMulSupport {G : Type u_1} [Group G] : GaloisCoinsertion toSubmonoid Submonoid.mulSupport

The support of a submonoid is the largest subgroup it contains.

Equations

• Subgroup.gciToSubmonoidMulSupport = ⋯.toGaloisCoinsertion ⋯

def AddSubgroup.gciToAddSubmonoidSupport {G : Type u_1} [AddGroup G] : GaloisCoinsertion toAddSubmonoid AddSubmonoid.support

The support of a submonoid is the largest subgroup it contains.

Equations

• AddSubgroup.gciToAddSubmonoidSupport = ⋯.toGaloisCoinsertion ⋯

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

@[deprecated "Trivially true" (since := "2026-09-28")]

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

@[deprecated "Trivially true" (since := "2026-09-28")]

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

@[deprecated Submonoid.IsMulPointed.eq_one_of_mem_of_inv_mem (since := "2026-09-28")]

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.

@[deprecated AddSubmonoid.IsPointed.eq_zero_of_mem_of_neg_mem (since := "2026-09-28")]

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

Alias of AddSubmonoid.IsPointed.eq_zero_of_mem_of_neg_mem.

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 = ⊥

Alias of the forward direction of isPointed_iff_support_eq_bot.

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

Alias of the reverse direction of isPointed_iff_support_eq_bot.

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

@[deprecated "Trivially true" (since := "2026-09-28")]

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

@[deprecated "Trivially true" (since := "2026-09-28")]

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

@[simp]

theorem Subgroup.mulSupport_eq {G : Type u_1} [Group G] (H : Subgroup G) : H.mulSupport = H

@[simp]

theorem AddSubgroup.support_eq {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.support = H

@[simp]

theorem Submonoid.mulSupport_bot {G : Type u_1} [Group G] : ⊥.mulSupport = ⊥

@[simp]

theorem AddSubmonoid.support_bot {G : Type u_1} [AddGroup G] : ⊥.support = ⊥

@[simp]

theorem Submonoid.mulSupport_top {G : Type u_1} [Group G] : ⊤.mulSupport = ⊤

@[simp]

theorem AddSubmonoid.support_top {G : Type u_1} [AddGroup G] : ⊤.support = ⊤

theorem Submonoid.mulSupport_mono {G : Type u_1} [Group G] {M N : Submonoid G} (h : M ≤ N) : M.mulSupport ≤ N.mulSupport

theorem AddSubmonoid.support_mono {G : Type u_1} [AddGroup G] {M N : AddSubmonoid G} (h : M ≤ N) : M.support ≤ N.support

@[simp]

theorem Submonoid.mulSupport_inf {G : Type u_1} [Group G] (M N : Submonoid G) : (M ⊓ N).mulSupport = M.mulSupport ⊓ N.mulSupport

@[simp]

theorem AddSubmonoid.support_inf {G : Type u_1} [AddGroup G] (M N : AddSubmonoid G) : (M ⊓ N).support = M.support ⊓ N.support

@[simp]

theorem Submonoid.mulSupport_sInf {G : Type u_1} [Group G] (s : Set (Submonoid G)) : (sInf s).mulSupport = ⨅ M ∈ s, M.mulSupport

@[simp]

theorem AddSubmonoid.support_sInf {G : Type u_1} [AddGroup G] (s : Set (AddSubmonoid G)) : (sInf s).support = ⨅ M ∈ s, M.support

@[simp]

theorem Submonoid.mulSupport_iInf {G : Type u_1} [Group G] {ι : Type u_3} (f : ι → Submonoid G) : (iInf f).mulSupport = ⨅ (i : ι), (f i).mulSupport

@[simp]

theorem AddSubmonoid.support_iInf {G : Type u_1} [AddGroup G] {ι : Type u_3} (f : ι → AddSubmonoid G) : (iInf f).support = ⨅ (i : ι), (f i).support

theorem Submonoid.IsMulSpanning.comap {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) {M' : Submonoid H} (hM' : M'.IsMulSpanning) : (Submonoid.comap f M').IsMulSpanning

theorem AddSubmonoid.IsSpanning.comap {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (f : G →+ H) {M' : AddSubmonoid H} (hM' : M'.IsSpanning) : (AddSubmonoid.comap f M').IsSpanning

@[simp]

theorem Submonoid.mulSupport_comap {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) (M' : Submonoid H) : (comap f M').mulSupport = Subgroup.comap f M'.mulSupport

@[simp]

theorem AddSubmonoid.support_comap {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (f : G →+ H) (M' : AddSubmonoid H) : (comap f M').support = AddSubgroup.comap f M'.support

theorem Submonoid.IsMulSpanning.map {G : Type u_1} [Group G] {H : Type u_2} [Group H] {f : G →* H} {M : Submonoid G} (hM : M.IsMulSpanning) (hf : Function.Surjective ⇑f) : (Submonoid.map f M).IsMulSpanning

theorem AddSubmonoid.IsSpanning.map {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] {f : G →+ H} {M : AddSubmonoid G} (hM : M.IsSpanning) (hf : Function.Surjective ⇑f) : (AddSubmonoid.map f M).IsSpanning

theorem Submonoid.map_mulSupport_le {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) (M : Submonoid G) : Subgroup.map f M.mulSupport ≤ (map f M).mulSupport

theorem AddSubmonoid.map_support_le {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (f : G →+ H) (M : AddSubmonoid G) : AddSubgroup.map f M.support ≤ (map f M).support

theorem Submonoid.mulSupport_map {G : Type u_1} [Group G] {H : Type u_2} [Group H] {f : G →* H} {M : Submonoid G} (hsupp : f.ker ≤ M.mulSupport) : (map f M).mulSupport = Subgroup.map f M.mulSupport

theorem AddSubmonoid.support_map {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] {f : G →+ H} {M : AddSubmonoid G} (hsupp : f.ker ≤ M.support) : (map f M).support = AddSubgroup.map f M.support