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. When M ∪ -M = G, the support of M forms an ideal. We define supports and prove how they interact with operations.

Main definitions

• AddSubmonoid.supportAddSubgroup: the support of a submonoid as a subgroup.
• AddSubmonoid.support: the support of a submonoid as an ideal.
• AddSubmonoid.HasMemOrNegMem: typeclass for submonoids satisfying M ∪ -M = G.

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

Typeclass for submonoids M of a group G such that M ∪ -M = G.

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

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

Typeclass for submonoids M of a group G such that M ∪ -M = G.

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

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

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

def Submonoid.supportSubgroup {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.supportSubgroup = { carrier := ↑M ∩ (↑M)⁻¹, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

def AddSubmonoid.supportAddSubgroup {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.supportAddSubgroup = { carrier := ↑M ∩ -↑M, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

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

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

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

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

class AddSubmonoid.HasIdealSupport {R : Type u_1} [Ring R] (M : AddSubmonoid R) : Prop

Typeclass to track when the support of a submonoid forms an ideal.

• smul_mem_support (x : R) {a : R} (ha : a ∈ M.supportAddSubgroup) : x * a ∈ M.supportAddSubgroup

theorem AddSubmonoid.hasIdealSupport_iff {R : Type u_1} [Ring R] {M : AddSubmonoid R} : M.HasIdealSupport ↔ ∀ (x a : R), a ∈ M → -a ∈ M → x * a ∈ M ∧ -(x * a) ∈ M

theorem AddSubmonoid.smul_mem {R : Type u_1} [Ring R] (M : AddSubmonoid R) [M.HasIdealSupport] (x : R) {a : R} (h₁a : a ∈ M) (h₂a : -a ∈ M) : x * a ∈ M

theorem AddSubmonoid.neg_smul_mem {R : Type u_1} [Ring R] (M : AddSubmonoid R) [M.HasIdealSupport] (x : R) {a : R} (h₁a : a ∈ M) (h₂a : -a ∈ M) : -(x * a) ∈ M

def AddSubmonoid.support {R : Type u_1} [Ring R] (M : AddSubmonoid R) [M.HasIdealSupport] : Ideal R

The support M ∩ -M of a submonoid M of a ring R, as an ideal.

Equations

• M.support = { toAddSubmonoid := M.supportAddSubgroup.toAddSubmonoid, smul_mem' := ⋯ }

theorem AddSubmonoid.mem_support {R : Type u_1} [Ring R] {M : AddSubmonoid R} [M.HasIdealSupport] {x : R} : x ∈ M.support ↔ x ∈ M ∧ -x ∈ M

theorem AddSubmonoid.coe_support {R : Type u_1} [Ring R] (M : AddSubmonoid R) [M.HasIdealSupport] : ↑M.support = ↑M ∩ -↑M

@[simp]

theorem AddSubmonoid.supportAddSubgroup_eq {R : Type u_1} [Ring R] (M : AddSubmonoid R) [M.HasIdealSupport] : M.supportAddSubgroup = Submodule.toAddSubgroup M.support

instance Subsemiring.instHasIdealSupportToAddSubmonoidOfHasMemOrNegMem {R : Type u_1} [Ring R] (M : Subsemiring R) [M.toAddSubmonoid.HasMemOrNegMem] : M.toAddSubmonoid.HasIdealSupport

@[simp]

theorem Subsemiring.comap_toSubmonoid' {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (Q : Subsemiring S) : (comap f Q).toSubmonoid = Submonoid.comap (↑f) Q.toSubmonoid

@[simp]

theorem Subsemiring.comap_toAddSubmonoid {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (Q : Subsemiring S) : (comap f Q).toAddSubmonoid = AddSubmonoid.comap f.toAddMonoidHom Q.toAddSubmonoid

@[simp]

theorem Subsemiring.map_toSubmonoid' {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (P : Subsemiring R) : (map f P).toSubmonoid = Submonoid.map (↑f) P.toSubmonoid

@[simp]

theorem Subsemiring.map_toAddSubmonoid {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (P : Subsemiring R) : (map f P).toAddSubmonoid = AddSubmonoid.map f.toAddMonoidHom P.toAddSubmonoid

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Submonoid.supportSubgroup_sInf {G : Type u_1} [Group G] (s : Set (Submonoid G)) : (sInf s).supportSubgroup = sInf (supportSubgroup '' s)

@[simp]

theorem AddSubmonoid.supportAddSubgroup_sInf {G : Type u_1} [AddGroup G] (s : Set (AddSubmonoid G)) : (sInf s).supportAddSubgroup = sInf (supportAddSubgroup '' s)

instance Submonoid.instHasMemOrInvMemComapMonoidHom {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (M' : Submonoid H) [M'.HasMemOrInvMem] : (comap f M').HasMemOrInvMem

instance AddSubmonoid.instHasMemOrNegMemComapAddMonoidHom {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) (M' : AddSubmonoid H) [M'.HasMemOrNegMem] : (comap f M').HasMemOrNegMem

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem AddSubmonoid.support_mono {R : Type u_1} [Ring R] {M N : AddSubmonoid R} [M.HasIdealSupport] [N.HasIdealSupport] (h : M ≤ N) : M.support ≤ N.support

instance AddSubmonoid.instHasIdealSupportMin {R : Type u_1} [Ring R] (M N : AddSubmonoid R) [M.HasIdealSupport] [N.HasIdealSupport] : (M ⊓ N).HasIdealSupport

@[simp]

theorem AddSubmonoid.support_inf {R : Type u_1} [Ring R] (M N : AddSubmonoid R) [M.HasIdealSupport] [N.HasIdealSupport] : (M ⊓ N).support = M.support ⊓ N.support

theorem AddSubmonoid.HasIdealSupport.sInf {R : Type u_1} [Ring R] {s : Set (AddSubmonoid R)} (h : ∀ M ∈ s, M.HasIdealSupport) : (InfSet.sInf s).HasIdealSupport

@[simp]

theorem AddSubmonoid.support_sInf {R : Type u_1} [Ring R] {s : Set (AddSubmonoid R)} (h : ∀ M ∈ s, M.HasIdealSupport) : (sInf s).support = sInf {I : Ideal R | ∃ (M : AddSubmonoid R) (hM : M ∈ s), I = M.support}

@[simp]

theorem AddSubmonoid.supportAddSubgroup_sSup {R : Type u_1} [Ring R] {s : Set (AddSubmonoid R)} (hsn : s.Nonempty) (hsd : DirectedOn (fun (x1 x2 : AddSubmonoid R) => x1 ≤ x2) s) : (sSup s).supportAddSubgroup = sSup (supportAddSubgroup '' s)

theorem AddSubmonoid.HasIdealSupport.sSup {R : Type u_1} [Ring R] {s : Set (AddSubmonoid R)} (hsn : s.Nonempty) (hsd : DirectedOn (fun (x1 x2 : AddSubmonoid R) => x1 ≤ x2) s) (h : ∀ M ∈ s, M.HasIdealSupport) : (sSup s).HasIdealSupport

@[simp]

theorem AddSubmonoid.support_sSup {R : Type u_1} [Ring R] {s : Set (AddSubmonoid R)} (hsn : s.Nonempty) (hsd : DirectedOn (fun (x1 x2 : AddSubmonoid R) => x1 ≤ x2) s) (h : ∀ M ∈ s, M.HasIdealSupport) : (sSup s).support = sSup {I : Ideal R | ∃ (M : AddSubmonoid R) (hM : M ∈ s), I = M.support}

instance AddSubmonoid.instHasIdealSupportComapAddMonoidHomToAddMonoidHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (M' : AddSubmonoid S) [M'.HasIdealSupport] : (comap f.toAddMonoidHom M').HasIdealSupport

@[simp]

theorem AddSubmonoid.comap_support {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (M' : AddSubmonoid S) [M'.HasIdealSupport] : (comap f.toAddMonoidHom M').support = Ideal.comap f M'.support

theorem AddSubmonoid.HasIdealSupport.map {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {f : R →+* S} {M : AddSubmonoid R} [M.HasIdealSupport] (hf : Function.Surjective ⇑f) (hsupp : f.toAddMonoidHom.ker ≤ M.supportAddSubgroup) : (AddSubmonoid.map f.toAddMonoidHom M).HasIdealSupport

@[simp]

theorem AddSubmonoid.map_support {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {f : R →+* S} {M : AddSubmonoid R} [M.HasIdealSupport] (hf : Function.Surjective ⇑f) (hsupp : f.toAddMonoidHom.ker ≤ M.supportAddSubgroup) : (map f.toAddMonoidHom M).support = Ideal.map f M.support