Relation isomorphisms form a group

This file contains Monoid instances for RelHom and OrderHom, where multiplication is given by composition. Likewise there is a Group instance for RelIso. Because OrderIso is an abbreviation for RelIso, there is no need for an additional instance.

TODO

• Rename the mul_def/one_def lemmas to mul_eq_comp/one_eq_id.
• Use the IsMulApplyEqComp and IsOneApplyEqSelf classes for RelHom and RelIso.

@[implicit_reducible]

instance RelHom.instMonoid {α : Type u_1} {r : α → α → Prop} : Monoid (r →r r)

Equations

• RelHom.instMonoid = { mul := RelHom.comp, mul_assoc := ⋯, one := RelHom.id r, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

theorem RelHom.one_def {α : Type u_1} {r : α → α → Prop} : 1 = RelHom.id r

theorem RelHom.mul_def {α : Type u_1} {r : α → α → Prop} (f g : r →r r) : f * g = f.comp g

@[simp]

theorem RelHom.coe_one {α : Type u_1} {r : α → α → Prop} : ⇑1 = id

@[simp]

theorem RelHom.coe_mul {α : Type u_1} {r : α → α → Prop} (f g : r →r r) : ⇑(f * g) = ⇑f ∘ ⇑g

theorem RelHom.one_apply {α : Type u_1} {r : α → α → Prop} (a : α) : 1 a = a

theorem RelHom.mul_apply {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r →r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x)

@[implicit_reducible]

instance RelEmbedding.instMonoid {α : Type u_1} {r : α → α → Prop} : Monoid (r ↪r r)

Equations

• RelEmbedding.instMonoid = { mul := fun (f g : r ↪r r) => g.trans f, mul_assoc := ⋯, one := RelEmbedding.refl r, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

theorem RelEmbedding.one_def {α : Type u_1} {r : α → α → Prop} : 1 = RelEmbedding.refl r

theorem RelEmbedding.mul_def {α : Type u_1} {r : α → α → Prop} (f g : r ↪r r) : f * g = g.trans f

@[simp]

theorem RelEmbedding.coe_one {α : Type u_1} {r : α → α → Prop} : ⇑1 = id

@[simp]

theorem RelEmbedding.coe_mul {α : Type u_1} {r : α → α → Prop} (f g : r ↪r r) : ⇑(f * g) = ⇑f ∘ ⇑g

theorem RelEmbedding.one_apply {α : Type u_1} {r : α → α → Prop} (a : α) : 1 a = a

theorem RelEmbedding.mul_apply {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ↪r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x)

@[implicit_reducible]

instance RelIso.instGroup {α : Type u_1} {r : α → α → Prop} : Group (r ≃r r)

Equations

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

theorem RelIso.one_def {α : Type u_1} {r : α → α → Prop} : 1 = RelIso.refl r

theorem RelIso.mul_def {α : Type u_1} {r : α → α → Prop} (f g : r ≃r r) : f * g = g.trans f

@[simp]

theorem RelIso.coe_one {α : Type u_1} {r : α → α → Prop} : ⇑1 = id

@[simp]

theorem RelIso.coe_mul {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r) : ⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂

theorem RelIso.one_apply {α : Type u_1} {r : α → α → Prop} (x : α) : 1 x = x

theorem RelIso.mul_apply {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ≃r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x)

@[simp]

theorem RelIso.inv_apply_self {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α) : e⁻¹ (e x) = x

@[simp]

theorem RelIso.apply_inv_self {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α) : e (e⁻¹ x) = x

@[implicit_reducible]

instance OrderHom.instMul {α : Type u_1} [Preorder α] : Mul (α →o α)

Equations

• OrderHom.instMul = { mul := fun (f g : α →o α) => f.comp g }

@[implicit_reducible]

instance OrderHom.instOne {α : Type u_1} [Preorder α] : One (α →o α)

Equations

• OrderHom.instOne = { one := OrderHom.id }

instance OrderHom.instIsMulApplyEqComp {α : Type u_1} [Preorder α] : IsMulApplyEqComp (α →o α) α

instance OrderHom.instIsOneApplyEqSelf {α : Type u_1} [Preorder α] : IsOneApplyEqSelf (α →o α) α

theorem OrderHom.mul_eq_comp {α : Type u_1} [Preorder α] (f g : α →o α) : f * g = f.comp g

theorem OrderHom.one_eq_id {α : Type u_1} [Preorder α] : 1 = id

@[implicit_reducible]

instance OrderHom.instMonoid {α : Type u_1} [Preorder α] : Monoid (α →o α)

Equations

• OrderHom.instMonoid = { toMul := OrderHom.instMul, mul_assoc := ⋯, toOne := OrderHom.instOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }