Ring of sets generated by a set

Stream: new members

[Iocta]

I'm looking for this theorem about ring-of-sets.

Let A be any collection of subsets of a given set. Then there exists a unique “smallest” ring containing A , where “smallest” means, by definition, that the ring contains A and the ring is contained in any ring that contains A . This smallest ring is called the ring generated by A and is denoted by R(A ).

I see IsSetRing. Where can I find the theorem?

[Kevin Buzzard]

I'm confused by this question. Where is the addition and multiplication defined for this ring? All we started with were sets. I'm also not clear about what "containing A" means. As an element? As a subset? What is the type of R(A)? Can you write the question in Lean?

Is the answer docs#Ring.closure ?

[Iocta]

Where is the addition and multiplication defined for this ring?

MeasureTheory.SetSemiring says

A semi-ring of sets C (in the sense of measure theory) is a family of sets containing ∅, stable by intersection and such that for all s, t ∈ C, t \ s is equal to a disjoint union of finitely many sets in C.

My impression is that this "ring of sets" defined by IsSetRing is a different thing from the ring in algebra, though perhaps there is a relationship I don't know about yet.

Is the answer docs#Ring.closure ?

That may be it...

[Kevin Buzzard]

I see, so perhaps something like "addition is union, multiplication is intersection"? I had misunderstood the kind of ring you were talking about. As far as I can see your ring might not have a 1, so docs#Ring.closure is no good for you because those kind of rings have 1. I don't know the answer to your question or even if the theorem is in Lean but it would be fun to prove.

[Kevin Buzzard]

import Mathlib

namespace MeasureTheory

def setRingClosure {α : Type} (A : Set (Set α)) : Set (Set α) :=
  ⋂₀ {R : Set (Set α) | A ⊆ R ∧ IsSetRing R}

variable {α : Type} (A : Set (Set α))

theorem setRingClosure_isSetRing : IsSetRing (setRingClosure A) := by
  sorry

[Eric Wieser]

Kevin Buzzard said:

addition is union, multiplication is intersection

Is docs#SetSemiring relevant?

[Kevin Buzzard]

I don't think you need it. Here, I can start you off. I find these kinds of exercises quite fun :-)

import Mathlib

namespace MeasureTheory

def setRingClosure {α : Type} (A : Set (Set α)) : Set (Set α) :=
  ⋂₀ {R : Set (Set α) | A ⊆ R ∧ IsSetRing R}

variable {α : Type} (A : Set (Set α))

lemma mem_setRingClosure_iff (s : Set α) :
    s ∈ setRingClosure A ↔ ∀ R, A ⊆ R ∧ IsSetRing R → s ∈ R := Set.mem_sInter

theorem setRingClosure_isSetRing : IsSetRing (setRingClosure A) where
  empty_mem := by
    rw [mem_setRingClosure_iff]
    intro R ⟨hAR, hR⟩
    exact hR.empty_mem
  union_mem := sorry
  diff_mem := sorry

[Soundwave]

Think they asked because there is also a semiring closure in the lib.

[Iocta]

import Mathlib

namespace MeasureTheory

variable {α : Type} (A : Set (Set α))

def setRingClosure {α : Type} (A : Set (Set α)) : Set (Set α) :=
  ⋂₀ {R : Set (Set α) | A ⊆ R ∧ IsSetRing R}

lemma mem_setRingClosure_iff (s : Set α) :
    s ∈ setRingClosure A ↔ ∀ R, A ⊆ R ∧ IsSetRing R → s ∈ R :=
  Set.mem_def

theorem setRingClosure_isSetRing : IsSetRing (setRingClosure A) where
  empty_mem := by
    -- Why does it let me do this instead of making me explicitly rewrite ∩₀?
    intro R ⟨hAR,hR⟩
    exact hR.empty_mem
  union_mem := by {
    intros s t hs ht
    intro R ⟨hAR, hR⟩
    simp [mem_setRingClosure_iff] at *
    apply hR.union_mem (hs R hAR hR) (ht R hAR hR)
  }
  diff_mem := by {
    intros s t hs ht
    simp [mem_setRingClosure_iff] at *
    intros R hAR hR
    apply hR.diff_mem (hs R hAR hR) (ht R hAR hR)
  }

[Iocta]

Why does intro R ⟨hAR,hR⟩ work to unpack the ⋂₀ instead of making me rewrite the ⋂₀ manually?

[Soundwave]

The head is ∈, not ⋂₀, which is reducible to the membership predicate. Use reduce to see what you're "actually" operating on.

[Etienne Marion]

The generated ring of sets is not in Mathlib. However there is docs#MeasureTheory.generateSetAlgebra which is the same but for an algebra of sets (same as a ring but requires to contain the whole set), maybe it will be enough for you, otherwise it can show you how to define it.