The category of measurable spaces

Measurable spaces and measurable functions form a (concrete) category MeasCat.

Main definitions

• Measure : MeasCat ⥤ MeasCat: the functor which sends a measurable space X to the space of measures on X; it is a monad (the "Giry monad").

• Borel : TopCat ⥤ MeasCat: sends a topological space X to X equipped with the σ-algebra of Borel sets (the σ-algebra generated by the open subsets of X).

Tags

measurable space, giry monad, borel

def MeasCat : Type (u + 1)

The category of measurable spaces and measurable functions.

Equations

• MeasCat = CategoryTheory.Bundled MeasurableSpace

instance MeasCat.instCoeSortType : CoeSort MeasCat (Type u_1)

Equations

• MeasCat.instCoeSortType = CategoryTheory.Bundled.coeSort

instance MeasCat.instMeasurableSpaceα (X : MeasCat) : MeasurableSpace ↑X

Equations

• X.instMeasurableSpaceα = X.str

def MeasCat.of (α : Type u) [ms : MeasurableSpace α] : MeasCat

Construct a bundled MeasCat from the underlying type and the typeclass.

Equations

• MeasCat.of α = { α := α, str := ms }

@[simp]

theorem MeasCat.coe_of (X : Type u) [MeasurableSpace X] : ↑(MeasCat.of X) = X

instance MeasCat.unbundledHom : CategoryTheory.UnbundledHom @Measurable

Equations

• MeasCat.unbundledHom = ⋯

instance instMeasCatLargeCategory : CategoryTheory.LargeCategory MeasCat

Equations

• instMeasCatLargeCategory = CategoryTheory.BundledHom.category fun (α β : Type ?u.9) (Iα : MeasurableSpace α) (Iβ : MeasurableSpace β) => Subtype Measurable

instance MeasCat.instConcreteCategory : CategoryTheory.ConcreteCategory MeasCat

Equations

• MeasCat.instConcreteCategory = id inferInstance

instance MeasCat.instInhabited : Inhabited MeasCat

Equations

• MeasCat.instInhabited = { default := MeasCat.of Empty }

def MeasCat.Measure : CategoryTheory.Functor MeasCat MeasCat

Measure X is the measurable space of measures over the measurable space X. It is the weakest measurable space, s.t. fun μ ↦ μ s is measurable for all measurable sets s in X. An important purpose is to assign a monadic structure on it, the Giry monad. In the Giry monad, the pure values are the Dirac measure, and the bind operation maps to the integral: (μ >>= ν) s = ∫ x. (ν x) s dμ.

In probability theory, the MeasCat-morphisms X → Prob X are (sub-)Markov kernels (here Prob is the restriction of Measure to (sub-)probability space.)

Equations

• One or more equations did not get rendered due to their size.

def MeasCat.Giry : CategoryTheory.Monad MeasCat

The Giry monad, i.e. the monadic structure associated with Measure.

Equations

• One or more equations did not get rendered due to their size.

def MeasCat.Integral : MeasCat.Giry.Algebra

An example for an algebra on Measure: the nonnegative Lebesgue integral is a hom, behaving nicely under the monad operations.

Equations

• One or more equations did not get rendered due to their size.

instance TopCat.hasForgetToMeasCat : CategoryTheory.HasForget₂ TopCat MeasCat

Equations

• TopCat.hasForgetToMeasCat = CategoryTheory.BundledHom.mkHasForget₂ borel (fun {X Y : CategoryTheory.Bundled TopologicalSpace} (f : X ⟶ Y) => ⟨f.toFun, ⋯⟩) @TopCat.hasForgetToMeasCat.proof_2

@[reducible, inline]

abbrev Borel : CategoryTheory.Functor TopCat MeasCat

The Borel functor, the canonical embedding of topological spaces into measurable spaces.

Equations

• Borel = CategoryTheory.forget₂ TopCat MeasCat