Saturation of a submonoid

We define a submonoid s to be saturated if x * y ∈ s → x ∈ s ∧ y ∈ s. The type of all saturated submonoids forms a complete lattice. For a given submonoid s we construct the saturation of s as the smallest saturated submonoid containing s, which when the underlying type is a commutative monoid, is given by the formula {x : M | ∃ y : M, x * y ∈ s}.

Saturated submonoids are used in the context of localisations.

We also define the type of saturated submonoids, and endow on it the structure of a complete lattice.

Main Definitions

• Submonoid.MulSaturated: the condition x * y ∈ s ↔ x ∈ s ∧ y ∈ s. Not to be confused with Submonoid.PowSaturated.
• SaturatedSubmonoid: the type of Submonoid satisfying MulSaturated. It is a complete lattice.
• Submonoid.saturation: the smallest saturated submonoid containing a given submonoid.

def Submonoid.MulSaturated {M : Type u_1} [MulOneClass M] (s : Submonoid M) : Prop

Given a submonoid s of M, we say that s is saturated if it satisfies x * y ∈ s → x ∈ s ∧ y ∈ s.

It is called MulSaturated here to be distinguished from Submonoid.PowSaturated or AddSubmonoid.NSMulSaturated, which is also called "saturated" in the literature.

def AddSubmonoid.AddSaturated {M : Type u_1} [AddZeroClass M] (s : AddSubmonoid M) : Prop

Given an additive submonoid s of M, we say that s is saturated if it satisfies x + y ∈ s → x ∈ s ∧ y ∈ s.

It is called AddSaturated here to be distinguished from Submonoid.PowSaturated or AddSubmonoid.NSMulSaturated, which is also called "saturated" in the literature.

theorem Submonoid.MulSaturated.mul_mem_iff {M : Type u_1} [MulOneClass M] {s : Submonoid M} (h : s.MulSaturated) {x y : M} : x * y ∈ s ↔ x ∈ s ∧ y ∈ s

theorem AddSubmonoid.AddSaturated.add_mem_iff {M : Type u_1} [AddZeroClass M] {s : AddSubmonoid M} (h : s.AddSaturated) {x y : M} : x + y ∈ s ↔ x ∈ s ∧ y ∈ s

theorem Submonoid.MulSaturated.top {M : Type u_1} [MulOneClass M] : ⊤.MulSaturated

theorem AddSubmonoid.AddSaturated.top {M : Type u_1} [AddZeroClass M] : ⊤.AddSaturated

theorem Submonoid.MulSaturated.inf {M : Type u_1} [MulOneClass M] {s₁ s₂ : Submonoid M} (h₁ : s₁.MulSaturated) (h₂ : s₂.MulSaturated) : (s₁ ⊓ s₂).MulSaturated

theorem AddSubmonoid.AddSaturated.inf {M : Type u_1} [AddZeroClass M] {s₁ s₂ : AddSubmonoid M} (h₁ : s₁.AddSaturated) (h₂ : s₂.AddSaturated) : (s₁ ⊓ s₂).AddSaturated

theorem Submonoid.MulSaturated.sInf {M : Type u_1} [MulOneClass M] {f : Set (Submonoid M)} (hf : ∀ s ∈ f, s.MulSaturated) : (InfSet.sInf f).MulSaturated

theorem AddSubmonoid.AddSaturated.sInf {M : Type u_1} [AddZeroClass M] {f : Set (AddSubmonoid M)} (hf : ∀ s ∈ f, s.AddSaturated) : (InfSet.sInf f).AddSaturated

theorem Submonoid.MulSaturated.iInf {M : Type u_1} [MulOneClass M] {ι : Sort u_2} {f : ι → Submonoid M} (hf : ∀ (i : ι), (f i).MulSaturated) : (_root_.iInf f).MulSaturated

theorem AddSubmonoid.AddSaturated.iInf {M : Type u_1} [AddZeroClass M] {ι : Sort u_2} {f : ι → AddSubmonoid M} (hf : ∀ (i : ι), (f i).AddSaturated) : (_root_.iInf f).AddSaturated

theorem Submonoid.MulSaturated.of_left {M : Type u_2} [CommMonoid M] {s : Submonoid M} (h : ∀ ⦃x y : M⦄, x * y ∈ s → x ∈ s) : s.MulSaturated

If M is commutative, we only need to check the left condition x ∈ s.

