Products of relation algebras

This module defines the relation algebra structure over products. This is a key component of the representation of a relation algebra.

@[instance_reducible]

instance Cslib.Pi.instRelationAlgebra {ι : Type u_1} {β : ι → Type u_2} [(i : ι) → RelationAlgebra (β i)] : RelationAlgebra ((i : ι) → β i)

Equations

• Cslib.Pi.instRelationAlgebra = { toBooleanAlgebra := Pi.instBooleanAlgebra, toMonoid := Pi.monoid, toStarMul := Pi.instStarMulForall, sup_mul := ⋯, star_sup := ⋯, tarski := ⋯ }

def Cslib.RelationAlgebraHom.pi {α : Type u_1} [RelationAlgebra α] {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → RelationAlgebra (β i)] (f : (i : ι) → RelationAlgebraHom α (β i)) : RelationAlgebraHom α ((i : ι) → β i)

The product of RelationAlgebraHoms is a RelationAlgebraHom into a product.

Equations

• Cslib.RelationAlgebraHom.pi f = { toFun := fun (a : α) (i : ι) => (f i) a, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[simp]

theorem Cslib.RelationAlgebraHom.pi_apply {α : Type u_1} [RelationAlgebra α] {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → RelationAlgebra (β i)] (f : (i : ι) → RelationAlgebraHom α (β i)) (a : α) (i : ι) : (pi f) a i = (f i) a

def Cslib.RelationAlgebraHom.eval {ι : Type u_2} (β : ι → Type u_3) [(i : ι) → RelationAlgebra (β i)] (i : ι) : RelationAlgebraHom ((i : ι) → β i) (β i)

The RelationAlgebraHom into a single fiber.

Equations

• Cslib.RelationAlgebraHom.eval β i = { toFun := fun (b : (i : ι) → β i) => b i, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[simp]

theorem Cslib.RelationAlgebraHom.eval_apply {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → RelationAlgebra (β i)] (i : ι) (b : (i : ι) → β i) : (eval β i) b = b i

def Cslib.RelationAlgebraHom.piEquiv (α : Type u_1) [RelationAlgebra α] {ι : Type u_2} (β : ι → Type u_3) [(i : ι) → RelationAlgebra (β i)] : ((i : ι) → RelationAlgebraHom α (β i)) ≃ RelationAlgebraHom α ((i : ι) → β i)

The equivalence between products of RelationAlgebraHom and the RelationAlgebraHom into a product that is given by composition of eval.

Equations

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