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

source

structure MeasCat :

Type (u + 1)

The category of measurable spaces and measurable functions.

carrier : Type u
The underlying measurable space.
str : MeasurableSpace self.carrier

source

instance MeasCat.instCoeSortType :

CoeSort MeasCat (Type u_1)

Equations

MeasCat.instCoeSortType = { coe := MeasCat.carrier }

source

@[reducible, inline]

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

MeasCat

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

Equations

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

source

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

(of X).carrier = X

source

instance MeasCat.instLargeCategory :

CategoryTheory.LargeCategory MeasCat

Equations

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

source

instance MeasCat.instFunLikeSubtypeForallCarrierMeasurable (X : MeasCat) (Y : MeasCat) :

FunLike { f : X.carrier → Y.carrier // Measurable f } X.carrier Y.carrier

Equations

X.instFunLikeSubtypeForallCarrierMeasurable Y = { coe := fun (f : { f : X.carrier → Y.carrier // Measurable f }) => ↑f, coe_injective' := ⋯ }

source

instance MeasCat.instConcreteCategorySubtypeForallCarrierMeasurable :

CategoryTheory.ConcreteCategory MeasCat fun (x1 x2 : MeasCat) => { f : x1.carrier → x2.carrier // Measurable f }

Equations

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

source

instance MeasCat.instInhabited :

Inhabited MeasCat

Equations

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

source

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