From dceb89a633bff600cfe8a42debdb025ba5317467 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 16 Jul 2024 13:44:47 -0700 Subject: [PATCH 1/9] def: some properties of indexed products/coproducts --- src/Cat/Diagram/Coproduct/Indexed.lagda.md | 122 +++++++++++++ src/Cat/Diagram/Product/Indexed.lagda.md | 188 ++++++++++++++++----- 2 files changed, 264 insertions(+), 46 deletions(-) diff --git a/src/Cat/Diagram/Coproduct/Indexed.lagda.md b/src/Cat/Diagram/Coproduct/Indexed.lagda.md index 05a48b041..b599074f4 100644 --- a/src/Cat/Diagram/Coproduct/Indexed.lagda.md +++ b/src/Cat/Diagram/Coproduct/Indexed.lagda.md @@ -98,9 +98,131 @@ Lift-Indexed-coproduct → Indexed-coproduct {Idx = Lift ℓ' I} (F ⊙ Lift.lower) → Indexed-coproduct F Lift-Indexed-coproduct _ = Indexed-coproduct-≃ (Lift-≃ e⁻¹) + +is-indexed-coproduct-is-prop + : ∀ {ℓ'} {Idx : Type ℓ'} + → {F : Idx → C.Ob} {ΣF : C.Ob} {ι : ∀ idx → C.Hom (F idx) ΣF} + → is-prop (is-indexed-coproduct F ι) +is-indexed-coproduct-is-prop {Idx = Idx} {F} {ΣF} {ι} P Q = path where + open is-indexed-coproduct + + p : ∀ {X} → (f : ∀ i → C.Hom (F i) X) → P .match f ≡ Q .match f + p f = Q .unique f (λ i → P .commute) + + path : P ≡ Q + path i .match f = p f i + path i .commute {i = idx} {f = f} = + is-prop→pathp (λ i → C.Hom-set _ _ (p f i C.∘ ι idx) (f idx)) + (P .commute) + (Q .commute) i + path i .unique {h = h} f q = + is-prop→pathp (λ i → C.Hom-set _ _ h (p f i)) + (P .unique f q) + (Q .unique f q) i + +module _ {ℓ'} {Idx : Type ℓ'} {F : Idx → C.Ob} {P P' : Indexed-coproduct F} where + private + module P = Indexed-coproduct P + module P' = Indexed-coproduct P' + + Indexed-coproduct-path + : (p : P.ΣF ≡ P'.ΣF) + → (∀ idx → PathP (λ i → C.Hom (F idx) (p i)) (P.ι idx) (P'.ι idx)) + → P ≡ P' + Indexed-coproduct-path p q i .Indexed-coproduct.ΣF = p i + Indexed-coproduct-path p q i .Indexed-coproduct.ι idx = q idx i + Indexed-coproduct-path p q i .Indexed-coproduct.has-is-ic = + is-prop→pathp (λ i → is-indexed-coproduct-is-prop {ΣF = p i} {ι = λ idx → q idx i}) + P.has-is-ic + P'.has-is-ic i ``` --> +## Uniqueness + +As universal constructions, indexed coproducts are unique up to isomorphism. +The proof follows the usual pattern: we use the universal morphisms to +construct morphisms in both directions, and uniqueness ensures that these +maps form an isomorphism. + +```agda +is-indexed-coproduct→iso + : ∀ {ℓ'} {Idx : Type ℓ'} {F : Idx → C.Ob} + → {ΣF ΣF' : C.Ob} + → {ι : ∀ i → C.Hom (F i) ΣF} {ι' : ∀ i → C.Hom (F i) ΣF'} + → is-indexed-coproduct F ι + → is-indexed-coproduct F ι' + → ΣF C.≅ ΣF' +is-indexed-coproduct→iso {ι = ι} {ι' = ι'} ΣF-coprod ΣF'-coprod = + C.make-iso (ΣF.match ι') (ΣF'.match ι) + (ΣF'.unique₂ (λ i → C.pullr ΣF'.commute ∙ ΣF.commute ∙ sym (C.idl _))) + (ΣF.unique₂ (λ i → C.pullr ΣF.commute ∙ ΣF'.commute ∙ sym (C.idl _))) + where + module ΣF = is-indexed-coproduct ΣF-coprod + module ΣF' = is-indexed-coproduct ΣF'-coprod +``` + + + +## Properties + +Let $X : \Sigma A B \to \cC$ be a family of objects in $\cC$. If the +the indexed coproducts $\Sigma_{a, b : \Sigma A B} X_{a,b}$ and +$\Sigma_{a : A} \Sigma_{b : B(a)} X_{a, b}$ exists, then they are isomorphic. + +The formal statement of this is a bit of a mouthful, but all of these +arguments are just required to ensure that the various coproducts actually +exist. + +```agda +is-indexed-coproduct-assoc + : ∀ {κ κ'} {A : Type κ} {B : A → Type κ'} + → {X : Σ A B → C.Ob} + → {ΣᵃᵇX : C.Ob} {ΣᵃΣᵇX : C.Ob} {ΣᵇX : A → C.Ob} + → {ιᵃᵇ : (ab : Σ A B) → C.Hom (X ab) ΣᵃᵇX} + → {ιᵃ : ∀ a → C.Hom (ΣᵇX a) ΣᵃΣᵇX} + → {ιᵇ : ∀ a → (b : B a) → C.Hom (X (a , b)) (ΣᵇX a)} + → is-indexed-coproduct X ιᵃᵇ + → is-indexed-coproduct ΣᵇX ιᵃ + → (∀ a → is-indexed-coproduct (λ b → X (a , b)) (ιᵇ a)) + → ΣᵃᵇX C.≅ ΣᵃΣᵇX +``` + +Luckily, the proof of this fact is easier than the statement! Indexed +coproducts are unique up to isomorphism, so it suffices to show that +$\Sigma_{a : A} \Sigma_{b : B(a)} X_{a, b}$ is an indexed product +over $X$, which follows almost immediately from our hypotheses. + +```agda +is-indexed-coproduct-assoc {A = A} {B} {X} {ΣᵃΣᵇX = ΣᵃΣᵇX} {ιᵃ = ιᵃ} {ιᵇ} Σᵃᵇ ΣᵃΣᵇ Σᵇ = + is-indexed-coproduct→iso Σᵃᵇ Σᵃᵇ' + where + open is-indexed-coproduct + + ιᵃᵇ' : ∀ (ab : Σ A B) → C.Hom (X ab) ΣᵃΣᵇX + ιᵃᵇ' (a , b) = ιᵃ a C.∘ ιᵇ a b + + Σᵃᵇ' : is-indexed-coproduct X ιᵃᵇ' + Σᵃᵇ' .match f = ΣᵃΣᵇ .match λ a → Σᵇ a .match λ b → f (a , b) + Σᵃᵇ' .commute = C.pulll (ΣᵃΣᵇ .commute) ∙ Σᵇ _ .commute + Σᵃᵇ' .unique {h = h} f p = + ΣᵃΣᵇ .unique _ λ a → + Σᵇ _ .unique _ λ b → + sym (C.assoc _ _ _) ∙ p (a , b) +``` + + # Disjoint coproducts An indexed coproduct $\sum F$ is said to be **disjoint** if every one of diff --git a/src/Cat/Diagram/Product/Indexed.lagda.md b/src/Cat/Diagram/Product/Indexed.lagda.md index c674246f3..1588fa0de 100644 --- a/src/Cat/Diagram/Product/Indexed.lagda.md +++ b/src/Cat/Diagram/Product/Indexed.lagda.md @@ -112,6 +112,43 @@ Lift-Indexed-product → Indexed-product {Idx = Lift ℓ' I} (F ⊙ Lift.lower) → Indexed-product F Lift-Indexed-product _ = Indexed-product-≃ (Lift-≃ e⁻¹) + +is-indexed-product-is-prop + : ∀ {ℓ'} {Idx : Type ℓ'} + → {F : Idx → C.Ob} {ΠF : C.Ob} {π : ∀ idx → C.Hom ΠF (F idx)} + → is-prop (is-indexed-product F π) +is-indexed-product-is-prop {Idx = Idx} {F = F} {ΠF = ΠF} {π = π} P Q = path where + open is-indexed-product + + p : ∀ {X} → (f : (i : Idx) → C.Hom X (F i)) → P .tuple f ≡ Q .tuple f + p f = Q .unique f (λ idx → P .commute) + + path : P ≡ Q + path i .tuple f = p f i + path i .commute {i = idx} {f = f} = + is-prop→pathp (λ i → C.Hom-set _ _ (π idx C.∘ p f i) (f idx)) + (P .commute) + (Q .commute) i + path i .unique {h = h} f q = + is-prop→pathp (λ i → C.Hom-set _ _ h (p f i)) + (P .unique f q) + (Q .unique f q) i + +module _ {ℓ'} {Idx : Type ℓ'} {F : Idx → C.Ob} {P P' : Indexed-product F} where + private + module P = Indexed-product P + module P' = Indexed-product P' + + Indexed-product-path + : (p : P.ΠF ≡ P'.ΠF) + → (∀ idx → PathP (λ i → C.Hom (p i) (F idx)) (P.π idx) (P'.π idx)) + → P ≡ P' + Indexed-product-path p q i .Indexed-product.ΠF = p i + Indexed-product-path p q i .Indexed-product.π idx = q idx i + Indexed-product-path p q i .Indexed-product.has-is-ip = + is-prop→pathp (λ i → is-indexed-product-is-prop {ΠF = p i} {π = λ idx → q idx i}) + P.has-is-ip + P'.has-is-ip i ``` --> @@ -124,64 +161,72 @@ is (at most) a contractible space of indexed products of that diagram. And again as is traditional with universal constructions, the proof is surprisingly straightforward! -```agda -Indexed-product-unique - : ∀ {ℓ'} {I : Type ℓ'} (F : I → C.Ob) - → is-category C → is-prop (Indexed-product F) -Indexed-product-unique {I = I} F c-cat x y = p where - module x = Indexed-product x - module y = Indexed-product y -``` - -All we have to do --- "all" --- is exhibit an isomorphism between the -apices which commutes with the projection function in one direction, and -with the product with morphisms in the other. That's it! The isomorphism +First, a general result: if two objects are both indexed products over the +same family of objects, then those objects are isomorphic. This isomorphism is induced by the universal properties, and is readily seen to commute with both projections: ```agda - apices : x.ΠF C.≅ y.ΠF - apices = C.make-iso (y.tuple x.π) (x.tuple y.π) - ( y.unique y.π (λ i → C.pulll y.commute ∙ x.commute) - ∙ sym (y.unique y.π λ i → C.idr _) ) - ( x.unique x.π (λ i → C.pulll x.commute ∙ y.commute) - ∙ sym (x.unique x.π λ i → C.idr _)) -``` +is-indexed-product→iso + : ∀ {ℓ'} {Idx : Type ℓ'} {F : Idx → C.Ob} + → {ΠF ΠF' : C.Ob} + → {π : ∀ i → C.Hom ΠF (F i)} {π' : ∀ i → C.Hom ΠF' (F i)} + → is-indexed-product F π + → is-indexed-product F π' + → ΠF C.≅ ΠF' +is-indexed-product→iso {π = π} {π' = π'} ΠF-prod ΠF'-prod = + C.make-iso (ΠF'.tuple π) (ΠF.tuple π') + (ΠF'.unique₂ (λ i → C.pulll ΠF'.commute ∙ ΠF.commute ∙ sym (C.idr _))) + (ΠF.unique₂ λ i → C.pulll ΠF.commute ∙ ΠF'.commute ∙ sym (C.idr _)) + where + module ΠF = is-indexed-product ΠF-prod + module ΠF' = is-indexed-product ΠF'-prod -By the characterisation of paths-over in Hom-sets, we get paths-over -between the projection maps and the product maps: +``` + - pres' : ∀ {Y} (f : ∀ j → C.Hom Y (F j)) - → PathP (λ i → C.Hom Y (c-cat .to-path apices i)) (x.tuple f) (y.tuple f) - pres' f = - Univalent.Hom-pathp-reflr-iso c-cat (y.unique f λ j → C.pulll y.commute ∙ x.commute) +With that out of the way, we can proceed to show our original result! +First, note that paths between indexed products are determined by a +path between apices, and a corresponding path-over between projections. +We can upgrade the iso from our previous lemma into a path, so all that +remains is to construct the path-over. + +```agda +Indexed-product-unique + : ∀ {ℓ'} {I : Type ℓ'} (F : I → C.Ob) + → is-category C → is-prop (Indexed-product F) +Indexed-product-unique {I = I} F c-cat x y = + Indexed-product-path + (c-cat .to-path apices) + pres + where + module x = Indexed-product x + module y = Indexed-product y + + apices : x.ΠF C.≅ y.ΠF + apices = Indexed-product→iso x y ``` -And after some munging (dealing with the axioms), that's exactly what we -need to prove that indexed products are unique. +By the characterisation of paths-over in Hom-sets, we get paths-over +between the projection maps and the product maps: ```agda - open Indexed-product - open is-indexed-product - p : x ≡ y - p i .ΠF = c-cat .to-path apices i - p i .π j = pres j i - p i .has-is-ip .tuple f = pres' f i - p i .has-is-ip .commute {i = j} {f = f} = - is-prop→pathp (λ i → C.Hom-set _ (F j) (pres j i C.∘ pres' f i) _) - (x .has-is-ip .commute) (y .has-is-ip .commute) i - p i .has-is-ip .unique {h = h} f = - is-prop→pathp - (λ i → Π-is-hlevel {A = C.Hom _ (c-cat .to-path apices i)} 1 - λ h → Π-is-hlevel {A = ∀ j → pres j i C.∘ h ≡ f j} 1 - λ p → C.Hom-set _ (c-cat .to-path apices i) h (pres' f i)) - (λ h → x.unique {h = h} f) (λ h → y.unique {h = h} f) i h + module apices = C._≅_ apices + abstract + pres : ∀ j → PathP (λ i → C.Hom (c-cat .to-path apices i) (F j)) (x.π j) (y.π j) + pres j = Univalent.Hom-pathp-refll-iso c-cat x.commute ``` We can also prove the converse direction: if indexed products in $\cC$ are unique, @@ -233,3 +278,54 @@ lying over our isomorphism. cat .to-path = path cat .to-path-over = path-over ``` + +## Properties + +Let $X : \Sigma A B \to \cC$ be a family of objects in $\cC$. If the +the indexed products $\Pi_{a, b : \Sigma A B} X_{a,b}$ and +$\Pi_{a : A} \Pi_{b : B(a)} X_{a, b}$ exists, then they are isomorphic. + +```agda +is-indexed-product-assoc + : ∀ {κ κ'} {A : Type κ} {B : A → Type κ'} + → {X : Σ A B → C.Ob} + → {ΠᵃᵇX : C.Ob} {ΠᵃΠᵇX : C.Ob} {ΠᵇX : A → C.Ob} + → {πᵃᵇ : (ab : Σ A B) → C.Hom ΠᵃᵇX (X ab)} + → {πᵃ : ∀ a → C.Hom ΠᵃΠᵇX (ΠᵇX a)} + → {πᵇ : ∀ a → (b : B a) → C.Hom (ΠᵇX a) (X (a , b))} + → is-indexed-product X πᵃᵇ + → is-indexed-product ΠᵇX πᵃ + → (∀ a → is-indexed-product (λ b → X (a , b)) (πᵇ a)) + → ΠᵃᵇX C.≅ ΠᵃΠᵇX +``` + +The proof is surprisingly straightforward: as indexed products are +unique up to iso, it suffices to show that $\Pi_{a : A} \Pi_{b : B(a)} X_{a, b}$ +is an indexed product over $X$. + +```agda +is-indexed-product-assoc {A = A} {B} {X} {ΠᵃΠᵇX = ΠᵃΠᵇX} {πᵃ = πᵃ} {πᵇ} Πᵃᵇ ΠᵃΠᵇ Πᵇ = + is-indexed-product→iso Πᵃᵇ Πᵃᵇ' + where + open is-indexed-product +``` + +We can construct projections by composing the projections out of each +successive product. + +```agda + πᵃᵇ' : ∀ (ab : Σ A B) → C.Hom ΠᵃΠᵇX (X ab) + πᵃᵇ' (a , b) = πᵇ a b C.∘ πᵃ a +``` + +The rest of the structure follows a similar pattern. + +``` + Πᵃᵇ' : is-indexed-product X πᵃᵇ' + Πᵃᵇ' .tuple f = ΠᵃΠᵇ .tuple λ a → Πᵇ a .tuple λ b → f (a , b) + Πᵃᵇ' .commute = C.pullr (ΠᵃΠᵇ .commute) ∙ Πᵇ _ .commute + Πᵃᵇ' .unique {h = h} f p = + ΠᵃΠᵇ .unique _ λ a → + Πᵇ _ .unique _ λ b → + C.assoc _ _ _ ∙ p (a , b) +``` From 5c85e1fb31eb530aa3e280847e92f5868c3ad4ca Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 16 Jul 2024 14:09:24 -0700 Subject: [PATCH 2/9] def: some properties of equalisers --- src/Cat/Diagram/Equaliser.lagda.md | 70 ++++++++++++++++++++++++++++-- 1 file changed, 67 insertions(+), 3 deletions(-) diff --git a/src/Cat/Diagram/Equaliser.lagda.md b/src/Cat/Diagram/Equaliser.lagda.md index b960e3da8..0b8ee7cbd 100644 --- a/src/Cat/Diagram/Equaliser.lagda.md +++ b/src/Cat/Diagram/Equaliser.lagda.md @@ -39,12 +39,12 @@ right-hand-sides agree. : ∀ {F} {e' : Hom F A} {p : f ∘ e' ≡ g ∘ e'} {other : Hom F E} → equ ∘ other ≡ e' → other ≡ universal p - + equal-∘ : f ∘ equ ∘ h ≡ g ∘ equ ∘ h equal-∘ {h = h} = f ∘ equ ∘ h ≡⟨ extendl equal ⟩ g ∘ equ ∘ h ∎ - + unique₂ : ∀ {F} {e' : Hom F A} {o1 o2 : Hom F E} → f ∘ e' ≡ g ∘ e' @@ -77,7 +77,7 @@ its domain: {apex} : Ob equ : Hom apex A has-is-eq : is-equaliser f g equ - + open is-equaliser has-is-eq public ``` @@ -106,6 +106,70 @@ module _ {o ℓ} {C : Precategory o ℓ} where where open is-equaliser equalises ``` +## Uniqueness + +As universal constructions, equalisers are unique up to isomorphism. +The proof follows the usual pattern: if $E, E'$ both equalise $f, g : A \to B$, +then we can construct maps between $E$ and $E'$ via the universal property +of equalisers, and uniqueness ensures that these maps form an isomorphism. + +```agda + is-equaliser→iso + : {E E' : Ob} + → {e : Hom E A} {e' : Hom E' A} + → is-equaliser C f g e + → is-equaliser C f g e' + → E ≅ E' + is-equaliser→iso {e = e} {e' = e'} eq eq' = + make-iso (eq' .universal (eq .equal)) (eq .universal (eq' .equal)) + (unique₂ eq' (eq' .equal) (pulll (eq' .factors) ∙ eq .factors) (idr _)) + (unique₂ eq (eq .equal) (pulll (eq .factors) ∙ eq' .factors) (idr _)) + where open is-equaliser +``` + +## Properties of equalisers + +The equaliser of the pair $(f, f) : A \to B$ always exists, and is given +by the identity map $\id : A \to A$. + +```agda + id-is-equaliser : is-equaliser C f f id + id-is-equaliser .is-equaliser.equal = refl + id-is-equaliser .is-equaliser.universal {e' = e'} _ = e' + id-is-equaliser .is-equaliser.factors = idl _ + id-is-equaliser .is-equaliser.unique p = sym (idl _) ∙ p +``` + +If $e : E \to A$ is an equaliser and an [[epimorphism]], then $e$ is +an iso. + +```agda + equaliser+epi→invertible + : ∀ {E} {e : Hom E A} + → is-equaliser C f g e + → is-epic e + → is-invertible e +``` + +Suppose that $e$ equalises some pair $(f, g) : A \to B$. By definition, +this means that $f \circ e = g \circ e$; however, $e$ is an epi, so +$f = g$. This in turn means that $id : A \to A$ can be extended into +a map $A \to E$ via the universal property of $e$, and universality +ensures that this extension is an isomorphism! + +```agda + equaliser+epi→invertible {f = f} {g = g} {e = e} e-equaliser e-epi = + make-invertible + (universal {e' = id} (ap₂ _∘_ f≡g refl)) + factors + (unique₂ (ap₂ _∘_ f≡g refl) (pulll factors) id-comm) + where + open is-equaliser e-equaliser + f≡g : f ≡ g + f≡g = e-epi f g equal +``` + + # Categories with all equalisers We also define a helper module for working with categories that have From 3537c8df5b2543a46ba1a93f7f9b077f0823d62f Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 16 Jul 2024 15:29:55 -0700 Subject: [PATCH 3/9] def: properties of pullbacks, kernel pairs --- .../Diagram/Coequaliser/RegularEpi.lagda.md | 12 +- src/Cat/Diagram/Congruence.lagda.md | 12 +- src/Cat/Diagram/Pullback.lagda.md | 195 ++++++++++++++++++ src/Cat/Diagram/Pullback/Properties.lagda.md | 23 +++ src/Cat/Instances/Sets/Congruences.lagda.md | 10 +- src/Cat/Morphism.lagda.md | 2 +- 6 files changed, 236 insertions(+), 18 deletions(-) diff --git a/src/Cat/Diagram/Coequaliser/RegularEpi.lagda.md b/src/Cat/Diagram/Coequaliser/RegularEpi.lagda.md index 2549d8ae6..1c8d73af2 100644 --- a/src/Cat/Diagram/Coequaliser/RegularEpi.lagda.md +++ b/src/Cat/Diagram/Coequaliser/RegularEpi.lagda.md @@ -45,7 +45,7 @@ arrows $R \tto a$. {r} : Ob {arr₁} {arr₂} : Hom r a has-is-coeq : is-coequaliser C arr₁ arr₂ f - + open is-coequaliser has-is-coeq public ``` @@ -55,7 +55,7 @@ fact epic: ```agda is-regular-epi→is-epic : is-epic f is-regular-epi→is-epic = is-coequaliser→is-epic _ has-is-coeq - + open is-regular-epi using (is-regular-epi→is-epic) public ``` @@ -73,9 +73,9 @@ epis: field {kernel} : Ob p₁ p₂ : Hom kernel a - is-kernel-pair : is-pullback C p₁ f p₂ f + has-kernel-pair : is-kernel-pair C p₁ p₂ f has-is-coeq : is-coequaliser C p₁ p₂ f - + is-effective-epi→is-regular-epi : is-regular-epi f is-effective-epi→is-regular-epi = re where open is-regular-epi hiding (has-is-coeq) @@ -107,14 +107,14 @@ module _ {o ℓ} {C : Precategory o ℓ} where is-regular-epi→is-effective-epi {f = f} kp reg = epi where module reg = is-regular-epi reg module kp = Pullback kp - + open is-effective-epi open is-coequaliser epi : is-effective-epi C f epi .kernel = kp.apex epi .p₁ = kp.p₁ epi .p₂ = kp.p₂ - epi .is-kernel-pair = kp.has-is-pb + epi .has-kernel-pair = kp.has-is-pb epi .has-is-coeq .coequal = kp.square epi .has-is-coeq .universal {F = F} {e'} p = reg.universal q where q : e' ∘ reg.arr₁ ≡ e' ∘ reg.arr₂ diff --git a/src/Cat/Diagram/Congruence.lagda.md b/src/Cat/Diagram/Congruence.lagda.md index f8dd02e82..388615840 100644 --- a/src/Cat/Diagram/Congruence.lagda.md +++ b/src/Cat/Diagram/Congruence.lagda.md @@ -427,10 +427,10 @@ identifies _exactly those_ objects related by $R$, and no more. record is-effective-congruence {A} (R : Congruence-on A) : Type (o ⊔ ℓ) where private module R = Congruence-on R field - {A/R} : Ob - quotient : Hom A A/R - has-quotient : is-quotient-of R quotient - is-kernel-pair : is-pullback C R.rel₁ quotient R.rel₂ quotient + {A/R} : Ob + quotient : Hom A A/R + has-quotient : is-quotient-of R quotient + has-kernel-pair : is-kernel-pair C R.rel₁ R.rel₂ quotient ``` If $f$ is the coequaliser of its kernel pair --- that is, it is an @@ -454,7 +454,7 @@ kernel-pair-is-effective {a = a} {b} {f} quot = epi where epi .is-effective-congruence.A/R = b epi .quotient = f epi .has-quotient = quot - epi .is-kernel-pair = + epi .has-kernel-pair = transport (λ i → is-pullback C (a×a.π₁∘factor {p1 = pb.p₁} {p2 = pb.p₂} (~ i)) f (a×a.π₂∘factor {p1 = pb.p₁} {p2 = pb.p₂} (~ i)) f) @@ -471,6 +471,6 @@ kp-effective-congruence→effective-epi {f = f} cong = epi where epi .kernel = Kernel-pair _ .Congruence-on.domain epi .p₁ = _ epi .p₂ = _ - epi .is-kernel-pair = cong.is-kernel-pair + epi .has-kernel-pair = cong.has-kernel-pair epi .has-is-coeq = cong.has-quotient ``` diff --git a/src/Cat/Diagram/Pullback.lagda.md b/src/Cat/Diagram/Pullback.lagda.md index cb68b0d37..34f2e40a7 100644 --- a/src/Cat/Diagram/Pullback.lagda.md +++ b/src/Cat/Diagram/Pullback.lagda.md @@ -152,6 +152,201 @@ module _ {o ℓ} {C : Precategory o ℓ} where ``` --> +## Kernel pairs {defines="kernel-pair"} + +The **kernel pair** of a morphism $f : X \to Y$ (if it exists) is +the pullback of $f$ along itself. Intuitively, one should think +of a kernel pair as a partition of $X$ induced by the preimage of +$f$. + + + +```agda + is-kernel-pair : ∀ {P X Y} → Hom P X → Hom P X → Hom X Y → Type _ + is-kernel-pair p1 p2 f = is-pullback C p1 f p2 f +``` + + + +Note that each of the projections out of the kernel pair of $f$ are +[[epimorphisms]]. Without loss of generality, we will focus our +attention on the first projection. + + +```agda + is-kernel-pair→epil + : ∀ {p1 p2 : Hom P X} {f : Hom X Y} + → is-kernel-pair C p1 p2 f + → is-epic p1 +``` + +Recall that a morphism is epic if it has a [[section]]; that is, +some morphism $u$ such that $p_1 \circ u = id$. We can construct +such a $u$ by applying the universal property of the pullback to +the following diagram. + +~~~{.quiver} +\begin{tikzcd} + X \\ + & P && X \\ + \\ + & X && Y + \arrow["u", from=1-1, to=2-2] + \arrow["id", curve={height=-12pt}, from=1-1, to=2-4] + \arrow["id"', curve={height=12pt}, from=1-1, to=4-2] + \arrow["{p_2}", from=2-2, to=2-4] + \arrow["{p_1}"', from=2-2, to=4-2] + \arrow["f", from=2-4, to=4-4] + \arrow["f"', from=4-2, to=4-4] +\end{tikzcd} +~~~ + +```agda + is-kernel-pair→epil {p1 = p1} is-kp = + has-section→epic $ + make-section + (universal refl) + p₁∘universal + where open is-pullback is-kp +``` + + + +If $f$ is a [[monomorphism]], then its kernel pair always exists, and +is given by $(id, id)$. + +```agda + monic→id-kernel-pair + : ∀ {f : Hom X Y} + → is-monic f + → is-kernel-pair C id id f +``` + +Clearly, the square $f \circ id = f \circ id$ commutes, so the tricky +bit will be constructing a universal morphism. If $f \circ p_1 = f \circ p_2$ +for some $p_1, p_2 : P \to X$, then we can simply use one of $p_1$ or +$p_2$ for our universal map; the choice we make does not matter, as +we can obtain $p_1 = p_2$ from the fact that $f$ is monic! The rest +of the universal property follows directly from this lovely little observation. + +```agda + monic→id-kernel-pair {f = f} f-monic = id-kp where + open is-pullback + + id-kp : is-kernel-pair C id id f + id-kp .square = refl + id-kp .universal {p₁' = p₁'} _ = p₁' + id-kp .p₁∘universal = idl _ + id-kp .p₂∘universal {p = p} = idl _ ∙ f-monic _ _ p + id-kp .unique p q = sym (idl _) ∙ p +``` + +Conversely, if $(id, id)$ is the kernel pair of $f$, then $f$ is monic. +Suppose that $f \circ g = f \circ h$ for some $g, h : A \to X$, and +note that both $g$ and $h$ are equal to the universal map obtained via +the square $f \circ g = f \circ h$. + +```agda + id-kernel-pair→monic + : ∀ {f : Hom X Y} + → is-kernel-pair C id id f + → is-monic f + id-kernel-pair→monic {f = f} id-kp g h p = + g ≡˘⟨ p₁∘universal ⟩ + id ∘ universal p ≡⟨ p₂∘universal ⟩ + h ∎ + where open is-pullback id-kp +``` + +We can strengthen this result by noticing that if $(p, p)$ is the kernel +pair of $f$ for some $P : \cC, p : P \to X$, then $(id, id)$ is also +a kernel pair of $f$. + +```agda + same-kernel-pair→id-kernel-pair + : ∀ {P} {p : Hom P X} {f : Hom X Y} + → is-kernel-pair C p p f + → is-kernel-pair C id id f +``` + +As usual, the difficulty is constructing the universal map. Suppose +that $f \circ p_1 = f \circ p_2$ for some $P' : \cC, p_1, p_2 : P' \to X$, +as in the following diagram: + +~~~{.quiver} +\begin{tikzcd} + {P'} \\ + & P && X \\ + \\ + & X && Y + \arrow["{p_2}", curve={height=-12pt}, from=1-1, to=2-4] + \arrow["{p_1}"', curve={height=12pt}, from=1-1, to=4-2] + \arrow["p", from=2-2, to=2-4] + \arrow["p"', from=2-2, to=4-2] + \arrow["f", from=2-4, to=4-4] + \arrow["f"', from=4-2, to=4-4] +\end{tikzcd} +~~~ + +This diagram is conspicuously missing a morphism, so let's fill +it in by using the universal property of the kernel pair. + +~~~{.quiver} +\begin{tikzcd} + {P'} \\ + & P && X \\ + \\ + & X && Y + \arrow["u", dashed, from=1-1, to=2-2] + \arrow["{p_2}", curve={height=-12pt}, from=1-1, to=2-4] + \arrow["{p_1}"', curve={height=12pt}, from=1-1, to=4-2] + \arrow["p", from=2-2, to=2-4] + \arrow["p"', from=2-2, to=4-2] + \arrow["f", from=2-4, to=4-4] + \arrow["f"', from=4-2, to=4-4] +\end{tikzcd} +~~~ + +Next, note that $p \circ u$ factorizes both $p_1$ *and* $p_2$; moreover, +it is the unique such map! + +```agda + same-kernel-pair→id-kernel-pair {p = p} {f = f} p-kp = id-kp where + open is-pullback + + id-kp : is-kernel-pair C id id f + id-kp .square = refl + id-kp .universal q = p ∘ p-kp .universal q + id-kp .p₁∘universal {p = q} = idl _ ∙ p-kp .p₁∘universal + id-kp .p₂∘universal {p = q} = idl _ ∙ p-kp .p₂∘universal + id-kp .unique q r = (sym (idl _)) ∙ q ∙ sym (p-kp .p₁∘universal) +``` + # Categories with all pullbacks We also provide a helper module for working with categories that have all diff --git a/src/Cat/Diagram/Pullback/Properties.lagda.md b/src/Cat/Diagram/Pullback/Properties.lagda.md index fec089c8c..198a00950 100644 --- a/src/Cat/Diagram/Pullback/Properties.lagda.md +++ b/src/Cat/Diagram/Pullback/Properties.lagda.md @@ -247,6 +247,29 @@ Pullbacks additionally preserve monomorphisms, as shown below: eq = pb.unique₂ {p = extendl pb.square} r p refl refl ``` +A similar result holds for isomorphisms. + +```agda + is-invertible→pullback-is-invertible + : ∀ {x y z} {f : Hom x z} {g : Hom y z} {p} {p1 : Hom p x} {p2 : Hom p y} + → is-invertible f + → is-pullback C p1 f p2 g + → is-invertible p2 + is-invertible→pullback-is-invertible {f = f} {g} {p1 = p1} {p2} f-inv pb = + make-invertible + (pb.universal {p₁' = f.inv ∘ g} {p₂' = id} (cancell f.invl ∙ sym (idr _))) + pb.p₂∘universal + (pb.unique₂ {p = pulll (cancell f.invl)} + (pulll pb.p₁∘universal) + (cancell pb.p₂∘universal) + (idr _ ∙ introl f.invr ∙ extendr pb.square) + (idr _)) + where + module f = is-invertible f-inv + module pb = is-pullback pb +``` + + @@ -76,7 +76,7 @@ _◆_ : ∀ {F G : Functor D E} {H K : Functor C D} → F => G → H => K → F F∘ H => G F∘ K _◆_ {E = E} {F = F} {G} {H} {K} α β = nat module horizontal-comp where private module E = Cat.Reasoning E - open Fr + open Cat.Functor.Reasoning nat : F F∘ H => G F∘ K nat .η x = G .F₁ (β .η _) E.∘ α .η _ nat .is-natural x y f = @@ -147,6 +147,28 @@ module _ (p : Functor C C') where postcompose .F-∘ f g = ext λ _ → p .F-∘ _ _ ``` +We also remark that horizontal composition obeys a very handy interchange +law. + +```agda +◆-interchange + : {F H L : Functor B C} {G K M : Functor A B} + → (α : F => H) (β : G => K) + → (γ : H => L) (δ : K => M) + → (γ ◆ δ) ∘nt (α ◆ β) ≡ (γ ∘nt α) ◆ (δ ∘nt β) +◆-interchange {B = B} {C = C} {A = A} {H = H} {L = L} α β γ δ = ext λ j → + (L.₁ (δ .η _) C.∘ γ .η _) C.∘ H.₁ (β .η _) C.∘ α .η _ ≡⟨ C.extendl (sym (L.shuffler (sym (γ .is-natural _ _ _)))) ⟩ + L.₁ (δ .η _ B.∘ β .η _) C.∘ γ .η _ C.∘ α .η _ ∎ + where + module A = Cat.Reasoning A + module B = Cat.Reasoning B + module C = Cat.Reasoning C + module L = Cat.Functor.Reasoning L + module H = Cat.Functor.Reasoning H + open Functor +``` + + @@ -155,7 +177,7 @@ module _ (p : Functor C C') where ```agda module _ {F G : Functor C D} where open Cat.Morphism - open Fr + open Cat.Functor.Reasoning _◂ni_ : F ≅ⁿ G → (H : Functor B C) → (F F∘ H) ≅ⁿ (G F∘ H) (α ◂ni H) = make-iso _ (α .to ◂ H) (α .from ◂ H) From 54a5cdb815cf89859de2ba03e5677f93e06a773e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia?= Date: Wed, 17 Jul 2024 05:06:53 -0300 Subject: [PATCH 6/9] Update src/Cat/Diagram/Product/Indexed.lagda.md --- src/Cat/Diagram/Product/Indexed.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cat/Diagram/Product/Indexed.lagda.md b/src/Cat/Diagram/Product/Indexed.lagda.md index 3724c56cc..b69e0f162 100644 --- a/src/Cat/Diagram/Product/Indexed.lagda.md +++ b/src/Cat/Diagram/Product/Indexed.lagda.md @@ -314,7 +314,7 @@ successive product. The rest of the structure follows a similar pattern. -``` +```agda Πᵃᵇ' : is-indexed-product X πᵃᵇ' Πᵃᵇ' .tuple f = ΠᵃΠᵇ .tuple λ a → Πᵇ a .tuple λ b → f (a , b) Πᵃᵇ' .commute = C.pullr (ΠᵃΠᵇ .commute) ∙ Πᵇ _ .commute From a1c8a0627e8b991bac46c64cde84dfabea0660c0 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 17 Jul 2024 16:43:40 -0700 Subject: [PATCH 7/9] fix: use \id --- src/Cat/Diagram/Pullback.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cat/Diagram/Pullback.lagda.md b/src/Cat/Diagram/Pullback.lagda.md index 34f2e40a7..3d50044ef 100644 --- a/src/Cat/Diagram/Pullback.lagda.md +++ b/src/Cat/Diagram/Pullback.lagda.md @@ -193,7 +193,7 @@ attention on the first projection. ``` Recall that a morphism is epic if it has a [[section]]; that is, -some morphism $u$ such that $p_1 \circ u = id$. We can construct +some morphism $u$ such that $p_1 \circ u = \id$. We can construct such a $u$ by applying the universal property of the pullback to the following diagram. From 7ded93708d00c7b38c65e7ee31c0f4ba6ed98409 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Fri, 19 Jul 2024 09:50:46 -0300 Subject: [PATCH 8/9] fixup: use \id some more --- src/Cat/Diagram/Equaliser.lagda.md | 2 +- src/Cat/Diagram/Pullback.lagda.md | 25 +++++++++++++------------ 2 files changed, 14 insertions(+), 13 deletions(-) diff --git a/src/Cat/Diagram/Equaliser.lagda.md b/src/Cat/Diagram/Equaliser.lagda.md index 0b8ee7cbd..9e0b51d02 100644 --- a/src/Cat/Diagram/Equaliser.lagda.md +++ b/src/Cat/Diagram/Equaliser.lagda.md @@ -153,7 +153,7 @@ an iso. Suppose that $e$ equalises some pair $(f, g) : A \to B$. By definition, this means that $f \circ e = g \circ e$; however, $e$ is an epi, so -$f = g$. This in turn means that $id : A \to A$ can be extended into +$f = g$. This in turn means that $\id : A \to A$ can be extended into a map $A \to E$ via the universal property of $e$, and universality ensures that this extension is an isomorphism! diff --git a/src/Cat/Diagram/Pullback.lagda.md b/src/Cat/Diagram/Pullback.lagda.md index 3d50044ef..ae4b1d507 100644 --- a/src/Cat/Diagram/Pullback.lagda.md +++ b/src/Cat/Diagram/Pullback.lagda.md @@ -238,7 +238,7 @@ the following diagram. --> If $f$ is a [[monomorphism]], then its kernel pair always exists, and -is given by $(id, id)$. +is given by $(\id, \id)$. ```agda monic→id-kernel-pair @@ -248,11 +248,12 @@ is given by $(id, id)$. ``` Clearly, the square $f \circ id = f \circ id$ commutes, so the tricky -bit will be constructing a universal morphism. If $f \circ p_1 = f \circ p_2$ -for some $p_1, p_2 : P \to X$, then we can simply use one of $p_1$ or -$p_2$ for our universal map; the choice we make does not matter, as -we can obtain $p_1 = p_2$ from the fact that $f$ is monic! The rest -of the universal property follows directly from this lovely little observation. +bit will be constructing a universal morphism. If $f \circ p_1 = f \circ +p_2$ for some $p_1, p_2 : P \to X$, then we can simply use one of $p_1$ +or $p_2$ for our universal map; the choice we make does not matter, as +we can obtain $p_1 = p_2$ from the fact that $f$ is monic! The rest of +the universal property follows directly from this lovely little +observation. ```agda monic→id-kernel-pair {f = f} f-monic = id-kp where @@ -266,10 +267,10 @@ of the universal property follows directly from this lovely little observation. id-kp .unique p q = sym (idl _) ∙ p ``` -Conversely, if $(id, id)$ is the kernel pair of $f$, then $f$ is monic. -Suppose that $f \circ g = f \circ h$ for some $g, h : A \to X$, and -note that both $g$ and $h$ are equal to the universal map obtained via -the square $f \circ g = f \circ h$. +Conversely, if $(\id, \id)$ is the kernel pair of $f$, then $f$ is +monic. Suppose that $f \circ g = f \circ h$ for some $g, h : A \to X$, +and note that both $g$ and $h$ are equal to the universal map obtained +via the square $f \circ g = f \circ h$. ```agda id-kernel-pair→monic @@ -284,8 +285,8 @@ the square $f \circ g = f \circ h$. ``` We can strengthen this result by noticing that if $(p, p)$ is the kernel -pair of $f$ for some $P : \cC, p : P \to X$, then $(id, id)$ is also -a kernel pair of $f$. +pair of $f$ for some $P : \cC, p : P \to X$, then $(\id, \id)$ is also a +kernel pair of $f$. ```agda same-kernel-pair→id-kernel-pair From 7c0c34dbc78a2bf7d0f254ee150e962e2dbeefbe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Fri, 19 Jul 2024 09:51:36 -0300 Subject: [PATCH 9/9] fixup: one more --- src/Cat/Diagram/Pullback.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cat/Diagram/Pullback.lagda.md b/src/Cat/Diagram/Pullback.lagda.md index ae4b1d507..c588925b7 100644 --- a/src/Cat/Diagram/Pullback.lagda.md +++ b/src/Cat/Diagram/Pullback.lagda.md @@ -247,7 +247,7 @@ is given by $(\id, \id)$. → is-kernel-pair C id id f ``` -Clearly, the square $f \circ id = f \circ id$ commutes, so the tricky +Clearly, the square $f \circ \id = f \circ \id$ commutes, so the tricky bit will be constructing a universal morphism. If $f \circ p_1 = f \circ p_2$ for some $p_1, p_2 : P \to X$, then we can simply use one of $p_1$ or $p_2$ for our universal map; the choice we make does not matter, as