Mercurial > hg > Members > kono > Proof > category

changeset 1017:90224a662c4e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
two equalizers in Topos
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Mar 2021 17:58:57 +0900
parents bbbe97d2a5ea
children 4b517d46e987
files src/CCC.agda src/ToposEx.agda
diffstat 2 files changed, 45 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCC.agda	Tue Mar 23 14:41:47 2021 +0900
+++ b/src/CCC.agda	Tue Mar 23 17:58:57 2021 +0900
@@ -186,11 +186,11 @@
 -- pull back on
 --
 --     iso          ○ b
---  e ⇐====⇒  b -----------→ 1
+--  e ⇐====⇒  b -----------→ 1         
 --  |         |              |
 --  |       m |              | ⊤
---  |         ↓    char m    ↓
---  + ------→ a -----------→ Ω
+--  |         ↓    char m    ↓    Ker h = Equalizer (char m mono)  (⊤ ∙ ○ a )
+--  + ------→ a -----------→ Ω        m = Equalizer (char m mono)  (⊤ ∙ ○ a )
 --     ker h        h
 --
 open Equalizer
@@ -202,8 +202,6 @@
 
 open Mono
 
-open import equalizer
-
 record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) 
         ( Ω : Obj A )
         ( ⊤ : Hom A (CCC.１ c) Ω )
@@ -217,18 +215,49 @@
      ker h = equalizer (Ker h)
      mm : {a b : Obj A} → (m :  Hom A b a) → (mono : Mono A m ) → A [ A [ equalizer (Ker (char m mono)) o Iso.≅→ (IsoL.iso-L (ker-iso m mono)) ] ≈  m ]
      mm m mono = IsoL.L≈iso  (ker-iso m mono)
