Representable relation algebras

One of the primary notions of interest in the study of relation algebras is the notion of representation by a relation algebra of concrete relations.

Recall Stone's representation for Boolean algebras which (at a low level of generality) states that every Boolean algebra has an isomorphism into a particuliar "field of sets". Tarski's hope was that an analogous property would hold for abstract relation algebras, with the isomorphism desired being into a relation algebra of concrete relations. This turns out to be false, with the clasification and conditions for the representation of a relation algebra thus being a matter of much interest.

def Cslib.RelationAlgebra.SquareRelations (α : Type u) : Type u

Relations over a type α. This definition exists because we need to prevent some instances from from Mathlib being included.

Equations

• Cslib.RelationAlgebra.SquareRelations α = SetRel α α

@[instance_reducible]

instance Cslib.RelationAlgebra.SquareRelations.instBooleanAlgebra (α : Type u) : BooleanAlgebra (SquareRelations α)

Equations

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

@[instance_reducible]

instance Cslib.RelationAlgebra.SquareRelations.instMonoid (α : Type u) : Monoid (SquareRelations α)

Equations

• Cslib.RelationAlgebra.SquareRelations.instMonoid α = { one := SetRel.id, mul := SetRel.comp, mul_assoc := ⋯, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

@[instance_reducible]

instance Cslib.RelationAlgebra.SquareRelations.instStarMul (α : Type u) : StarMul (SquareRelations α)

Equations

• Cslib.RelationAlgebra.SquareRelations.instStarMul α = { star := SetRel.inv, star_involutive := ⋯, star_mul := ⋯ }

@[instance_reducible]

instance Cslib.RelationAlgebra.SquareRelations.inst (α : Type u) : RelationAlgebra (SquareRelations α)

Equations

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

structure Cslib.RelationAlgebra.Representation (α : Type u) [RelationAlgebra α] (ι : Type v) (β : ι → Type w) : Type (max (max u v) w)

A representation of a relation algebra is an injective morphism into a product of relations.

• hom : RelationAlgebraHom α ((i : ι) → SquareRelations (β i))

  A RelationAlgebraHom into a product of relations.

• injective : Function.Injective ⇑self.hom

def Cslib.RelationAlgebra.Representable (α : Type u) [RelationAlgebra α] : Prop

A relation algebra is representable if a Representation exists.

Equations

• Cslib.RelationAlgebra.Representable α = ∃ (ι : Type ?u.1) (β : ι → Type ?u.1), Nonempty (Cslib.RelationAlgebra.Representation α ι β)