Absorption of sets

Let M act on α, let A and B be sets in α. We say that A absorbs B if for sufficiently large a : M, we have B ⊆ a • A. Formally, "for sufficiently large a : M" means "for all but a bounded set of a".

Traditionally, this definition is formulated for the action of a (semi)normed ring on a module over that ring.

We formulate it in a more general settings for two reasons:

• this way we don't have to depend on metric spaces, normed rings etc;
• some proofs look nicer with this definition than with something like ∃ r : ℝ, ∀ a : R, r ≤ ‖a‖ → B ⊆ a • A.

Implementation notes

For now, all theorems assume that we deal with (a generalization of) a module over a division ring. Some lemmas have multiplicative versions for MulDistribMulActions. They can be added later when someone needs them.

Keywords

absorbs, absorbent

def Absorbs (M : Type u_1) {α : Type u_2} [Bornology M] [SMul M α] (s : Set α) (t : Set α) : Prop

A set s absorbs another set t if t is contained in all scalings of s by all but a bounded set of elements.

Equations

• Absorbs M s t = ∀ᶠ (a : M) in Bornology.cobounded M, t ⊆ a • s

def Absorbent (M : Type u_1) {α : Type u_2} [Bornology M] [SMul M α] (s : Set α) : Prop

A set is absorbent if it absorbs every singleton.

Equations

• Absorbent M s = ∀ (x : α), Absorbs M s {x}

theorem Absorbs.empty {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} : Absorbs M s ∅

@[deprecated Absorbs.empty]

theorem absorbs_empty {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} : Absorbs M s ∅

Alias of Absorbs.empty.

theorem Absorbs.eventually {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t : Set α} (h : Absorbs M s t) : ∀ᶠ (a : M) in Bornology.cobounded M, t ⊆ a • s

@[simp]

theorem Absorbs.of_boundedSpace {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t : Set α} [BoundedSpace M] : Absorbs M s t

theorem Absorbs.mono_left {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s₁ : Set α} {s₂ : Set α} {t : Set α} (h : Absorbs M s₁ t) (hs : s₁ ⊆ s₂) : Absorbs M s₂ t

theorem Absorbs.mono_right {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t₁ : Set α} {t₂ : Set α} (h : Absorbs M s t₁) (ht : t₂ ⊆ t₁) : Absorbs M s t₂

theorem Absorbs.mono {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} (h : Absorbs M s₁ t₁) (hs : s₁ ⊆ s₂) (ht : t₂ ⊆ t₁) : Absorbs M s₂ t₂

@[simp]

theorem absorbs_union {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t₁ : Set α} {t₂ : Set α} : Absorbs M s (t₁ ∪ t₂) ↔ Absorbs M s t₁ ∧ Absorbs M s t₂

theorem Absorbs.union {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t₁ : Set α} {t₂ : Set α} (h₁ : Absorbs M s t₁) (h₂ : Absorbs M s t₂) : Absorbs M s (t₁ ∪ t₂)

theorem Set.Finite.absorbs_sUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {T : Set (Set α)} (hT : T.Finite) : Absorbs M s (⋃₀ T) ↔ ∀ t ∈ T, Absorbs M s t

theorem Absorbs.sUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {T : Set (Set α)} (hT : T.Finite) (hs : ∀ t ∈ T, Absorbs M s t) : Absorbs M s (⋃₀ T)

@[simp]

theorem absorbs_iUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Sort u_3} [Finite ι] {t : ι → Set α} : Absorbs M s (⋃ (i : ι), t i) ↔ ∀ (i : ι), Absorbs M s (t i)

theorem Absorbs.iUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Sort u_3} [Finite ι] {t : ι → Set α} : (∀ (i : ι), Absorbs M s (t i)) → Absorbs M s (⋃ (i : ι), t i)

Alias of the reverse direction of absorbs_iUnion.

theorem Set.Finite.absorbs_biUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α} {I : Set ι} (hI : I.Finite) : Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)

