Mercurial > hg > Members > kono > Proof > category
changeset 977:8ffdc897f29b
fix Topos equalizer iso
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 02 Mar 2021 17:56:31 +0900 |
| parents | 73fd14a73d49 |
| children | db288effad97 |
| files | src/CCC.agda src/ToposEx.agda src/cat-utility.agda |
| diffstat | 3 files changed, 66 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- a/src/CCC.agda Tue Mar 02 09:48:12 2021 +0900 +++ b/src/CCC.agda Tue Mar 02 17:56:31 2021 +0900 @@ -171,7 +171,7 @@ field char-ker : {a b : Obj A } {h : Hom A a Ω} (m : Hom A b a) → (mono : Mono A m) → A [ char m mono ≈ h ] - ker-char : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → Iso A b ( equalizer-c (Ker ( char m mono ))) + ker-char : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → IsoL A m (equalizer (Ker ( char m mono ))) record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field
--- a/src/ToposEx.agda Tue Mar 02 09:48:12 2021 +0900 +++ b/src/ToposEx.agda Tue Mar 02 17:56:31 2021 +0900 @@ -21,6 +21,15 @@ -- -- Ker t h : Equalizer A h (A [ ⊤ o (○ a) ]) + mh=⊤ : {a d : Obj A} (h : Hom A a (Ω t)) (p1 : Hom A d a) (p2 : Hom A d １) (eq : A [ A [ h o p1 ] ≈ A [ ⊤ t o p2 ] ] ) + → A [ A [ h o p1 ] ≈ A [ A [ ⊤ t o ○ a ] o p1 ] ] + mh=⊤ {a} {d} h p1 p2 eq = begin + h o p1 ≈⟨ eq ⟩ + ⊤ t o p2 ≈⟨ cdr (IsCCC.e2 isCCC) ⟩ + ⊤ t o (○ d) ≈↑⟨ cdr (IsCCC.e2 isCCC) ⟩ + ⊤ t o ( ○ a o p1 ) ≈⟨ assoc ⟩ + (⊤ t o ○ a ) o p1 ∎ + topos-pullback : {a : Obj A} → (h : Hom A a (Ω t)) → Pullback A h (⊤ t) topos-pullback {a} h = record { ab = equalizer-c (Ker t h) -- b @@ -28,7 +37,7 @@ ; π2 = ○ ( equalizer-c (Ker t h) ) -- ○ b ; isPullback = record { commute = comm - ; pullback = λ {d} {p1} {p2} eq → IsEqualizer.k (isEqualizer (Ker t h)) p1 (lemma1 p1 p2 eq ) + ; pullback = λ {d} {p1} {p2} eq → IsEqualizer.k (isEqualizer (Ker t h)) p1 (mh=⊤ h p1 p2 eq ) ; π1p=π1 = IsEqualizer.ek=h (isEqualizer (Ker t h)) ; π2p=π2 = λ {d} {p1'} {p2'} {eq} → lemma2 eq ; uniqueness = uniq @@ -41,25 +50,17 @@ (⊤ t o ○ a ) o equalizer (Ker t h) ≈↑⟨ assoc ⟩ ⊤ t o (○ a o equalizer (Ker t h)) ≈⟨ cdr e2 ⟩ ⊤ t o ○ (equalizer-c (Ker t h)) ∎ - lemma1 : {d : Obj A} (p1 : Hom A d a) (p2 : Hom A d １) (eq : A [ A [ h o p1 ] ≈ A [ ⊤ t o p2 ] ] ) - → A [ A [ h o p1 ] ≈ A [ A [ ⊤ t o ○ a ] o p1 ] ] - lemma1 {d} p1 p2 eq = begin - h o p1 ≈⟨ eq ⟩ - ⊤ t o p2 ≈⟨ cdr e2 ⟩ - ⊤ t o (○ d) ≈↑⟨ cdr e2 ⟩ - ⊤ t o ( ○ a o p1 ) ≈⟨ assoc ⟩ - (⊤ t o ○ a ) o p1 ∎ lemma2 : {d : Obj A} {p1' : Hom A d a} {p2' : Hom A d １} (eq : A [ A [ h o p1' ] ≈ A [ ⊤ t o p2' ] ] ) - → A [ A [ ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(lemma1 p1' p2' eq) ] ≈ p2' ] + → A [ A [ ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(mh=⊤ h p1' p2' eq) ] ≈ p2' ] lemma2 {d} {p1'} {p2'} eq = begin - ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(lemma1 p1' p2' eq) ≈⟨ e2 ⟩ + ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(mh=⊤ h p1' p2' eq) ≈⟨ e2 ⟩ ○ d ≈↑⟨ e2 ⟩ p2' ∎ uniq : {d : Obj A} (p' : Hom A d (equalizer-c (Ker t h))) (π1' : Hom A d a) (π2' : Hom A d １) (eq : A [ A [ h o π1' ] ≈ A [ ⊤ t o π2' ] ]) (π1p=π1' : A [ A [ equalizer (Ker t h) o p' ] ≈ π1' ]) (π2p=π2' : A [ A [ ○ (equalizer-c (Ker t h)) o p' ] ≈ π2' ]) - → A [ IsEqualizer.k (isEqualizer (Ker t h)) π1' (lemma1 π1' π2' eq) ≈ p' ] + → A [ IsEqualizer.k (isEqualizer (Ker t h)) π1' (mh=⊤ h π1' π2' eq) ≈ p' ] uniq {d} (p') p1' p2' eq pe1 pe2 = begin - IsEqualizer.k (isEqualizer (Ker t h)) p1' (lemma1 p1' p2' eq) ≈⟨ IsEqualizer.uniqueness (isEqualizer (Ker t h)) pe1 ⟩ + IsEqualizer.k (isEqualizer (Ker t h)) p1' (mh=⊤ h p1' p2' eq) ≈⟨ IsEqualizer.uniqueness (isEqualizer (Ker t h)) pe1 ⟩ p' ∎ topos-m-pullback : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → Pullback A (char t m mono ) (⊤ t) @@ -69,12 +70,23 @@ ; π2 = ○ b ; isPullback = record { commute = char-m=⊤ t m mono - ; pullback = λ {d} {p1} {p2} eq → {!!} -- Iso.≅← (IsTopos.ker-char (isTopos t) ? ? ) -- IsEqualizer.k (isEqualizer (Ker t ?)) ? ? - ; π1p=π1 = {!!} -- IsEqualizer.ek=h (isEqualizer (Ker t h)) - ; π2p=π2 = {!!} -- λ {d} {p1'} {p2'} {eq} → lemma2 eq + ; pullback = λ {d} {p1} {p2} eq → + Iso.≅← (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono )) o IsEqualizer.k (isEqualizer (Ker t (char t m mono))) p1 (mh=⊤ (char t m mono) 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)) ; uniqueness = {!!} } } where + f← = Iso.≅← (IsoL.iso-L (IsTopos.ker-char (isTopos t) m mono )) + k : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) → A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] → Hom A d (equalizer-c (Ker t (char t m mono))) + k p1 p2 eq = IsEqualizer.k (isEqualizer (Ker t (char t m mono))) p1 (mh=⊤ (char t m mono) p1 p2 eq ) + lemma3 : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) + → (eq : A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] ) → m o (f← o k p1 p2 eq ) ≈ p1 + lemma3 {d} p1 p2 eq = begin + m o (f← o k p1 p2 eq ) ≈⟨ assoc ⟩ + (m o f← ) o k p1 p2 eq ≈⟨ car (IsoL.iso≈L (IsTopos.ker-char (isTopos t) m mono )) ⟩ + equalizer (Ker t (char t m mono)) o k p1 p2 eq ≈⟨ IsEqualizer.ek=h (isEqualizer (Ker t (char t m mono))) ⟩ + p1 ∎ δmono : {b : Obj A } → Mono A < id1 A b , id1 A b > δmono = record { @@ -112,10 +124,14 @@ ip = topos-m-pullback < id1 A b , id1 A b > δmono k : Hom A a b k = IsPullback.pullback (Pullback.isPullback ip ) eq - -- δb o (A Category.o Pullback.π1 ip) k ≈ ⊤ t o ○ a - -- Pullback.π1 ip o k ≈ < f , g > + p0 : δb o ( Pullback.π1 ip o k ) ≈ ⊤ t o ○ a + p0 = begin + δb o ( Pullback.π1 ip o k ) ≈⟨⟩ + char t < id1 A b , id1 A b > δmono o ( Pullback.π1 ip o k ) ≈⟨ {!!} ⟩ + char t < id1 A b , id1 A b > δmono o < f , g > ≈⟨ eq ⟩ + ⊤ t o ○ a ∎ pf : f ≈ id1 A b o k - pf = IsPullback.uniqueness (Pullback.isPullback ip ) k < f , g > (○ a) eq {!!} (IsCCC.e2 isCCC) + pf = {!!} -- IsPullback.uniqueness (Pullback.isPullback ip ) k (Pullback.π1 ip o k ) (○ a) p0 refl-hom (IsCCC.e2 isCCC) p2 : < f , g > ≈ ( < id1 A b , id1 A b > o k ) p2 = begin < f , g > ≈⟨ IsCCC.π-cong isCCC pf {!!} ⟩
--- a/src/cat-utility.agda Tue Mar 02 09:48:12 2021 +0900 +++ b/src/cat-utility.agda Tue Mar 02 17:56:31 2021 +0900 @@ -22,6 +22,36 @@ iso→ : C [ C [ ≅← o ≅→ ] ≈ id1 C x ] iso← : C [ C [ ≅→ o ≅← ] ≈ id1 C y ] + record IsoR {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) + {a b c : Obj C } + ( f : Hom C a b ) + ( g : Hom C a c ) + : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where + field + iso-R : Iso C b c + iso≈R : C [ C [ Iso.≅→ iso-R o f ] ≈ g ] + R≈iso : C [ C [ Iso.≅← iso-R o g ] ≈ f ] + R≈iso = begin Iso.≅← iso-R o g ≈↑⟨ cdr iso≈R ⟩ + Iso.≅← iso-R o (Iso.≅→ iso-R o f) ≈⟨ assoc ⟩ + (Iso.≅← iso-R o Iso.≅→ iso-R ) o f ≈⟨ car (Iso.iso→ iso-R ) ⟩ + id1 C _ o f ≈⟨ idL ⟩ + f ∎ where open ≈-Reasoning C + + record IsoL {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) + {a b c : Obj C } + ( f : Hom C b a ) + ( g : Hom C c a ) + : Set ( suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁)) where + field + iso-L : Iso C b c + iso≈L : C [ C [ f o Iso.≅← iso-L ] ≈ g ] + L≈iso : C [ C [ g o Iso.≅→ iso-L ] ≈ f ] + L≈iso = begin g o Iso.≅→ iso-L ≈↑⟨ car iso≈L ⟩ + (f o Iso.≅← iso-L ) o Iso.≅→ iso-L ≈↑⟨ assoc ⟩ + f o (Iso.≅← iso-L o Iso.≅→ iso-L ) ≈⟨ cdr (Iso.iso→ iso-L ) ⟩ + f o id1 C _ ≈⟨ idR ⟩ + f ∎ where open ≈-Reasoning C + record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A )