theorem AddSubmonoid.AddSaturated.of_left {M : Type u_2} [AddCommMonoid M] {s : AddSubmonoid M} (h : ∀ ⦃x y : M⦄, x + y ∈ s → x ∈ s) : s.AddSaturated

If M is commutative, we only need to check the left condition x ∈ s.

theorem Submonoid.MulSaturated.of_right {M : Type u_2} [CommMonoid M] {s : Submonoid M} (h : ∀ ⦃x y : M⦄, x * y ∈ s → y ∈ s) : s.MulSaturated

If M is commutative, we only need to check the right condition y ∈ s.

theorem AddSubmonoid.AddSaturated.of_right {M : Type u_2} [AddCommMonoid M] {s : AddSubmonoid M} (h : ∀ ⦃x y : M⦄, x + y ∈ s → y ∈ s) : s.AddSaturated

If M is commutative, we only need to check the right condition y ∈ s.

structure SaturatedAddSubmonoid (M : Type u_1) [AddZeroClass M] extends AddSubmonoid M : Type u_1

A saturated additive submonoid is a submonoid s that satisfies x + y ∈ s → x ∈ s ∧ y ∈ s.

• carrier : Set M
• add_mem' {a b : M} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• addSaturated : self.AddSaturated

structure SaturatedSubmonoid (M : Type u_1) [MulOneClass M] extends Submonoid M : Type u_1

A saturated submonoid is a submonoid s that satisfies x * y ∈ s → x ∈ s ∧ y ∈ s.

• carrier : Set M
• mul_mem' {a b : M} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• mulSaturated : self.MulSaturated

theorem SaturatedSubmonoid.toSubmonoid_injective {M : Type u_1} [MulOneClass M] : Function.Injective toSubmonoid

theorem SaturatedAddSubmonoid.toAddSubmonoid_injective {M : Type u_1} [AddZeroClass M] : Function.Injective toAddSubmonoid

theorem SaturatedSubmonoid.ext {M : Type u_1} [MulOneClass M] {s₁ s₂ : SaturatedSubmonoid M} (h : s₁.toSubmonoid = s₂.toSubmonoid) : s₁ = s₂

theorem SaturatedAddSubmonoid.ext {M : Type u_1} [AddZeroClass M] {s₁ s₂ : SaturatedAddSubmonoid M} (h : s₁.toAddSubmonoid = s₂.toAddSubmonoid) : s₁ = s₂

theorem SaturatedAddSubmonoid.ext_iff {M : Type u_1} [AddZeroClass M] {s₁ s₂ : SaturatedAddSubmonoid M} : s₁ = s₂ ↔ s₁.toAddSubmonoid = s₂.toAddSubmonoid

theorem SaturatedSubmonoid.ext_iff {M : Type u_1} [MulOneClass M] {s₁ s₂ : SaturatedSubmonoid M} : s₁ = s₂ ↔ s₁.toSubmonoid = s₂.toSubmonoid

@[implicit_reducible]

instance SaturatedSubmonoid.instSetLike (M : Type u_1) [MulOneClass M] : SetLike (SaturatedSubmonoid M) M

@[implicit_reducible]

instance SaturatedAddSubmonoid.instSetLike (M : Type u_1) [AddZeroClass M] : SetLike (SaturatedAddSubmonoid M) M

@[implicit_reducible]

instance SaturatedSubmonoid.instPartialOrder {M : Type u_1} [MulOneClass M] : PartialOrder (SaturatedSubmonoid M)

@[implicit_reducible]

instance SaturatedAddSubmonoid.instPartialOrder {M : Type u_1} [AddZeroClass M] : PartialOrder (SaturatedAddSubmonoid M)

theorem SaturatedSubmonoid.ext' {M : Type u_1} [MulOneClass M] {s₁ s₂ : SaturatedSubmonoid M} (h : ∀ (x : M), x ∈ s₁ ↔ x ∈ s₂) : s₁ = s₂

theorem SaturatedAddSubmonoid.ext' {M : Type u_1} [AddZeroClass M] {s₁ s₂ : SaturatedAddSubmonoid M} (h : ∀ (x : M), x ∈ s₁ ↔ x ∈ s₂) : s₁ = s₂

instance SaturatedSubmonoid.instSubmonoidClass (M : Type u_1) [MulOneClass M] : SubmonoidClass (SaturatedSubmonoid M) M