theorem Absorbs.biUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α} {I : Set ι} (hI : I.Finite) : (∀ i ∈ I, Absorbs M s (t i)) → Absorbs M s (⋃ i ∈ I, t i)

Alias of the reverse direction of Set.Finite.absorbs_biUnion.

@[deprecated Set.Finite.absorbs_biUnion]

theorem Set.Finite.absorbs_iUnion {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α} {I : Set ι} (hI : I.Finite) : Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)

Alias of Set.Finite.absorbs_biUnion.

@[simp]

theorem absorbs_biUnion_finset {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α} {I : Finset ι} : Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)

theorem Absorbs.biUnion_finset {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α} {I : Finset ι} : (∀ i ∈ I, Absorbs M s (t i)) → Absorbs M s (⋃ i ∈ I, t i)

Alias of the reverse direction of absorbs_biUnion_finset.

@[deprecated absorbs_biUnion_finset]

theorem absorbs_iUnion_finset {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {ι : Type u_3} {t : ι → Set α} {I : Finset ι} : Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)

Alias of absorbs_biUnion_finset.

theorem Absorbs.add {M : Type u_1} {E : Type u_2} [Bornology M] {s₁ : Set E} {s₂ : Set E} {t₁ : Set E} {t₂ : Set E} [AddZeroClass E] [DistribSMul M E] (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) : Absorbs M (s₁ + s₂) (t₁ + t₂)

theorem Absorbs.zero {M : Type u_1} {E : Type u_2} [Bornology M] [Zero E] [SMulZeroClass M E] {s : Set E} (hs : 0 ∈ s) : Absorbs M s 0

@[simp]

theorem Absorbs.univ {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s : Set α} : Absorbs G₀ Set.univ s

theorem absorbs_iff_eventually_cobounded_mapsTo {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s : Set α} {t : Set α} : Absorbs G₀ s t ↔ ∀ᶠ (c : G₀) in Bornology.cobounded G₀, Set.MapsTo (fun (x : α) => c⁻¹ • x) t s

theorem Absorbs.eventually_cobounded_mapsTo {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s : Set α} {t : Set α} : Absorbs G₀ s t → ∀ᶠ (c : G₀) in Bornology.cobounded G₀, Set.MapsTo (fun (x : α) => c⁻¹ • x) t s

Alias of the forward direction of absorbs_iff_eventually_cobounded_mapsTo.

theorem Set.Finite.absorbs_sInter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {t : Set α} {S : Set (Set α)} (hS : S.Finite) : Absorbs G₀ (⋂₀ S) t ↔ ∀ s ∈ S, Absorbs G₀ s t

theorem Absorbs.sInter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {t : Set α} {S : Set (Set α)} (hS : S.Finite) : (∀ s ∈ S, Absorbs G₀ s t) → Absorbs G₀ (⋂₀ S) t

Alias of the reverse direction of Set.Finite.absorbs_sInter.

@[simp]

theorem absorbs_inter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s : Set α} {t : Set α} {u : Set α} : Absorbs G₀ (s ∩ t) u ↔ Absorbs G₀ s u ∧ Absorbs G₀ t u

theorem Absorbs.inter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s : Set α} {t : Set α} {u : Set α} (hs : Absorbs G₀ s u) (ht : Absorbs G₀ t u) : Absorbs G₀ (s ∩ t) u

@[simp]

theorem absorbs_iInter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {t : Set α} {ι : Sort u_3} [Finite ι] {s : ι → Set α} : Absorbs G₀ (⋂ (i : ι), s i) t ↔ ∀ (i : ι), Absorbs G₀ (s i) t

theorem Absorbs.iInter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {t : Set α} {ι : Sort u_3} [Finite ι] {s : ι → Set α} : (∀ (i : ι), Absorbs G₀ (s i) t) → Absorbs G₀ (⋂ (i : ι), s i) t

Alias of the reverse direction of absorbs_iInter.

theorem Set.Finite.absorbs_biInter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {t : Set α} {ι : Type u_3} {I : Set ι} (hI : I.Finite) {s : ι → Set α} : Absorbs G₀ (⋂ i ∈ I, s i) t ↔ ∀ i ∈ I, Absorbs G₀ (s i) t