+     fe=ge : {a b : Obj A} → (m :  Hom A b a) → (mono : Mono A m ) →  A [ A [ char m mono o m ] ≈ A [ A [ ⊤ o CCC.○ c a ] o m ] ]
+     fe=ge {a} {b} m mono = begin
+        char m mono o m ≈↑⟨ cdr (mm m mono) ⟩
+        char m mono o (equalizer (Ker (char m mono)) o Iso.≅→ (IsoL.iso-L (ker-iso m mono))) ≈⟨ assoc ⟩
+        (char m mono o equalizer (Ker (char m mono))) o Iso.≅→ (IsoL.iso-L (ker-iso m mono)) ≈⟨ car ( IsEqualizer.fe=ge (Equalizer.isEqualizer (Ker (char m mono))) )  ⟩
+        (( ⊤ o CCC.○ c a) o equalizer (Ker (char m mono)) ) o Iso.≅→ (IsoL.iso-L (ker-iso m mono)) ≈↑⟨ assoc ⟩
+        ( ⊤ o CCC.○ c a) o (equalizer (Ker (char m mono))  o Iso.≅→ (IsoL.iso-L (ker-iso m mono))) ≈⟨ cdr (mm m mono)  ⟩
+        ( ⊤ o CCC.○ c a) o m ∎  where   open ≈-Reasoning A 
+     ek=h : {a b : Obj A} → (m :  Hom A b a) → (mono : Mono A m ) →  {d : Obj A} {h : Hom A d a}
+           {eq : A [ A [ char m mono o h ] ≈ A [ A [ ⊤ o CCC.○ c a ] o h ] ]} →
+            A [ A [ m o (A Category.o Iso.≅← (IsoL.iso-L (ker-iso m mono))) (IsEqualizer.k (isEqualizer (Ker (char m mono))) h eq) ] ≈ h ]
+     ek=h {a} {b} m mono {d} {h} {eq} = begin
+            m o (  Iso.≅← (IsoL.iso-L (ker-iso m mono)) o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h eq ) ≈↑⟨ car (mm m mono) ⟩
+            (equalizer (Ker (char m mono)) o Iso.≅→ (IsoL.iso-L (ker-iso m mono))) o (  Iso.≅← (IsoL.iso-L (ker-iso m mono)) o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h eq ) ≈↑⟨ assoc ⟩
+            _ o (Iso.≅→ (IsoL.iso-L (ker-iso m mono)) o (  Iso.≅← (IsoL.iso-L (ker-iso m mono)) o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h eq )) ≈⟨ cdr assoc ⟩
+            equalizer (Ker (char m mono)) o ((Iso.≅→ (IsoL.iso-L (ker-iso m mono)) o   Iso.≅← (IsoL.iso-L (ker-iso m mono))) o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h eq ) ≈⟨ cdr (car (Iso.iso←  (IsoL.iso-L (ker-iso m mono)))) ⟩
+            equalizer (Ker (char m mono)) o (id1 A _ o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h eq ) ≈⟨ cdr idL ⟩
+            equalizer (Ker (char m mono)) o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h eq  ≈⟨ IsEqualizer.ek=h (isEqualizer (Ker (char m mono))) ⟩
+            h ∎  where   open ≈-Reasoning A
+     uniqueness : {a b : Obj A} → (m :  Hom A b a) → (mono : Mono A m ) →  {d : Obj A} {h : Hom A d a}
+            {eq : A [ A [ char m mono o h ] ≈ A [ A [ ⊤ o CCC.○ c a ] o h ] ]}
+            {k' : Hom A d b} → A [ A [ m o k' ] ≈ h ]
+               → A [ (A Category.o Iso.≅← (IsoL.iso-L (ker-iso m mono))) (IsEqualizer.k (isEqualizer (Ker (char m mono))) h eq) ≈ k' ]
+     uniqueness {a} {b} m mono {d} {h} {eq} {k'} eqk = begin
+            Iso.≅← (IsoL.iso-L (ker-iso m mono))  o  (IsEqualizer.k (isEqualizer (Ker (char m mono))) h eq) ≈⟨ cdr ( IsEqualizer.uniqueness (Equalizer.isEqualizer (Ker (char m mono))) (  begin
+             equalizer (Ker (char m mono)) o ((Iso.≅→ (IsoL.iso-L (ker-iso m mono)))  o k' ) ≈⟨ assoc  ⟩
+             (equalizer (Ker (char m mono)) o Iso.≅→ (IsoL.iso-L (ker-iso m mono)))  o k'  ≈⟨ car (mm m mono)  ⟩
+             m o k' ≈⟨ eqk  ⟩
+             h ∎ ))   ⟩
+            Iso.≅← (IsoL.iso-L (ker-iso m mono)) o ( Iso.≅→ (IsoL.iso-L (ker-iso m mono)) o k' ) ≈⟨ assoc ⟩
+            (Iso.≅← (IsoL.iso-L (ker-iso m mono)) o  Iso.≅→ (IsoL.iso-L (ker-iso m mono)) ) o k'  ≈⟨ car (Iso.iso→  (IsoL.iso-L (ker-iso m mono)) )⟩
+            id1 A _ o k' ≈⟨  idL ⟩
+            k' ∎  where   open ≈-Reasoning A
      mequ : {a b : Obj A} → (m :  Hom A b a) → (mono : Mono A m ) → Equalizer A (char m mono)  (A [ ⊤ o (CCC.○ c a) ])
-     mequ {a} {b} m mono = record { equalizer-c = b ; equalizer = m ; isEqualizer = 
-            subst (λ k → IsEqualizer A k _ _ ) {!!} -- 
-              ( equalizer+iso (Ker (char m mono)) (Iso.≅→ (IsoL.iso-L (ker-iso m mono)))
-                 (Iso.≅← (IsoL.iso-L (ker-iso m mono))) (Iso.iso→ (IsoL.iso-L (ker-iso m mono))) (Iso.iso← (IsoL.iso-L (ker-iso m mono))) ) }
+     mequ {a} {b} m mono = record { equalizer-c = b ; equalizer =  m ; isEqualizer = record {
+           fe=ge = fe=ge m mono 
+         ; k = λ {d} h fh=gh → A [ Iso.≅← (IsoL.iso-L (ker-iso m mono)) o IsEqualizer.k (Equalizer.isEqualizer (Ker (char m mono))) h fh=gh ]
+         ; ek=h = ek=h m mono
+         ; uniqueness = uniqueness m mono
+         } }
      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 ≈⟨ {!!} ⟩
-            char (ker (char m mono) ) {!!} o m ≈⟨ {!!} ⟩
-            char m mono  o (ker (char m mono) o Iso.≅→ (IsoL.iso-L (ker-iso m mono))) ≈⟨ {!!} ⟩
-            (char m mono  o ker (char m mono) ) o Iso.≅→ (IsoL.iso-L (ker-iso m mono)) ≈⟨ {!!} ⟩
-            {!!} ≈⟨ {!!} ⟩
+            char m mono  o m ≈⟨ fe=ge m mono ⟩
             (⊤ o  CCC.○ c a) o m ≈↑⟨ assoc ⟩
             ⊤ o  (CCC.○ c a o m ) ≈⟨ cdr (IsCCC.e2 (CCC.isCCC c)) ⟩
             ⊤ o CCC.○ c b  ∎  where   open ≈-Reasoning A
--- a/src/ToposEx.agda	Tue Mar 23 14:41:47 2021 +0900
+++ b/src/ToposEx.agda	Tue Mar 23 17:58:57 2021 +0900
@@ -77,7 +77,7 @@
     ; π1 = m    
     ; π2 = ○ b   
     ; isPullback = record {
-              commute = ? -- char-m=⊤ t m mono
+              commute = IsTopos.char-m=⊤ (Topos.isTopos t) m mono
          ;    pullback = λ {d} {p1} {p2} eq →  f← o k  p1 p2 eq
          ;    π1p=π1 = λ {d} {p1'} {p2'} {eq} → lemma3 p1' p2' eq
          ;    π2p=π2 = λ {d} {p1'} {p2'} {eq} → trans-hom (IsCCC.e2 isCCC) (sym (IsCCC.e2 isCCC))
@@ -149,7 +149,7 @@
             char t < id1 A b , id1 A b > δmono o < f , f >  ≈↑⟨ cdr ( IsCCC.π-cong isCCC idL idL ) ⟩
             char t < id1 A b , id1 A b > δmono o < id1 A _ o f , id1 A _ o f >    ≈↑⟨ cdr ( IsCCC.distr-π isCCC ) ⟩
             char t < id1 A b , id1 A b > δmono o (< id1 A _ , id1 A _ > o f)   ≈⟨ assoc ⟩
-           (char t < id1 A b , id1 A b > δmono o < id1 A b , id1 A b > ) o f  ≈⟨ car ? ⟩
+           (char t < id1 A b , id1 A b > δmono o < id1 A b , id1 A b > ) o f  ≈⟨ car (IsTopos.char-m=⊤ (Topos.isTopos t) _  δmono ) ⟩
             (⊤ t o  ○  b)  o f  ≈↑⟨ assoc ⟩
             ⊤ t o  (○  b  o f)  ≈⟨ cdr (IsCCC.e2 isCCC)  ⟩
             ⊤ t o  ○  a  ∎