Library UniMath.CategoryTheory.LatticeObject

*****************************************************************************
Internal lattice objects in a category
Contents:
Based on "Sheaves in Geometry and Logic" by Mac Lane and Moerdijk (Section IV.8, page 198)
Written by: Anders Mörtberg, 2017

Definition of lattice objects and bounded lattice objects

Section LatticeObject_def.

Context {C : precategory} {BPC : BinProducts C}.

Local Notation "c ⊗ d" := (BinProductObject C (BPC c d)) : cat.
Local Notation "f '××' g" := (BinProductOfArrows _ _ _ f g) (at level 80) : cat.
Local Notation "1" := (identity _) : cat.

Let π1 {x y} : Cx y,x := BinProductPr1 _ (BPC x y).
Let π2 {x y} : Cx y,y := BinProductPr2 _ (BPC x y).

Definition binprod_assoc (x y z : C) : C(x y) z,x (y z) :=
  BinProductArrow _ _ (π1 · π1) (BinProductArrow _ _ (π1 · π2) π2).
Let α {x y z} : C(x y) z,x (y z) := binprod_assoc x y z.

Definition binprod_delta (x : C) : Cx,x x :=
  BinProductArrow _ _ (identity x) (identity x).
Let δ {x} : Cx,x x := binprod_delta x.

Definition binprod_swap (x y : C) : Cx y,y x :=
  BinProductArrow _ _ (BinProductPr2 _ _) (BinProductPr1 _ _).
Let τ {x y} : Cx y,y x := binprod_swap x y.

Equation witnessing that a morphism representing a binary operation is associative as illustrated by the diagram:
               f×1
 (L ⊗ L) ⊗ L -------> L ⊗ L
     |                  |
   α |                  |
     V                  |
 L ⊗ (L ⊗ L)            | f
     |                  |
 1×f |                  |
     V                  V
   L ⊗ L ----------->   L
              f
Definition isassoc_cat {L} (f : CL L,L) : UU := (f ×× 1) · f = α · (1 ×× f) · f.

Equation witnessing that a morphism representing a binary operation is commutative as illustrated by the diagram:
   L ⊗ L
     |   \
     |     \
   τ |       \ f
     |         \
     |          V
   L ⊗ L -----> L
           f
Definition iscomm_cat {L} (f : CL L,L) : UU := f = τ · f.

Equation witnessing the absorbtion law as illustrated by the diagram:
           δ×1                   α
   L ⊗ L ------> (L ⊗ L) ⊗ L -------> L ⊗ (L ⊗ L)
     |                                    |
  π1 |                                    | 1×g
     V                                    V
     L <------------------------------- L ⊗ L
                       f
If f is ∧ and g is ∨ this expresses: x ∧ (x ∨ y) = x
A lattice object L has operation meet and join satisfying the above laws
Definition latticeob (L : C) : UU :=
   (meet_mor join_mor : CL L,L), latticeop_cat meet_mor join_mor.

Definition mk_latticeob {L : C} {meet_mor join_mor : CL L,L} :
  latticeop_cat meet_mor join_mor latticeob L :=
    λ (isL : latticeop_cat meet_mor join_mor), meet_mor,, join_mor ,, isL.

Definition meet_mor {L : C} (isL : latticeob L) : CL L,L := pr1 isL.
Definition join_mor {L : C} (isL : latticeob L) : CL L,L := pr1 (pr2 isL).

Bounded lattice objects

Context {TC : Terminal C}.

Let ι {x : C} : Cx,TC x :=
  BinProductArrow _ _ (TerminalArrow _ _) (identity x).

Given u : C⟦TC,L⟧ the equation witnessing the left unit law is given by the diagram:
          ι
     L ------> 1 ⊗ L
     |           |
   1 |           | u×1
     V           V
     L <------ L ⊗ L
          f
Definition islunit_cat {L} (f : CL L,L) (u : CTC,L) : UU :=
  ι · (u ×× 1) · f = 1.

Definition bounded_latticeop_cat {L} (l : latticeob L) (bot top : CTC,L) :=
  (islunit_cat (join_mor l) bot) × (islunit_cat (meet_mor l) top).

Definition bounded_latticeob (L : C) : UU :=
   (l : latticeob L) (bot top : CTC,L), bounded_latticeop_cat l bot top.

Definition mk_bounded_latticeob {L} {l : latticeob L} {bot top : CTC,L} :
  bounded_latticeop_cat l bot top bounded_latticeob L := λ bl, l,, bot,, top,, bl.

Definition bounded_latticeob_to_latticeob X : bounded_latticeob X latticeob X := pr1.
Coercion bounded_latticeob_to_latticeob : bounded_latticeob >-> latticeob.

Definition bot_mor {L} (isL : bounded_latticeob L) : CTC,L := pr1 (pr2 isL).
Definition top_mor {L} (isL : bounded_latticeob L) : CTC,L := pr1 (pr2 (pr2 isL)).

End LatticeObject_def.

Arguments latticeob {_} _ _.
Arguments bounded_latticeob {_} _ _ _.

