Mercurial > hg > Members > kono > Proof > category

comparison universal-mapping.agda @ 300:d6a6dd305da2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
arrow and lambda fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 29 Sep 2013 14:01:07 +0900
parents 63f6157a6a19
children a5f2ca67e7c5
comparison
equal deleted inserted replaced
299:8c72f5284bc8 300:d6a6dd305da2
340 340
341 -- Assuming 341 -- Assuming
342 -- naturality of left (Φ) 342 -- naturality of left (Φ)
343 -- k = Hom A b b' ; f' = k o f h Hom A a' a ; f' = f o h 343 -- k = Hom A b b' ; f' = k o f h Hom A a' a ; f' = f o h
344 -- left left 344 -- left left
345 -- f : Hom A F(a) b --------> f* : Hom B a U(b) f' : Hom A F(a')b -------> f'* : Hom B a' U(b) 345 -- f : Hom A F(a) b -------→ f* : Hom B a U(b) f' : Hom A F(a')b ------→ f'* : Hom B a' U(b)
346 -- | | | | 346 -- | | | |
347 -- |k* |U(k*) |F(h*) |h* 347 -- |k* |U(k*) |F(h*) |h*
348 -- v v v v 348 -- v v v v
349 -- f': Hom A F(a) b'-------> f'* : Hom B a U(b') f: Hom A F(a) b ---------> f* : Hom B a U(b) 349 -- f': Hom A F(a) b'------→ f'* : Hom B a U(b') f: Hom A F(a) b --------→ f* : Hom B a U(b)
350 -- left left 350 -- left left
351 351
352 record UnityOfOppsite {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 352 record UnityOfOppsite {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
353 ( U : Functor B A ) 353 ( U : Functor B A )
354 ( F : Functor A B ) 354 ( F : Functor A B )
357 right : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b 357 right : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b
358 left : {a : Obj A} { b : Obj B } → Hom B (FObj F a) b → Hom A a ( FObj U b ) 358 left : {a : Obj A} { b : Obj B } → Hom B (FObj F a) b → Hom A a ( FObj U b )
359 right-injective : {a : Obj A} { b : Obj B } → {f : Hom A a (FObj U b) } → A [ left ( right f ) ≈ f ] 359 right-injective : {a : Obj A} { b : Obj B } → {f : Hom A a (FObj U b) } → A [ left ( right f ) ≈ f ]
360 left-injective : {a : Obj A} { b : Obj B } → {f : Hom B (FObj F a) b } → B [ right ( left f ) ≈ f ] 360 left-injective : {a : Obj A} { b : Obj B } → {f : Hom B (FObj F a) b } → B [ right ( left f ) ≈ f ]
361 --- naturality of Φ 361 --- naturality of Φ
362 left-commute1 : {a : Obj A} {b b' : Obj B } -> 362 left-commute1 : {a : Obj A} {b b' : Obj B } →
363 { f : Hom B (FObj F a) b } -> { k : Hom B b b' } -> 363 { f : Hom B (FObj F a) b } → { k : Hom B b b' } →
364 A [ left ( B [ k o f ] ) ≈ A [ FMap U k o left f ] ] 364 A [ left ( B [ k o f ] ) ≈ A [ FMap U k o left f ] ]
365 left-commute2 : {a a' : Obj A} {b : Obj B } -> 365 left-commute2 : {a a' : Obj A} {b : Obj B } →
366 { f : Hom B (FObj F a) b } -> { h : Hom A a' a } -> 366 { f : Hom B (FObj F a) b } → { h : Hom A a' a } →
367 A [ left ( B [ f o FMap F h ] ) ≈ A [ left f o h ] ] 367 A [ left ( B [ f o FMap F h ] ) ≈ A [ left f o h ] ]
368 r-cong : {a : Obj A} { b : Obj B } → { f g : Hom A a ( FObj U b ) } → A [ f ≈ g ] → B [ right f ≈ right g ] 368 r-cong : {a : Obj A} { b : Obj B } → { f g : Hom A a ( FObj U b ) } → A [ f ≈ g ] → B [ right f ≈ right g ]
369 l-cong : {a : Obj A} { b : Obj B } → { f g : Hom B (FObj F a) b } → B [ f ≈ g ] → A [ left f ≈ left g ] 369 l-cong : {a : Obj A} { b : Obj B } → { f g : Hom B (FObj F a) b } → B [ f ≈ g ] → A [ left f ≈ left g ]
370 -- naturality of right (Φ-1) 370 -- naturality of right (Φ-1)
371 right-commute1 : {a : Obj A} {b b' : Obj B } -> 371 right-commute1 : {a : Obj A} {b b' : Obj B } →
372 { g : Hom A a (FObj U b)} -> { k : Hom B b b' } -> 372 { g : Hom A a (FObj U b)} → { k : Hom B b b' } →
373 B [ B [ k o right g ] ≈ right ( A [ FMap U k o g ] ) ] 373 B [ B [ k o right g ] ≈ right ( A [ FMap U k o g ] ) ]
374 right-commute1 {a} {b} {b'} {g} {k} = let open ≈-Reasoning (B) in 374 right-commute1 {a} {b} {b'} {g} {k} = let open ≈-Reasoning (B) in
375 begin 375 begin
376 k o right g 376 k o right g
377 ≈⟨ sym left-injective ⟩ 377 ≈⟨ sym left-injective ⟩
379 ≈⟨ r-cong left-commute1 ⟩ 379 ≈⟨ r-cong left-commute1 ⟩
380 right ( A [ FMap U k o left ( right g ) ] ) 380 right ( A [ FMap U k o left ( right g ) ] )
381 ≈⟨ r-cong (lemma-1 g k) ⟩ 381 ≈⟨ r-cong (lemma-1 g k) ⟩
382 right ( A [ FMap U k o g ] ) 382 right ( A [ FMap U k o g ] )
383 ∎ where 383 ∎ where
384 lemma-1 : {a : Obj A} {b b' : Obj B } -> 384 lemma-1 : {a : Obj A} {b b' : Obj B } →
385 ( g : Hom A a (FObj U b)) -> ( k : Hom B b b' ) -> 385 ( g : Hom A a (FObj U b)) → ( k : Hom B b b' ) →
386 A [ A [ FMap U k o left ( right g ) ] ≈ A [ FMap U k o g ] ] 386 A [ A [ FMap U k o left ( right g ) ] ≈ A [ FMap U k o g ] ]
387 lemma-1 g k = let open ≈-Reasoning (A) in 387 lemma-1 g k = let open ≈-Reasoning (A) in
388 begin 388 begin
389 FMap U k o left ( right g ) 389 FMap U k o left ( right g )
390 ≈⟨ cdr ( right-injective) ⟩ 390 ≈⟨ cdr ( right-injective) ⟩
391 FMap U k o g 391 FMap U k o g
392 ∎ 392 ∎
393 right-commute2 : {a a' : Obj A} {b : Obj B } -> 393 right-commute2 : {a a' : Obj A} {b : Obj B } →
394 { g : Hom A a (FObj U b) } -> { h : Hom A a' a } -> 394 { g : Hom A a (FObj U b) } → { h : Hom A a' a } →
395 B [ B [ right g o FMap F h ] ≈ right ( A [ g o h ] ) ] 395 B [ B [ right g o FMap F h ] ≈ right ( A [ g o h ] ) ]
396 right-commute2 {a} {a'} {b} {g} {h} = let open ≈-Reasoning (B) in 396 right-commute2 {a} {a'} {b} {g} {h} = let open ≈-Reasoning (B) in
397 begin 397 begin
398 right g o FMap F h 398 right g o FMap F h
399 ≈⟨ sym left-injective ⟩ 399 ≈⟨ sym left-injective ⟩
401 ≈⟨ r-cong left-commute2 ⟩ 401 ≈⟨ r-cong left-commute2 ⟩
402 right ( A [ left ( right g ) o h ] ) 402 right ( A [ left ( right g ) o h ] )
403 ≈⟨ r-cong ( lemma-2 g h ) ⟩ 403 ≈⟨ r-cong ( lemma-2 g h ) ⟩
404 right ( A [ g o h ] ) 404 right ( A [ g o h ] )
405 ∎ where 405 ∎ where
406 lemma-2 : {a a' : Obj A} {b : Obj B } -> 406 lemma-2 : {a a' : Obj A} {b : Obj B } →
407 ( g : Hom A a (FObj U b)) -> ( h : Hom A a' a ) -> 407 ( g : Hom A a (FObj U b)) → ( h : Hom A a' a ) →
408 A [ A [ left ( right g ) o h ] ≈ A [ g o h ] ] 408 A [ A [ left ( right g ) o h ] ≈ A [ g o h ] ]
409 lemma-2 g h = let open ≈-Reasoning (A) in car ( right-injective ) 409 lemma-2 g h = let open ≈-Reasoning (A) in car ( right-injective )
410 410
411 Adj2UO : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 411 Adj2UO : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
412 { U : Functor B A } 412 { U : Functor B A }
460 ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ 460 ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩
461 f o id1 B (FObj F a) 461 f o id1 B (FObj F a)
462 ≈⟨ idR ⟩ 462 ≈⟨ idR ⟩
463 f 463 f
464 ∎ 464 ∎
465 left-commute1 : {a : Obj A} {b b' : Obj B } -> 465 left-commute1 : {a : Obj A} {b b' : Obj B } →
466 { f : Hom B (FObj F a) b } -> { k : Hom B b b' } -> 466 { f : Hom B (FObj F a) b } → { k : Hom B b b' } →
467 A [ left ( B [ k o f ] ) ≈ A [ FMap U k o left f ] ] 467 A [ left ( B [ k o f ] ) ≈ A [ FMap U k o left f ] ]
468 left-commute1 {a} {b} {b'} {f} {k} = let open ≈-Reasoning (A) in 468 left-commute1 {a} {b} {b'} {f} {k} = let open ≈-Reasoning (A) in
469 begin 469 begin
470 left ( B [ k o f ] ) 470 left ( B [ k o f ] )
471 ≈⟨⟩ 471 ≈⟨⟩
475 ≈↑⟨ assoc ⟩ 475 ≈↑⟨ assoc ⟩
476 FMap U k o ( FMap U f o (TMap η a) ) 476 FMap U k o ( FMap U f o (TMap η a) )
477 ≈⟨⟩ 477 ≈⟨⟩
478 FMap U k o left f 478 FMap U k o left f
479 ∎ 479 ∎
480 left-commute2 : {a a' : Obj A} {b : Obj B } -> 480 left-commute2 : {a a' : Obj A} {b : Obj B } →
481 { f : Hom B (FObj F a) b } -> { h : Hom A a' a} -> 481 { f : Hom B (FObj F a) b } → { h : Hom A a' a} →
482 A [ left ( B [ f o FMap F h ] ) ≈ A [ left f o h ] ] 482 A [ left ( B [ f o FMap F h ] ) ≈ A [ left f o h ] ]
483 left-commute2 {a'} {a} {b} {f} {h} = let open ≈-Reasoning (A) in 483 left-commute2 {a'} {a} {b} {f} {h} = let open ≈-Reasoning (A) in
484 begin 484 begin
485 left ( B [ f o FMap F h ] ) 485 left ( B [ f o FMap F h ] )
486 ≈⟨⟩ 486 ≈⟨⟩
503 l-cong eq = let open ≈-Reasoning (A) in ( car ( fcong U eq ) ) 503 l-cong eq = let open ≈-Reasoning (A) in ( car ( fcong U eq ) )
504 504
505 505
506 open UnityOfOppsite 506 open UnityOfOppsite
507 507
508 -- f : a -----------> U(b) 508 -- f : a ----------→ U(b)
509 -- 1_F(a) :F(a) ---------> F(a) 509 -- 1_F(a) :F(a) --------→ F(a)
510 -- ε(b) = right uo (1_F(a)) :UF(b)---------> a 510 -- ε(b) = right uo (1_F(a)) :UF(b)--------→ a
511 -- η(a) = left uo (1_U(a)) : a -----------> FU(a) 511 -- η(a) = left uo (1_U(a)) : a ----------→ FU(a)
512 512
513 513
514 uo-η-map : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 514 uo-η-map : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
515 ( U : Functor B A ) 515 ( U : Functor B A )
516 ( F : Functor A B ) → 516 ( F : Functor A B ) →
524 uo-ε-map A B U F uo b = right uo ( id1 A (FObj U b) ) 524 uo-ε-map A B U F uo b = right uo ( id1 A (FObj U b) )
525 525
526 uo-solution : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 526 uo-solution : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
527 ( U : Functor B A ) 527 ( U : Functor B A )
528 ( F : Functor A B ) → 528 ( F : Functor A B ) →
529 ( uo : UnityOfOppsite A B U F) → {a : Obj A} {b : Obj B } -> 529 ( uo : UnityOfOppsite A B U F) → {a : Obj A} {b : Obj B } →
530 ( f : Hom A a (FObj U b )) -> Hom B (FObj F a) b 530 ( f : Hom A a (FObj U b )) → Hom B (FObj F a) b
531 uo-solution A B U F uo {a} {b} f = -- B [ right uo (id1 A (FObj U b)) o FMap F f ] 531 uo-solution A B U F uo {a} {b} f = -- B [ right uo (id1 A (FObj U b)) o FMap F f ]
532 right uo f 532 right uo f
533 533
534 -- F(ε(b)) o η(F(b)) 534 -- F(ε(b)) o η(F(b))
535 -- F( right uo (id1 A (FObj U b)) ) o left uo (id1 B (FObj F a)) ] == 1 535 -- F( right uo (id1 A (FObj U b)) ) o left uo (id1 B (FObj F a)) ] == 1