instance SaturatedAddSubmonoid.instAddSubmonoidClass (M : Type u_1) [AddZeroClass M] : AddSubmonoidClass (SaturatedAddSubmonoid M) M

@[simp]

theorem SaturatedSubmonoid.mem_toSubmonoid {M : Type u_1} [MulOneClass M] {s : SaturatedSubmonoid M} {x : M} : x ∈ s.toSubmonoid ↔ x ∈ s

@[simp]

theorem SaturatedAddSubmonoid.mem_toAddSubmonoid {M : Type u_1} [AddZeroClass M] {s : SaturatedAddSubmonoid M} {x : M} : x ∈ s.toAddSubmonoid ↔ x ∈ s

@[implicit_reducible]

instance SaturatedSubmonoid.instTop {M : Type u_1} [MulOneClass M] : Top (SaturatedSubmonoid M)

@[implicit_reducible]

instance SaturatedAddSubmonoid.instTop {M : Type u_1} [AddZeroClass M] : Top (SaturatedAddSubmonoid M)

@[simp]

theorem SaturatedSubmonoid.mem_top {M : Type u_1} [MulOneClass M] {x : M} : x ∈ ⊤

@[simp]

theorem SaturatedAddSubmonoid.mem_top {M : Type u_1} [AddZeroClass M] {x : M} : x ∈ ⊤

@[implicit_reducible]

instance SaturatedSubmonoid.instMin (M : Type u_1) [MulOneClass M] : Min (SaturatedSubmonoid M)

@[implicit_reducible]

instance SaturatedAddSubmonoid.instMin (M : Type u_1) [AddZeroClass M] : Min (SaturatedAddSubmonoid M)

@[implicit_reducible]

instance SaturatedSubmonoid.instInfSet (M : Type u_1) [MulOneClass M] : InfSet (SaturatedSubmonoid M)

@[implicit_reducible]

instance SaturatedAddSubmonoid.instInfSet (M : Type u_1) [AddZeroClass M] : InfSet (SaturatedAddSubmonoid M)

theorem SaturatedSubmonoid.mem_sInf {M : Type u_1} [MulOneClass M] {f : Set (SaturatedSubmonoid M)} {x : M} : x ∈ sInf f ↔ ∀ s ∈ f, x ∈ s

theorem SaturatedAddSubmonoid.mem_sInf {M : Type u_1} [AddZeroClass M] {f : Set (SaturatedAddSubmonoid M)} {x : M} : x ∈ sInf f ↔ ∀ s ∈ f, x ∈ s

@[implicit_reducible]

instance SaturatedSubmonoid.instCompleteSemilatticeInf (M : Type u_1) [MulOneClass M] : CompleteSemilatticeInf (SaturatedSubmonoid M)

@[implicit_reducible]

instance SaturatedAddSubmonoid.instCompleteSemilatticeInf (M : Type u_1) [AddZeroClass M] : CompleteSemilatticeInf (SaturatedAddSubmonoid M)

def Submonoid.saturation {M : Type u_1} [MulOneClass M] (s : Submonoid M) : SaturatedSubmonoid M

The saturation of a submonoid s is the intersection of all saturated submonoids that contain s.

If M is a commutative monoid, then this is {x : M | ∃ y : M, x * y ∈ s}.

def AddSubmonoid.saturation {M : Type u_1} [AddZeroClass M] (s : AddSubmonoid M) : SaturatedAddSubmonoid M

The saturation of an additive submonoid s is the intersection of all saturated submonoids that contain s.

If M is a commutative additive monoid, then this is {x : M | ∃ y : M, x + y ∈ s}.

theorem Submonoid.gc_saturation (M : Type u_1) [MulOneClass M] : GaloisConnection saturation fun (x : SaturatedSubmonoid M) => x.toSubmonoid

theorem AddSubmonoid.gc_saturation (M : Type u_1) [AddZeroClass M] : GaloisConnection saturation fun (x : SaturatedAddSubmonoid M) => x.toAddSubmonoid

def Submonoid.giSaturation (M : Type u_1) [MulOneClass M] : GaloisInsertion saturation fun (x : SaturatedSubmonoid M) => x.toSubmonoid

saturation forms a GaloisInsertion with the forgetful functor SaturatedSubmonoid.toSubmonoid.

