module Cat.Morphism.Duality {o โ„“} (๐’ž : Precategory o โ„“) where

Duality of morphism classes๐Ÿ”—

In this file we prove that morphisms classes in a category correspond to their duals in the opposite category. There is very little interesting mathematical content in this file; it is pure boilerplate.

We start by showing that monos and epis are dual.

co-monoโ†’epi : a ๐’ž^op.โ†ช b โ†’ b ๐’ž.โ†  a
co-monoโ†’epi f .Cat.Morphism.mor = ๐’ž^op.mor f
co-monoโ†’epi f .Cat.Morphism.epic = ๐’ž^op.monic f

epiโ†’co-mono : b ๐’ž.โ†  a โ†’ a ๐’ž^op.โ†ช b
epiโ†’co-mono f .Cat.Morphism.mor = ๐’ž.mor f
epiโ†’co-mono f .Cat.Morphism.monic = ๐’ž.epic f

co-epiโ†’mono : a ๐’ž^op.โ†  b โ†’ b ๐’ž.โ†ช a
co-epiโ†’mono f .Cat.Morphism.mor = ๐’ž^op.mor f
co-epiโ†’mono f .Cat.Morphism.monic = ๐’ž^op.epic f

monoโ†’co-epi : b ๐’ž.โ†ช a โ†’ a ๐’ž^op.โ†  b
monoโ†’co-epi f .Cat.Morphism.mor = ๐’ž.mor f
monoโ†’co-epi f .Cat.Morphism.epic = ๐’ž.monic f

Next, sections and retractions.

co-sectionโ†’retract : ๐’ž^op.has-section f โ†’ ๐’ž.has-retract f
co-sectionโ†’retract f .Cat.Morphism.retract = ๐’ž^op.section f
co-sectionโ†’retract f .Cat.Morphism.is-retract = ๐’ž^op.is-section f

retractโ†’co-section : ๐’ž.has-retract f โ†’ ๐’ž^op.has-section f
retractโ†’co-section f .Cat.Morphism.section = ๐’ž.retract f
retractโ†’co-section f .Cat.Morphism.is-section = ๐’ž.is-retract f

co-retractโ†’section : ๐’ž^op.has-retract f โ†’ ๐’ž.has-section f
co-retractโ†’section f .Cat.Morphism.section = ๐’ž^op.retract f
co-retractโ†’section f .Cat.Morphism.is-section = ๐’ž^op.is-retract f

sectionโ†’co-retract : ๐’ž.has-section f โ†’ ๐’ž^op.has-retract f
sectionโ†’co-retract f .Cat.Morphism.retract = ๐’ž.section f
sectionโ†’co-retract f .Cat.Morphism.is-retract = ๐’ž.is-section f

Next, we show that invertible morphisms are self-dual.

co-inversesโ†’inverses : ๐’ž^op.Inverses f g โ†’ ๐’ž.Inverses f g
co-inversesโ†’inverses i .Cat.Morphism.Inverses.invl =
  ๐’ž^op.Inverses.invr i
co-inversesโ†’inverses i .Cat.Morphism.Inverses.invr =
  ๐’ž^op.Inverses.invl i

inversesโ†’co-inverses : ๐’ž.Inverses f g โ†’ ๐’ž^op.Inverses f g
inversesโ†’co-inverses i .Cat.Morphism.Inverses.invl =
  ๐’ž.Inverses.invr i
inversesโ†’co-inverses i .Cat.Morphism.Inverses.invr =
  ๐’ž.Inverses.invl i

co-invertibleโ†’invertible : ๐’ž^op.is-invertible f โ†’ ๐’ž.is-invertible f
co-invertibleโ†’invertible i .Cat.Morphism.is-invertible.inv =
  ๐’ž^op.is-invertible.inv i
co-invertibleโ†’invertible i .Cat.Morphism.is-invertible.inverses =
  co-inversesโ†’inverses (๐’ž^op.is-invertible.inverses i)

invertibleโ†’co-invertible : ๐’ž.is-invertible f โ†’ ๐’ž^op.is-invertible f
invertibleโ†’co-invertible i .Cat.Morphism.is-invertible.inv =
  ๐’ž.is-invertible.inv i
invertibleโ†’co-invertible i .Cat.Morphism.is-invertible.inverses =
  inversesโ†’co-inverses (๐’ž.is-invertible.inverses i)

co-isoโ†’iso : a ๐’ž^op.โ‰… b โ†’ b ๐’ž.โ‰… a
co-isoโ†’iso f .Cat.Morphism.to = ๐’ž^op.to f
co-isoโ†’iso f .Cat.Morphism.from = ๐’ž^op.from f
co-isoโ†’iso f .Cat.Morphism.inverses = co-inversesโ†’inverses (๐’ž^op.inverses f)

isoโ†’co-iso : b ๐’ž.โ‰… a โ†’ a ๐’ž^op.โ‰… b
isoโ†’co-iso f .Cat.Morphism.to = ๐’ž.to f
isoโ†’co-iso f .Cat.Morphism.from = ๐’ž.from f
isoโ†’co-iso f .Cat.Morphism.inverses = inversesโ†’co-inverses (๐’ž.inverses f)