Section LatticeObject_accessors.

Context {C : precategory} (BPC : BinProducts C) {L : C} (isL : latticeob BPC L).

Definition isassoc_meet_mor : isassoc_cat (meet_mor isL) :=
  pr1 (pr1 (pr2 (pr2 isL))).
Definition iscomm_meet_mor : iscomm_cat (meet_mor isL) :=
  pr2 (pr1 (pr2 (pr2 isL))).
Definition isassoc_join_mor : isassoc_cat (join_mor isL) :=
  pr1 (pr1 (pr2 (pr2 (pr2 isL)))).
Definition iscomm_join_mor : iscomm_cat (join_mor isL) :=
  pr2 (pr1 (pr2 (pr2 (pr2 isL)))).
Definition meet_mor_absorb_join_mor : isabsorb_cat (meet_mor isL) (join_mor isL) :=
  pr1 (pr2 (pr2 (pr2 (pr2 isL)))).
Definition join_mor_absorb_meet_mor : isabsorb_cat (join_mor isL) (meet_mor isL) :=
  pr2 (pr2 (pr2 (pr2 (pr2 isL)))).

End LatticeObject_accessors.

Section BoundedLatticeObject_accessors.

Context {C : precategory} (BPC : BinProducts C) (TC : Terminal C).
Context {L : C} (l : bounded_latticeob BPC TC L).

Definition islunit_join_mor_bot_mor : islunit_cat (join_mor l) (bot_mor l) :=
  pr1 (pr2 (pr2 (pr2 l))).

Definition islunit_meet_mor_top_mor : islunit_cat (meet_mor l) (top_mor l) :=
  pr2 (pr2 (pr2 (pr2 l))).

End BoundedLatticeObject_accessors.

Definition of sublattice objects

Section SublatticeObject.

Context {C : precategory} (BPC : BinProducts C) {M L : C}.
Context {i : CM,L} (Hi : isMonic i) (l : latticeob BPC L).

Local Notation "c ⊗ d" := (BinProductObject C (BPC c d)) : cat.
Local Notation "f '××' g" := (BinProductOfArrows _ _ _ f g) (at level 90) : cat.

This asserts that i is a lattice homomorphism internally
Context {meet_mor_M : CM M,M} (Hmeet : meet_mor_M · i = (i ×× i) · meet_mor l).
Context {join_mor_M : CM M,M} (Hjoin : join_mor_M · i = (i ×× i) · join_mor l).

Local Lemma identity_comm : identity M · i = i · identity L.
Proof.
  rewrite id_left, id_right. reflexivity.
Qed.

Local Lemma binprod_assoc_comm :
  ((i ×× i) ×× i) · @binprod_assoc _ BPC L L L =
  @binprod_assoc _ BPC M M M · (i ×× (i ×× i)).
Proof.
unfold binprod_assoc; rewrite postcompWithBinProductArrow.
apply BinProductArrowUnique.
- rewrite <-assoc, BinProductPr1Commutes.
  rewrite assoc, BinProductOfArrowsPr1, <- assoc, BinProductOfArrowsPr1, assoc.
  reflexivity.
- rewrite postcompWithBinProductArrow.
  apply BinProductArrowUnique.
  + etrans; [ apply cancel_postcomposition; rewrite <-assoc;
              apply maponpaths, BinProductPr2Commutes |].
    rewrite <- assoc, BinProductPr1Commutes.
    rewrite assoc, BinProductOfArrowsPr1, <- assoc, BinProductOfArrowsPr2, assoc.
    reflexivity.
  + etrans; [ apply cancel_postcomposition; rewrite <-assoc;
              apply maponpaths, BinProductPr2Commutes |].
    rewrite <- assoc, BinProductPr2Commutes, BinProductOfArrowsPr2.
    reflexivity.
Qed.

Local Lemma binprod_delta_comm :
  i · @binprod_delta _ BPC L = @binprod_delta _ BPC M · (i ×× i).
Proof.
unfold binprod_delta; rewrite postcompWithBinProductArrow.
apply BinProductArrowUnique.
- rewrite <-assoc, BinProductPr1Commutes, identity_comm. reflexivity.
- rewrite <-assoc, BinProductPr2Commutes, identity_comm. reflexivity.
Qed.

Local Lemma isassoc_cat_comm {f : CM M,M} {g : CL L,L} (Hfg : f · i = (i ×× i) · g) :
  isassoc_cat g isassoc_cat f.
Proof.
unfold isassoc_cat; intros H; apply Hi.
rewrite <-!assoc, !Hfg, !assoc, BinProductOfArrows_comp, Hfg, <- !assoc, identity_comm.
rewrite <- BinProductOfArrows_comp, <- assoc, H, !assoc.
apply cancel_postcomposition.
rewrite <-!assoc, BinProductOfArrows_comp, Hfg, identity_comm.
rewrite <- BinProductOfArrows_comp, !assoc, binprod_assoc_comm.
reflexivity.
Qed.