theorem Absorbs.biInter {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {t : Set α} {ι : Type u_3} {I : Set ι} (hI : I.Finite) {s : ι → Set α} : (∀ i ∈ I, Absorbs G₀ (s i) t) → Absorbs G₀ (⋂ i ∈ I, s i) t

Alias of the reverse direction of Set.Finite.absorbs_biInter.

@[simp]

theorem absorbs_zero_iff {G₀ : Type u_1} [GroupWithZero G₀] [Bornology G₀] [(Bornology.cobounded G₀).NeBot] {E : Type u_3} [AddMonoid E] [DistribMulAction G₀ E] {s : Set E} : Absorbs G₀ s 0 ↔ 0 ∈ s

@[simp]

theorem absorbs_neg_neg {M : Type u_1} {E : Type u_2} [Monoid M] [AddGroup E] [DistribMulAction M E] [Bornology M] {s : Set E} {t : Set E} : Absorbs M (-s) (-t) ↔ Absorbs M s t

theorem Absorbs.of_neg_neg {M : Type u_1} {E : Type u_2} [Monoid M] [AddGroup E] [DistribMulAction M E] [Bornology M] {s : Set E} {t : Set E} : Absorbs M (-s) (-t) → Absorbs M s t

Alias of the forward direction of absorbs_neg_neg.

theorem Absorbs.neg_neg {M : Type u_1} {E : Type u_2} [Monoid M] [AddGroup E] [DistribMulAction M E] [Bornology M] {s : Set E} {t : Set E} : Absorbs M s t → Absorbs M (-s) (-t)

Alias of the reverse direction of absorbs_neg_neg.

theorem Absorbs.sub {M : Type u_1} {E : Type u_2} [Monoid M] [AddGroup E] [DistribMulAction M E] [Bornology M] {s₁ : Set E} {s₂ : Set E} {t₁ : Set E} {t₂ : Set E} (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) : Absorbs M (s₁ - s₂) (t₁ - t₂)

theorem Absorbent.mono {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t : Set α} (ht : Absorbent M s) (hsub : s ⊆ t) : Absorbent M t

@[deprecated Absorbent.mono]

theorem Absorbent.subset {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t : Set α} (ht : Absorbent M s) (hsub : s ⊆ t) : Absorbent M t

Alias of Absorbent.mono.

theorem absorbent_iff_forall_absorbs_singleton {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} : Absorbent M s ↔ ∀ (x : α), Absorbs M s {x}

theorem Absorbent.absorbs {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} (hs : Absorbent M s) {x : α} : Absorbs M s {x}

theorem Absorbent.absorbs_finite {M : Type u_1} {α : Type u_2} [Bornology M] [SMul M α] {s : Set α} {t : Set α} (hs : Absorbent M s) (ht : t.Finite) : Absorbs M s t

theorem Absorbent.vadd_absorbs {M : Type u_1} {E : Type u_2} [Bornology M] [AddZeroClass E] [DistribSMul M E] {s₁ : Set E} {s₂ : Set E} {t : Set E} {x : E} (h₁ : Absorbent M s₁) (h₂ : Absorbs M s₂ t) : Absorbs M (s₁ + s₂) (x +ᵥ t)

theorem absorbent_univ {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] : Absorbent G₀ Set.univ

theorem absorbent_iff_inv_smul {G₀ : Type u_1} {α : Type u_2} [GroupWithZero G₀] [Bornology G₀] [MulAction G₀ α] {s : Set α} : Absorbent G₀ s ↔ ∀ (x : α), ∀ᶠ (c : G₀) in Bornology.cobounded G₀, c⁻¹ • x ∈ s

theorem Absorbent.zero_mem {G₀ : Type u_1} {E : Type u_3} [GroupWithZero G₀] [Bornology G₀] [(Bornology.cobounded G₀).NeBot] [AddMonoid E] [DistribMulAction G₀ E] {s : Set E} (hs : Absorbent G₀ s) : 0 ∈ s