# 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.

- of :: (

- carrier : Type u

  The underlying measurable space.

- str : MeasurableSpace self.carrier

- )

Instances For

source
instance MeasCat.instCoeSortType :
CoeSort MeasCat (Type u_1)
Equations

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

source
theorem MeasCat.coe_of (X : Type u) [MeasurableSpace X] :
{ carrier := X, str := inst✝ }.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 := { carrier := Empty, str := Empty.instMeasurableSpace } }

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

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

Instances For

source
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.

Instances For

source
def MeasCat.Integral :
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.

Instances For

source
instance TopCat.hasForgetToMeasCat :
CategoryTheory.HasForget₂ TopCat MeasCat
Equations

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

source
@[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

Instances For