def AddSubmonoid.giSaturation (M : Type u_1) [AddZeroClass M] : GaloisInsertion saturation fun (x : SaturatedAddSubmonoid M) => x.toAddSubmonoid

saturation forms a GaloisInsertion with the forgetful functor SaturatedAddSubmonoid.toAddSubmonoid.

theorem Submonoid.saturation_le_iff_le {M : Type u_1} [MulOneClass M] {a : Submonoid M} {b : SaturatedSubmonoid M} : a.saturation ≤ b ↔ a ≤ b.toSubmonoid

theorem AddSubmonoid.saturation_le_iff_le {M : Type u_1} [AddZeroClass M] {a : AddSubmonoid M} {b : SaturatedAddSubmonoid M} : a.saturation ≤ b ↔ a ≤ b.toAddSubmonoid

theorem Submonoid.saturation_le_of_le {M : Type u_1} [MulOneClass M] {a : Submonoid M} {b : SaturatedSubmonoid M} : a ≤ b.toSubmonoid → a.saturation ≤ b

Alias of the reverse direction of Submonoid.saturation_le_iff_le.

theorem AddSubmonoid.saturation_le_of_le {M : Type u_1} [AddZeroClass M] {a : AddSubmonoid M} {b : SaturatedAddSubmonoid M} : a ≤ b.toAddSubmonoid → a.saturation ≤ b

theorem Submonoid.le_toSubmonoid_saturation {M : Type u_1} [MulOneClass M] {a : Submonoid M} : a ≤ a.saturation.toSubmonoid

theorem AddSubmonoid.le_toAddSubmonoid_saturation {M : Type u_1} [AddZeroClass M] {a : AddSubmonoid M} : a ≤ a.saturation.toAddSubmonoid

@[simp]

theorem Submonoid.saturation_toSubmonoid {M : Type u_1} [MulOneClass M] {b : SaturatedSubmonoid M} : b.saturation = b

@[simp]

theorem AddSubmonoid.saturation_toAddSubmonoid {M : Type u_1} [AddZeroClass M] {b : SaturatedAddSubmonoid M} : b.saturation = b

theorem Submonoid.saturation_induction {M : Type u_1} [MulOneClass M] {s : Submonoid M} {p : (x : M) → x ∈ s.saturation → Prop} (mem : ∀ (x : M) (hx : x ∈ s), p x ⋯) (mul : ∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x * y) ⋯) (of_mul : ∀ (x y : M) (hxy : x * y ∈ s.saturation), p (x * y) hxy → p x ⋯ ∧ p y ⋯) {x : M} (hx : x ∈ s.saturation) : p x hx

theorem AddSubmonoid.saturation_induction {M : Type u_1} [AddZeroClass M] {s : AddSubmonoid M} {p : (x : M) → x ∈ s.saturation → Prop} (mem : ∀ (x : M) (hx : x ∈ s), p x ⋯) (add : ∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x + y) ⋯) (of_add : ∀ (x y : M) (hxy : x + y ∈ s.saturation), p (x + y) hxy → p x ⋯ ∧ p y ⋯) {x : M} (hx : x ∈ s.saturation) : p x hx

theorem Submonoid.mem_saturation_iff {M : Type u_1} [CommMonoid M] {s : Submonoid M} {x : M} : x ∈ s.saturation ↔ ∃ (y : M), x * y ∈ s

theorem AddSubmonoid.mem_saturation_iff {M : Type u_1} [AddCommMonoid M] {s : AddSubmonoid M} {x : M} : x ∈ s.saturation ↔ ∃ (y : M), x + y ∈ s

theorem Submonoid.mem_saturation_iff' {M : Type u_1} [CommMonoid M] {s : Submonoid M} {x : M} : x ∈ s.saturation ↔ ∃ (y : M), y * x ∈ s

theorem AddSubmonoid.mem_saturation_iff' {M : Type u_1} [AddCommMonoid M] {s : AddSubmonoid M} {x : M} : x ∈ s.saturation ↔ ∃ (y : M), y + x ∈ s

theorem Submonoid.mem_saturation_iff_exists_dvd {M : Type u_1} [CommMonoid M] {s : Submonoid M} {x : M} : x ∈ s.saturation ↔ ∃ m ∈ s, x ∣ m

@[implicit_reducible]

instance SaturatedSubmonoid.instCompleteLattice (M : Type u_1) [MulOneClass M] : CompleteLattice (SaturatedSubmonoid M)

