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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem Submonoid.comap_mulSupport {G : Type u_2} {H : Type u_3} [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_2} {H : Type u_3} [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_2} {H : Type u_3} [Group G] [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_2} {H : Type u_3} [AddGroup G] [AddGroup H] {f : G →+ H} {M : AddSubmonoid G} (hM : M.IsSpanning) (hf : Function.Surjective ⇑f) : (AddSubmonoid.map f M).IsSpanning

@[simp]

theorem Submonoid.map_mulSupport {G : Type u_2} {H : Type u_3} [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_2} {H : Type u_3} [AddCommGroup G] [AddCommGroup H] {f : G →+ H} {M : AddSubmonoid G} (hsupp : f.ker ≤ M.support) : (map f M).support = AddSubgroup.map f M.support

theorem Submonoid.oneLE.isMulPointed (G : Type u_1) [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] : (oneLE G).IsMulPointed

theorem AddSubmonoid.nonneg.isAddPointed (G : Type u_1) [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] : (nonneg G).IsPointed

theorem Submonoid.oneLE.isMulSpanning (G : Type u_1) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] : (oneLE G).IsMulSpanning

theorem AddSubmonoid.nonneg.isAddSpanning (G : Type u_1) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] : (nonneg G).IsSpanning

@[reducible, inline]

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

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

Equations

• PartialOrder.mkOfSubmonoid hM = { 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} (hM : M.IsPointed) : PartialOrder G

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

Equations

• PartialOrder.mkOfAddSubmonoid hM = { 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} {hM : 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} {hM : M.IsPointed} {a b : G} : a ≤ b ↔ b - a ∈ M

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

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

@[reducible, inline]

abbrev LinearOrder.mkOfSubmonoid {G : Type u_1} [CommGroup G] {M : Submonoid G} (hM : M.IsMulPointed) (hMs : 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} (hM : M.IsPointed) (hMs : 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 h

@[simp]

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

@[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⟩) = LinearOrder.mkOfSubmonoid ⋯ ⋯

@[simp]

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

@[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