Local Lemma iscomm_cat_comm {f : CM M,M} {g : CL L,L} (Hfg : f · i = (i ×× i) · g) :
  iscomm_cat g iscomm_cat f.
Proof.
unfold iscomm_cat; intros H; apply Hi.
rewrite <- !assoc, !Hfg.
etrans; [eapply maponpaths, H|].
rewrite !assoc; apply cancel_postcomposition.
unfold binprod_swap; rewrite postcompWithBinProductArrow.
apply BinProductArrowUnique; rewrite <- assoc.
× now rewrite BinProductPr1Commutes, BinProductOfArrowsPr2.
× now rewrite BinProductPr2Commutes, BinProductOfArrowsPr1.
Qed.

Local Lemma isabsorb_cat_comm {f1 f2 : CM M,M} {g1 g2 : CL L,L}
  (Hfg1 : f1 · i = (i ×× i) · g1) (Hfg2 : f2 · i = (i ×× i) · g2) :
  isabsorb_cat g1 g2 isabsorb_cat f1 f2.
Proof.
unfold isabsorb_cat; intros H; apply Hi.
assert (HH : BinProductPr1 C (BPC M M) · i = (i ×× i) · BinProductPr1 C (BPC L L)).
{ now rewrite BinProductOfArrowsPr1. }
rewrite HH, <- H, <-!assoc, Hfg1, !assoc.
apply cancel_postcomposition.
rewrite <-!assoc, BinProductOfArrows_comp, Hfg2, identity_comm, !assoc.
rewrite BinProductOfArrows_comp, <-identity_comm, binprod_delta_comm.
etrans; [| eapply pathsinv0; do 2 apply cancel_postcomposition;
           now rewrite <-BinProductOfArrows_comp].
rewrite <-!assoc; apply maponpaths.
rewrite assoc, binprod_assoc_comm, <-assoc; apply maponpaths.
now rewrite identity_comm, BinProductOfArrows_comp.
Qed.

Definition sub_latticeob : latticeob BPC M.
Proof.
use mk_latticeob.
- apply meet_mor_M.
- apply join_mor_M.
- repeat split.
  + now apply (isassoc_cat_comm Hmeet), (isassoc_meet_mor _ l).
  + now apply (iscomm_cat_comm Hmeet), (iscomm_meet_mor _ l).
  + now apply (isassoc_cat_comm Hjoin), (isassoc_join_mor _ l).
  + now apply (iscomm_cat_comm Hjoin), (iscomm_join_mor _ l).
  + now apply (isabsorb_cat_comm Hmeet Hjoin), (meet_mor_absorb_join_mor _ l).
  + now apply (isabsorb_cat_comm Hjoin Hmeet), (join_mor_absorb_meet_mor _ l).
Defined.

End SublatticeObject.

Section SubboundedlatticeObject.

Context {C : precategory} (BPC : BinProducts C) (TC : Terminal C).
Context {M L : C} {i : CM,L} (Hi : isMonic i) (l : bounded_latticeob BPC TC L).

Local Notation "c ⊗ d" := (BinProductObject C (BPC c d)) : cat.
Local Notation "f '××' g" := (BinProductOfArrows _ _ _ f g) (at level 90) : cat.

Context {meet_mor_M : CM M,M} (Hmeet : meet_mor_M · i = (i ×× i) · meet_mor l).
Context {join_mor_M : CM M,M} (Hjoin : join_mor_M · i = (i ×× i) · join_mor l).
Context {bot_mor_M : CTC,M} (Hbot : bot_mor_M · i = bot_mor l).
Context {top_mor_M : CTC,M} (Htop : top_mor_M · i = top_mor l).

Lemma islunit_cat_comm
  {fM : CM M,M} {fL : CL L,L} (Hf : fM · i = (i ×× i) · fL)
  {gM : C TC,M} {gL : CTC,L} (Hg : gM · i = gL) :
  islunit_cat fL gL islunit_cat fM gM.
Proof.
unfold islunit_cat; intros H; apply Hi.
rewrite <-!assoc.
etrans; [ do 2 apply maponpaths; apply Hf |].
rewrite identity_comm, <-H, postcompWithBinProductArrow, !assoc.
apply cancel_postcomposition.
rewrite !postcompWithBinProductArrow, <-assoc, Hg, !id_left.
apply pathsinv0, BinProductArrowUnique.
- rewrite <- assoc, BinProductPr1Commutes, assoc.
  now apply cancel_postcomposition, TerminalArrowUnique.
- now rewrite <- assoc, BinProductPr2Commutes, id_right.
Qed.

Definition sub_bounded_latticeob : bounded_latticeob BPC TC M.
Proof.
use mk_bounded_latticeob.
- exact (sub_latticeob BPC Hi l Hmeet Hjoin).
- exact bot_mor_M.
- exact top_mor_M.
- split.
  + now apply (islunit_cat_comm Hjoin Hbot), (islunit_join_mor_bot_mor BPC TC l).
  + now apply (islunit_cat_comm Hmeet Htop), (islunit_meet_mor_top_mor BPC TC l).
Defined.

End SubboundedlatticeObject.