Mercurial > hg > Members > kono > Proof > category
changeset 258:281b8962abbe
simpler equalizer iso
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 16 Sep 2013 17:26:42 +0900 |
| parents | 99751fb809e0 |
| children | c442322d22b3 |
| files | equalizer.agda |
| diffstat | 1 files changed, 27 insertions(+), 92 deletions(-) [+] |
line wrap: on
line diff
--- a/equalizer.agda Sat Sep 14 11:21:42 2013 +0900 +++ b/equalizer.agda Mon Sep 16 17:26:42 2013 +0900 @@ -181,105 +181,40 @@ c-iso-l : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } { e' : Hom A c' a } ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) - → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) - → Hom A c c' -- should be e' = c-sio-l o e -c-iso-l {c} {c'} eqa eqa' keqa = equalizer keqa - -c-iso-r : { c c' a b : Obj A } {f g : Hom A a b } {e : Hom A c a } {e' : Hom A c' a} → ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) - → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) - → Hom A c' c -- e = c-sio-r o e' -c-iso-r {c} {c'} eqa eqa' keqa = k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) + → Hom A c c' +c-iso-l {c} {c'} eqa eqa' = k eqa' (equalizer eqa) ( fe=ge eqa ) - -- e' f - -- c'----------> a ------->b f e j = g e j - -- ^ g - -- |k h - -- | h = e(eqaj) o k jhek = jh (uniqueness) - -- | - -- c j o (k (eqa ef ef) j ) = id c h = e(eqaj) - -- - -- h j e f = h j e g → h = 'j e f - -- h = j e f -> j = j' - -- +c-iso-r : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } { e' : Hom A c' a } + ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) + → Hom A c' c +c-iso-r {c} {c'} eqa eqa' = k eqa (equalizer eqa') ( fe=ge eqa' ) -e←e' : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) - → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) - → A [ A [ e' o c-iso-l eqa eqa' keqa ] ≈ e ] -e←e' {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin - e' o c-iso-l eqa eqa' keqa - ≈⟨⟩ - e' o k eqa' e (fe=ge eqa) +c-iso-lr : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } { e' : Hom A c' a } + ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) → + A [ A [ c-iso-l eqa eqa' o c-iso-r eqa eqa' ] ≈ id1 A c' ] +c-iso-lr {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' = let open ≈-Reasoning (A) in begin + c-iso-l eqa eqa' o c-iso-r eqa eqa' ≈⟨⟩ - equalizer eqa' o k eqa' e (fe=ge eqa) - ≈⟨ ek=h eqa' ⟩ - e - ∎ - -e'←e : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) - → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) - → A [ A [ e o c-iso-r eqa eqa' keqa ] ≈ e' ] -e'←e {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin - e o c-iso-r eqa eqa' keqa - ≈⟨⟩ - e o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) - ≈↑⟨ car (ek=h eqa' ) ⟩ - ( equalizer eqa' o k eqa' e (fe=ge eqa) ) o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) - ≈⟨⟩ - ( e' o k eqa' e (fe=ge eqa) ) o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) - ≈↑⟨ assoc ⟩ - e' o (( k eqa' e (fe=ge eqa) ) o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ) - ≈⟨⟩ - e' o (equalizer keqa o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ) - ≈⟨ cdr ( ek=h keqa ) ⟩ - e' o id c' + k eqa' (equalizer eqa) ( fe=ge eqa ) o k eqa (equalizer eqa') ( fe=ge eqa' ) + ≈↑⟨ uniqueness eqa' ( begin + e' o ( k eqa' (equalizer eqa) (fe=ge eqa) o k eqa (equalizer eqa') (fe=ge eqa') ) + ≈⟨ assoc ⟩ + ( e' o k eqa' (equalizer eqa) (fe=ge eqa) ) o k eqa (equalizer eqa') (fe=ge eqa') + ≈⟨ car (ek=h eqa') ⟩ + e o k eqa (equalizer eqa') (fe=ge eqa') + ≈⟨ ek=h eqa ⟩ + e' + ∎ )⟩ + k eqa' e' ( fe=ge eqa' ) + ≈⟨ uniqueness eqa' ( begin + e' o id c' ≈⟨ idR ⟩ - e' - ∎ - --- e←e' e'←e e = e --- e'←e e←e e' = e' is enough for isomorphism but we can prove l o r = id also. - -c-iso→ : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) - → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) - → A [ A [ c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ] ≈ id1 A c' ] -c-iso→ {c} {c'} {a} {b} {f} {g} eqa eqa' keqa = let open ≈-Reasoning (A) in begin - c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa - ≈⟨⟩ - equalizer keqa o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) - ≈⟨ ek=h keqa ⟩ + e' + ∎ )⟩ id c' ∎ -c-iso← : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) - → ( keqa : Equalizer A (k eqa' e (fe=ge eqa )) (A [ f o e' ]) (A [ g o e' ]) ) - → ( keqa' : Equalizer A (k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )) (A [ f o e ]) (A [ g o e ]) ) - → A [ A [ c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ] ≈ id1 A c ] -c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' = let open ≈-Reasoning (A) in begin - c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa - ≈⟨⟩ - k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) o k eqa' e (fe=ge eqa ) - ≈⟨⟩ - equalizer keqa' o k eqa' e (fe=ge eqa ) - ≈⟨ cdr ( begin - k eqa' e (fe=ge eqa ) - ≈⟨ uniqueness eqa' ( begin - e' o k keqa' (id c) (f1=g1 (fe=ge eqa) (id c)) - ≈↑⟨ car (e'←e eqa eqa' keqa ) ⟩ - ( e o equalizer keqa' ) o k keqa' (id c) (f1=g1 (fe=ge eqa) (id c)) - ≈↑⟨ assoc ⟩ - e o ( equalizer keqa' o k keqa' (id c) (f1=g1 (fe=ge eqa) (id c))) - ≈⟨ cdr ( ek=h keqa' ) ⟩ - e o id c - ≈⟨ idR ⟩ - e - ∎ )⟩ - k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) ) - ∎ )⟩ - equalizer keqa' o k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) ) - ≈⟨ ek=h keqa' ⟩ - id c - ∎ - +-- c-iso-rl is obvious from the symmetry --------------------------------