transitive_iso.lean

import tactic.basic
import category_theory.category
open category_theory

universes u v

variables {C : Type u} [category.{v} C] {X Y Z : C}


structure are_isomorph (X Y: C) :=
  (arrow: X ⟶ Y)
  (inv: Y ⟶ X)
  (prop1: arrow ≫ inv = 𝟙 X)
  (prop2: inv ≫ arrow = 𝟙 Y)



lemma transitive_iso (iso_xy: are_isomorph X Y) (iso_yz: are_isomorph Y Z): are_isomorph X Z :=
begin
  exact { 
    arrow := iso_xy.arrow ≫ iso_yz.arrow,
    inv := iso_yz.inv ≫ iso_xy.inv,
    prop1 := 
      begin
        rw category.assoc,
        rw ← category.assoc iso_yz.arrow iso_yz.inv iso_xy.inv,
        rw iso_yz.prop1,
        rw category.id_comp,
        rw iso_xy.prop1,
      end ,
    prop2 :=
      begin
        rw category.assoc,
        rw ← category.assoc iso_xy.inv iso_xy.arrow iso_yz.arrow,
        rw iso_xy.prop2,
        rw category.id_comp,
        rw iso_yz.prop2,
      end
  }