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 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.

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

Typeclass for submonoids of a group with zero support.

• eq_zero_of_mem_of_neg_mem {x : G} (hx₁ : x ∈ M) (hx₂ : -x ∈ M) : x = 0

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

Typeclass for submonoids M of a group G such that M generates G as a subgroup.

• mem_or_neg_mem (a : G) : a ∈ M ∨ -a ∈ M

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 contained in M.

Equations

• M.mulSupport = { carrier := ↑M ∩ (↑M)⁻¹, mul_mem' := ⋯, one_mem' := ⋯, 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 contained in M.

Equations

• M.support = { carrier := ↑M ∩ -↑M, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem Submonoid.mem_mulSupport {G : Type u_1} [Group G] {M : Submonoid G} {x : G} : x ∈ M.mulSupport ↔ x ∈ M ∧ x⁻¹ ∈ M

theorem AddSubmonoid.mem_support {G : Type u_1} [AddGroup G] {M : AddSubmonoid G} {x : G} : x ∈ M.support ↔ x ∈ M ∧ -x ∈ M

theorem Submonoid.coe_mulSupport {G : Type u_1} [Group G] (M : Submonoid G) : ↑M.mulSupport = ↑M ∩ (↑M)⁻¹

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

class Submonoid.IsMulPointed {G : Type u_2} [Group G] (M : Submonoid G) : Prop

Typeclass for submonoids of a group with zero support.

• eq_one_of_mem_of_inv_mem {x : G} (hx₁ : x ∈ M) (hx₂ : x⁻¹ ∈ M) : x = 1

theorem Submonoid.eq_one_of_mem_of_inv_mem₂ {G : Type u_2} {inst✝ : Group G} {M : Submonoid G} [self : 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.eq_zero_of_mem_of_neg_mem₂ {G : Type u_2} {inst✝ : AddGroup G} {M : AddSubmonoid G} [self : M.IsPointed] {x : G} (hx₁ : x ∈ M) (hx₂ : -x ∈ M) : x = 0

@[simp]

theorem Submonoid.mulSupport_eq_bot {G : Type u_2} [Group G] (M : Submonoid G) [M.IsMulPointed] : M.mulSupport = ⊥

@[simp]

theorem AddSubmonoid.support_eq_bot {G : Type u_2} [AddGroup G] (M : AddSubmonoid G) [M.IsPointed] : M.support = ⊥

theorem Submonoid.IsMulPointed.of_mulSupport_eq_bot {G : Type u_2} [Group G] (M : Submonoid G) (h : M.mulSupport = ⊥) : M.IsMulPointed

theorem AddSubmonoid.IsPointed.of_support_eq_bot {G : Type u_2} [AddGroup G] (M : AddSubmonoid G) (h : M.support = ⊥) : M.IsPointed

class Submonoid.IsMulSpanning {G : Type u_3} [Group G] (M : Submonoid G) : Prop

Typeclass for submonoids M of a group G such that M generates G as a subgroup.

• mem_or_inv_mem (a : G) : a ∈ M ∨ a⁻¹ ∈ M

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

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

theorem Submonoid.IsMulSpanning.maximal_isMulPointed {G : Type u_2} [Group G] (M : Submonoid G) [M.IsMulPointed] [M.IsMulSpanning] : Maximal IsMulPointed M

theorem AddSubmonoid.IsSpanning.maximal_isPointed {G : Type u_2} [AddGroup G] (M : AddSubmonoid G) [M.IsPointed] [M.IsSpanning] : Maximal IsPointed M

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Submonoid.mulSupport_sInf {G : Type u_3} [Group G] (s : Set (Submonoid G)) : (sInf s).mulSupport = sInf (mulSupport '' s)

@[simp]

theorem AddSubmonoid.support_sInf {G : Type u_3} [AddGroup G] (s : Set (AddSubmonoid G)) : (sInf s).support = sInf (support '' s)

instance Submonoid.instIsMulSpanningComapMonoidHom {G : Type u_3} {H : Type u_4} [Group G] [Group H] (f : G →* H) (M' : Submonoid H) [M'.IsMulSpanning] : (comap f M').IsMulSpanning

instance AddSubmonoid.instIsAddSpanningComapAddMonoidHom {G : Type u_3} {H : Type u_4} [AddGroup G] [AddGroup H] (f : G →+ H) (M' : AddSubmonoid H) [M'.IsSpanning] : (comap f M').IsSpanning

@[simp]

theorem Submonoid.comap_mulSupport {G : Type u_3} {H : Type u_4} [Group G] [Group H] (f : G →* H) (M' : Submonoid H) : (comap f M').mulSupport = Subgroup.comap f M'.mulSupport

@[simp]

theorem AddSubmonoid.comap_support {G : Type u_3} {H : Type u_4} [AddGroup G] [AddGroup H] (f : G →+ H) (M' : AddSubmonoid H) : (comap f M').support = AddSubgroup.comap f M'.support

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

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

@[simp]

theorem Submonoid.map_mulSupport {G : Type u_3} {H : Type u_4} [CommGroup G] [CommGroup H] {f : G →* H} {M : Submonoid G} (hsupp : f.ker ≤ M.mulSupport) : (map f M).mulSupport = Subgroup.map f M.mulSupport

@[simp]

theorem AddSubmonoid.map_support {G : Type u_3} {H : Type u_4} [AddCommGroup G] [AddCommGroup H] {f : G →+ H} {M : AddSubmonoid G} (hsupp : f.ker ≤ M.support) : (map f M).support = AddSubgroup.map f M.support

instance instIsMulPointedOneLE (G : Type u_1) [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] : (Submonoid.oneLE G).IsMulPointed

instance instIsAddPointedNonneg (G : Type u_1) [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] : (AddSubmonoid.nonneg G).IsPointed

instance instIsMulSpanningOneLE (G : Type u_1) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] : (Submonoid.oneLE G).IsMulSpanning

instance instIsAddSpanningNonneg (G : Type u_1) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] : (AddSubmonoid.nonneg G).IsSpanning

@[reducible, inline]

abbrev PartialOrder.mkOfSubmonoid {G : Type u_1} [CommGroup G] (M : Submonoid G) [M.IsMulPointed] : PartialOrder G

Construct a partial order by designating a submonoid with zero support in an abelian group.

Equations

• PartialOrder.mkOfSubmonoid M = { le := fun (a b : G) => b / a ∈ M, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[reducible, inline]

abbrev PartialOrder.mkOfAddSubmonoid {G : Type u_1} [AddCommGroup G] (M : AddSubmonoid G) [M.IsPointed] : PartialOrder G

Construct a partial order by designating a submonoid with zero support in an abelian group.

Equations

• PartialOrder.mkOfAddSubmonoid M = { le := fun (a b : G) => b - a ∈ M, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[simp]

theorem PartialOrder.mkOfSubmonoid_le_iff {G : Type u_1} [CommGroup G] {M : Submonoid G} [M.IsMulPointed] {a b : G} : a ≤ b ↔ b / a ∈ M

@[simp]

theorem PartialOrder.mkOfAddSubmonoid_le_iff {G : Type u_1} [AddCommGroup G] {M : AddSubmonoid G} [M.IsPointed] {a b : G} : a ≤ b ↔ b - a ∈ M

theorem IsOrderedMonoid.mkOfSubmonoid {G : Type u_1} [CommGroup G] (M : Submonoid G) [M.IsMulPointed] : IsOrderedMonoid G

theorem IsOrderedAddMonoid.mkOfAddSubmonoid {G : Type u_1} [AddCommGroup G] (M : AddSubmonoid G) [M.IsPointed] : IsOrderedAddMonoid G

@[reducible, inline]

abbrev LinearOrder.mkOfSubmonoid {G : Type u_1} [CommGroup G] (M : Submonoid G) [M.IsMulPointed] [M.IsMulSpanning] [DecidablePred fun (x : G) => x ∈ M] : LinearOrder G

Construct a linear order by designating a maximal submonoid with zero support in an abelian group.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LinearOrder.mkOfAddSubmonoid {G : Type u_1} [AddCommGroup G] (M : AddSubmonoid G) [M.IsPointed] [M.IsSpanning] [DecidablePred fun (x : G) => x ∈ M] : LinearOrder G

Construct a linear order by designating a maximal submonoid with zero support in an abelian group.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommGroup.submonoidPartialOrderEquiv (G : Type u_1) [CommGroup G] : { C : Submonoid G // C.IsMulPointed } ≃ { o : PartialOrder G // IsOrderedMonoid G }

Equivalence between submonoids with zero support in an abelian group G and partially ordered group structures on G.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddCommGroup.addSubmonoidPartialOrderEquiv (G : Type u_1) [AddCommGroup G] : { C : AddSubmonoid G // C.IsPointed } ≃ { o : PartialOrder G // IsOrderedAddMonoid G }

Equivalence between submonoids with zero support in an abelian group G and partially ordered group structures on G.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommGroup.submonoidPartialOrderEquiv_apply {G : Type u_1} [CommGroup G] (C : Submonoid G) (h : C.IsMulPointed) : ↑((submonoidPartialOrderEquiv G) ⟨C, h⟩) = PartialOrder.mkOfSubmonoid C

@[simp]

theorem AddCommGroup.addSubmonoidPartialOrderEquiv_apply {G : Type u_1} [AddCommGroup G] (C : AddSubmonoid G) (h : C.IsPointed) : ↑((addSubmonoidPartialOrderEquiv G) ⟨C, h⟩) = PartialOrder.mkOfAddSubmonoid C

@[simp]

theorem CommGroup.submonoidPartialOrderEquiv_symm_apply {G : Type u_1} [CommGroup G] (o : PartialOrder G) (h : IsOrderedMonoid G) : ↑((submonoidPartialOrderEquiv G).symm ⟨o, h⟩) = Submonoid.oneLE G

@[simp]

theorem AddCommGroup.addSubmonoidPartialOrderEquiv_symm_apply {G : Type u_1} [AddCommGroup G] (o : PartialOrder G) (h : IsOrderedAddMonoid G) : ↑((addSubmonoidPartialOrderEquiv G).symm ⟨o, h⟩) = AddSubmonoid.nonneg G

noncomputable def CommGroup.submonoidLinearOrderEquiv (G : Type u_1) [CommGroup G] : { C : Submonoid G // C.IsMulPointed ∧ C.IsMulSpanning } ≃ { o : LinearOrder G // IsOrderedMonoid G }

Equivalence between maximal submonoids with zero support in an abelian group G and linearly ordered group structures on G.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddCommGroup.addSubmonoidLinearOrderEquiv (G : Type u_1) [AddCommGroup G] : { C : AddSubmonoid G // C.IsPointed ∧ C.IsSpanning } ≃ { o : LinearOrder G // IsOrderedAddMonoid G }

Equivalence between maximal submonoids with zero support in an abelian group G and linearly ordered group structures on G.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CommGroup.submonoidLinearOrderEquiv_apply {G : Type u_1} [CommGroup G] (C : Submonoid G) (h : C.IsMulPointed ∧ C.IsMulSpanning) : ↑((submonoidLinearOrderEquiv G) ⟨C, h⟩) = have this := ⋯; have this_1 := ⋯; LinearOrder.mkOfSubmonoid C

@[simp]

theorem AddCommGroup.addSubmonoidLinearOrderEquiv_apply {G : Type u_1} [AddCommGroup G] (C : AddSubmonoid G) (h : C.IsPointed ∧ C.IsSpanning) : ↑((addSubmonoidLinearOrderEquiv G) ⟨C, h⟩) = have this := ⋯; have this_1 := ⋯; LinearOrder.mkOfAddSubmonoid C

@[simp]

theorem CommGroup.submonoidLinearOrderEquiv_symm_apply {G : Type u_1} [CommGroup G] (l : LinearOrder G) (h : IsOrderedMonoid G) : ↑((submonoidLinearOrderEquiv G).symm ⟨l, h⟩) = Submonoid.oneLE G

@[simp]

theorem AddCommGroup.addSubmonoidLinearOrderEquiv_symm_apply {G : Type u_1} [AddCommGroup G] (l : LinearOrder G) (h : IsOrderedAddMonoid G) : ↑((addSubmonoidLinearOrderEquiv G).symm ⟨l, h⟩) = AddSubmonoid.nonneg G