Morphisms and isomorphisms of relation algebras

structure Cslib.RelationAlgebraHom (α : Type u_1) (β : Type u_2) [RelationAlgebra α] [RelationAlgebra β] extends BoundedLatticeHom α β, α →⋆* β : Type (max u_1 u_2)

The type of relation algebra homomorphisms from α to β, preserving both the Boolean algebra and composition operations

• toFun : α → β
• map_sup' (a b : α) : self.toFun (a ⊔ b) = self.toFun a ⊔ self.toFun b
• map_inf' (a b : α) : self.toFun (a ⊓ b) = self.toFun a ⊓ self.toFun b
• map_top' : self.toFun ⊤ = ⊤
• map_bot' : self.toFun ⊥ = ⊥
• map_one' : self.toFun 1 = 1
• map_mul' (x y : α) : self.toFun (x * y) = self.toFun x * self.toFun y
• map_star' (a : α) : self.toFun (star a) = star (self.toFun a)

structure Cslib.RelationAlgebraEquiv (α : Type u_1) (β : Type u_2) [RelationAlgebra α] [RelationAlgebra β] extends (fun (x1 x2 : α) => x1 ≤ x2) ≃r fun (x1 x2 : β) => x1 ≤ x2, α ≃⋆* β : Type (max u_1 u_2)

The type of relation algebra equivalence from α to β, preserving both the Boolean algebra and composition operations

• toFun : α → β
• invFun : β → α
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_rel_iff' {a b : α} : self.toEquiv a ≤ self.toEquiv b ↔ a ≤ b
• map_mul' (x y : α) : self.toFun (x * y) = self.toFun x * self.toFun y
• map_star' (a : α) : self.toFun (star a) = star (self.toFun a)

@[instance_reducible]

instance Cslib.RelationAlgebraHom.instFunLike {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] : FunLike (RelationAlgebraHom α β) α β

Equations

• Cslib.RelationAlgebraHom.instFunLike = { coe := fun (f : Cslib.RelationAlgebraHom α β) => f.toFun, coe_injective := ⋯ }

instance Cslib.RelationAlgebraHom.instBoundedLatticeHomClass {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] : BoundedLatticeHomClass (RelationAlgebraHom α β) α β

instance Cslib.RelationAlgebraHom.instMonoidHomClass {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] : MonoidHomClass (RelationAlgebraHom α β) α β

instance Cslib.RelationAlgebraHom.instStarHomClass {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] : StarHomClass (RelationAlgebraHom α β) α β

theorem Cslib.RelationAlgebraHom.ext {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] {f g : RelationAlgebraHom α β} (h : ∀ (a : α), f a = g a) : f = g

theorem Cslib.RelationAlgebraHom.ext_iff {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] {f g : RelationAlgebraHom α β} : f = g ↔ ∀ (a : α), f a = g a

def Cslib.RelationAlgebraHom.id (α : Type u_4) [RelationAlgebra α] : RelationAlgebraHom α α

id as a RelationAlgebraHom

Equations

• Cslib.RelationAlgebraHom.id α = { toBoundedLatticeHom := BoundedLatticeHom.id α, map_one' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

def Cslib.RelationAlgebraHom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [RelationAlgebra α] [RelationAlgebra β] [RelationAlgebra γ] (f : RelationAlgebraHom β γ) (g : RelationAlgebraHom α β) : RelationAlgebraHom α γ

Composition of RelationAlgebraHom

Equations

• f.comp g = { toBoundedLatticeHom := f.comp g.toBoundedLatticeHom, map_one' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[simp]

theorem Cslib.RelationAlgebraHom.id_apply {α : Type u_1} [RelationAlgebra α] (a : α) : (RelationAlgebraHom.id α) a = a

@[simp]

theorem Cslib.RelationAlgebraHom.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [RelationAlgebra α] [RelationAlgebra β] [RelationAlgebra γ] (f : RelationAlgebraHom β γ) (g : RelationAlgebraHom α β) (a : α) : (f.comp g) a = f (g a)

@[instance_reducible]

instance Cslib.RelationAlgebraEquiv.instEquivLike {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] : EquivLike (RelationAlgebraEquiv α β) α β

Equations

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

instance Cslib.RelationAlgebraEquiv.instOrderIsoClass {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] : OrderIsoClass (RelationAlgebraEquiv α β) α β

instance Cslib.RelationAlgebraEquiv.instMulEquivClass {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] : MulEquivClass (RelationAlgebraEquiv α β) α β

instance Cslib.RelationAlgebraEquiv.instStarHomClass {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] : StarHomClass (RelationAlgebraEquiv α β) α β

theorem Cslib.RelationAlgebraEquiv.ext {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] {f g : RelationAlgebraEquiv α β} (h : ∀ (a : α), f a = g a) : f = g

theorem Cslib.RelationAlgebraEquiv.ext_iff {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] {f g : RelationAlgebraEquiv α β} : f = g ↔ ∀ (a : α), f a = g a

def Cslib.RelationAlgebraEquiv.refl (α : Type u_4) [RelationAlgebra α] : RelationAlgebraEquiv α α

The reflexive RelationAlgebraEquiv

Equations

• Cslib.RelationAlgebraEquiv.refl α = { toOrderIso := OrderIso.refl α, map_mul' := ⋯, map_star' := ⋯ }

def Cslib.RelationAlgebraEquiv.symm {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] (f : RelationAlgebraEquiv α β) : RelationAlgebraEquiv β α

The symmetric RelationAlgebraEquiv

Equations

• f.symm = { toOrderIso := f.symm, map_mul' := ⋯, map_star' := ⋯ }

def Cslib.RelationAlgebraEquiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [RelationAlgebra α] [RelationAlgebra β] [RelationAlgebra γ] (f : RelationAlgebraEquiv α β) (g : RelationAlgebraEquiv β γ) : RelationAlgebraEquiv α γ

The transitive RelationAlgebraEquiv

Equations

• f.trans g = { toOrderIso := f.trans g.toOrderIso, map_mul' := ⋯, map_star' := ⋯ }

def Cslib.RelationAlgebraEquiv.toHom {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] (f : RelationAlgebraEquiv α β) : RelationAlgebraHom α β

The RelationAlgebraHom underlying an RelationAlgebraEquiv

Equations

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

@[simp]

theorem Cslib.RelationAlgebraEquiv.refl_apply {α : Type u_1} [RelationAlgebra α] (a : α) : (RelationAlgebraEquiv.refl α) a = a

@[simp]

theorem Cslib.RelationAlgebraEquiv.trans_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [RelationAlgebra α] [RelationAlgebra β] [RelationAlgebra γ] (f : RelationAlgebraEquiv α β) (g : RelationAlgebraEquiv β γ) (a : α) : (f.trans g) a = g (f a)

@[simp]

theorem Cslib.RelationAlgebraEquiv.toHom_apply {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] (f : RelationAlgebraEquiv α β) (a : α) : f.toHom a = f a

@[simp]

theorem Cslib.RelationAlgebraEquiv.symm_apply_apply {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] (f : RelationAlgebraEquiv α β) (a : α) : f.symm (f a) = a

@[simp]

theorem Cslib.RelationAlgebraEquiv.apply_symm_apply {α : Type u_1} {β : Type u_2} [RelationAlgebra α] [RelationAlgebra β] (f : RelationAlgebraEquiv α β) (b : β) : f (f.symm b) = b