@[implicit_reducible]

instance SaturatedAddSubmonoid.instCompleteLattice (M : Type u_1) [AddZeroClass M] : CompleteLattice (SaturatedAddSubmonoid M)

theorem SaturatedSubmonoid.bot_def {M : Type u_1} [MulOneClass M] : ⊥ = ⊥.saturation

theorem SaturatedAddSubmonoid.bot_def {M : Type u_1} [AddZeroClass M] : ⊥ = ⊥.saturation

theorem SaturatedSubmonoid.sup_def {M : Type u_1} [MulOneClass M] {s₁ s₂ : SaturatedSubmonoid M} : s₁ ⊔ s₂ = (s₁.toSubmonoid ⊔ s₂.toSubmonoid).saturation

theorem SaturatedAddSubmonoid.sup_def {M : Type u_1} [AddZeroClass M] {s₁ s₂ : SaturatedAddSubmonoid M} : s₁ ⊔ s₂ = (s₁.toAddSubmonoid ⊔ s₂.toAddSubmonoid).saturation

theorem SaturatedSubmonoid.sSup_def {M : Type u_1} [MulOneClass M] {f : Set (SaturatedSubmonoid M)} : sSup f = (sSup (toSubmonoid '' f)).saturation

theorem SaturatedAddSubmonoid.sSup_def {M : Type u_1} [AddZeroClass M] {f : Set (SaturatedAddSubmonoid M)} : sSup f = (sSup (toAddSubmonoid '' f)).saturation

theorem SaturatedSubmonoid.iSup_def {M : Type u_1} [MulOneClass M] {ι : Sort u_2} {f : ι → SaturatedSubmonoid M} : iSup f = (⨆ (i : ι), (f i).toSubmonoid).saturation

theorem SaturatedAddSubmonoid.iSup_def {M : Type u_1} [AddZeroClass M] {ι : Sort u_2} {f : ι → SaturatedAddSubmonoid M} : iSup f = (⨆ (i : ι), (f i).toAddSubmonoid).saturation

theorem SaturatedSubmonoid.mem_bot_iff {M : Type u_1} [CommMonoid M] {x : M} : x ∈ ⊥ ↔ IsUnit x

theorem SaturatedAddSubmonoid.mem_bot_iff {M : Type u_1} [AddCommMonoid M] {x : M} : x ∈ ⊥ ↔ IsAddUnit x

@[simp]

theorem Submonoid.saturation_bot {M : Type u_1} [MulOneClass M] : ⊥.saturation = ⊥

@[simp]

theorem AddSubmonoid.saturation_bot {M : Type u_1} [AddZeroClass M] : ⊥.saturation = ⊥

@[simp]

theorem Submonoid.saturation_top {M : Type u_1} [MulOneClass M] : ⊤.saturation = ⊤

@[simp]

theorem AddSubmonoid.saturation_top {M : Type u_1} [AddZeroClass M] : ⊤.saturation = ⊤

@[simp]

theorem Submonoid.saturation_sup {M : Type u_1} [MulOneClass M] {s₁ s₂ : Submonoid M} : (s₁ ⊔ s₂).saturation = s₁.saturation ⊔ s₂.saturation

@[simp]

theorem AddSubmonoid.saturation_sup {M : Type u_1} [AddZeroClass M] {s₁ s₂ : AddSubmonoid M} : (s₁ ⊔ s₂).saturation = s₁.saturation ⊔ s₂.saturation

@[simp]

theorem Submonoid.saturation_sSup {M : Type u_1} [MulOneClass M] {f : Set (Submonoid M)} : (sSup f).saturation = ⨆ s ∈ f, s.saturation

@[simp]

theorem AddSubmonoid.saturation_sSup {M : Type u_1} [AddZeroClass M] {f : Set (AddSubmonoid M)} : (sSup f).saturation = ⨆ s ∈ f, s.saturation

@[simp]

theorem Submonoid.saturation_iSup {M : Type u_1} [MulOneClass M] {ι : Sort u_2} {f : ι → Submonoid M} : (iSup f).saturation = ⨆ (i : ι), (f i).saturation

@[simp]

theorem AddSubmonoid.saturation_iSup {M : Type u_1} [AddZeroClass M] {ι : Sort u_2} {f : ι → AddSubmonoid M} : (iSup f).saturation = ⨆ (i : ι), (f i).saturation