Mercurial > hg > Members > kono > Proof > category

changeset 1072:cf92383daef5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 08 May 2021 13:02:41 +0900
parents 167bb69baac9
children 785d8b2ba48f
files src/CCC.agda
diffstat 1 files changed, 25 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCC.agda	Sat May 08 12:37:01 2021 +0900
+++ b/src/CCC.agda	Sat May 08 13:02:41 2021 +0900
@@ -223,6 +223,21 @@
           if=ig : ( m o Iso.≅← i ) o f  ≈ ( m o Iso.≅← i ) o g  →  m o (Iso.≅← i o f ) ≈  m o ( Iso.≅← i o g ) 
           if=ig eq = trans-hom assoc (trans-hom eq (sym-hom assoc ) ) 
 
+iso-mono→ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {m : Hom A a b}  ( mono : Mono A m ) (i : Iso A c a ) → Mono A (A [ m o Iso.≅→ i ] )
+iso-mono→ A {a} {b} {c} {m} mono i = record { isMono = λ {d} f g → im f g } where
+     im : {d : Obj A} (f g : Hom A d c ) →   A [ A [ A [ m o Iso.≅→ i ]  o f ] ≈ A [  A [ m o Iso.≅→ i ] o g ] ] → A [ f ≈ g ]
+     im {d} f g mf=mg = begin
+       f ≈↑⟨ idL ⟩
+       id1 A _  o f ≈↑⟨ car (Iso.iso→ i)  ⟩
+       ( Iso.≅← i o Iso.≅→ i) o f ≈↑⟨ assoc ⟩
+        Iso.≅← i o (Iso.≅→ i  o f) ≈⟨ cdr ( Mono.isMono mono _ _ (if=ig mf=mg) ) ⟩
+        Iso.≅← i o (Iso.≅→ i  o g) ≈⟨ assoc ⟩
+       ( Iso.≅← i o Iso.≅→ i) o g ≈⟨ car (Iso.iso→ i) ⟩
+       id1 A _  o g ≈⟨ idL ⟩
+       g ∎  where
+          open ≈-Reasoning A
+          if=ig : ( m o Iso.≅→ i ) o f  ≈ ( m o Iso.≅→ i ) o g  →  m o (Iso.≅→ i o f ) ≈  m o ( Iso.≅→ i o g ) 
+          if=ig eq = trans-hom assoc (trans-hom eq (sym-hom assoc ) ) 
 
 record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) 
         ( Ω : Obj A )
@@ -231,7 +246,7 @@
         (char : {a b : Obj A} → (m :  Hom A b a) → Mono A m  → Hom A a Ω) :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
          ker-m : {a b : Obj A} → (m : Hom A b a ) → (mono : Mono A m) → IsEqualizer A m (char m mono) (A [ ⊤ o (CCC.○ c a) ])
-         char-iso  : {a b c : Obj A } {m : Hom A a b}  {h : Hom A  b Ω}( mono : Mono A m ) → ( i : Iso A a (equalizer-c (Ker h))  )
+         char-iso  : {a b : Obj A } {m : Hom A a b}  {h : Hom A  b Ω}( mono : Mono A m ) → ( i : Iso A a (equalizer-c (Ker h))  )
              → A [ char (A [ m o Iso.≅← i ]) (iso-mono A mono i) ≈ h ]
          char-cong  : {a b : Obj A } { m m' :  Hom A b a } { mono : Mono A m } { mono' : Mono A m' }
              → A [ m  ≈  m'  ] → A [ char m mono ≈ char m' mono'  ]
@@ -240,16 +255,18 @@
      char-uniqueness  : {a b : Obj A } {h : Hom A a Ω}  
              → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ]
      char-uniqueness {a} {b} {h}  = begin
-            char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈⟨ char-cong {!!} ⟩
-            char ( ( equalizer (Ker h)  o  Iso.≅→ (≡-iso A _))  o Iso.≅← (≡-iso A _) ) (≡-mono h) ≈⟨ char-iso (≡-mono→ h) (≡-iso A _) ⟩
+            char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈⟨ char-cong (
+              begin
+              equalizer (Ker h)  ≈↑⟨ idR ⟩
+              equalizer (Ker h) o id1 A _  ≈↑⟨ cdr (idR) ⟩
+              equalizer (Ker h) o ( id1 A _   o id1 A _ )  ≈⟨ assoc ⟩
+              (equalizer (Ker h)  o  Iso.≅→ (≡-iso A _))  o Iso.≅← (≡-iso A _) ∎ ) ⟩
+            char ( ( equalizer (Ker h)  o  Iso.≅→ (≡-iso A _))  o Iso.≅← (≡-iso A _) ) (iso-mono A (≡-mono→ h) (≡-iso A _)) ≈⟨ char-iso (≡-mono→ h) (≡-iso A _) ⟩
             h ∎  where
         open ≈-Reasoning A
-        ≡-mono : {a b : Obj A } (h : Hom A a Ω) →
-            Mono A ( ( equalizer (Ker h) o (Iso.≅→ (≡-iso A (equalizer-c (Ker h)))))   o Iso.≅← (≡-iso A (equalizer-c (Ker h)))) 
-        ≡-mono = {!!}
-        ≡-mono→ : {a b : Obj A } (h : Hom A a Ω) →
+        ≡-mono→ : {a : Obj A } (h : Hom A a Ω) →
             Mono A ( equalizer (Ker h) o (Iso.≅→ (≡-iso A (equalizer-c (Ker h)))))
-        ≡-mono→ = {!!}
+        ≡-mono→ {a} h = iso-mono→ A (record { isMono =  λ f g → monic (Ker h)}  ) (≡-iso A _)
      char-m=⊤ :  {a b : Obj A} → (m :  Hom A b a) → (mono : Mono A m) → A [ A [ char m mono  o m ] ≈ A [ ⊤ o CCC.○ c b ] ]
      char-m=⊤ {a} {b} m mono  = begin
             char m mono  o m ≈⟨ IsEqualizer.fe=ge (ker-m m mono)  ⟩