Mercurial > hg > Members > kono > Proof > category
changeset 1017:90224a662c4e
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.1 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 ∎