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/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/Equaliser.lagda.md b/src/Cat/Diagram/Equaliser.lagda.md index b960e3da8..9e0b51d02 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 diff --git a/src/Cat/Diagram/Product/Indexed.lagda.md b/src/Cat/Diagram/Product/Indexed.lagda.md index c674246f3..b69e0f162 100644 --- a/src/Cat/Diagram/Product/Indexed.lagda.md +++ b/src/Cat/Diagram/Product/Indexed.lagda.md @@ -71,12 +71,6 @@ record Indexed-product (F : Idx → C.Ob) : Type (o ⊔ ℓ ⊔ level-of Idx) wh π : ∀ i → C.Hom ΠF (F i) has-is-ip : is-indexed-product F π open is-indexed-product has-is-ip public - -has-products-indexed-by : ∀ {ℓ} (I : Type ℓ) → Type _ -has-products-indexed-by I = ∀ (F : I → C.Ob) → Indexed-product F - -has-indexed-products : ∀ ℓ → Type _ -has-indexed-products ℓ = ∀ {I : Type ℓ} → has-products-indexed-by I ``` @@ -124,64 +155,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: +``` + + +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. - 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) +```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 +272,72 @@ 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. + +```agda + Πᵃᵇ' : 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) +``` + +# Categories with all indexed products + +```agda +has-products-indexed-by : ∀ {ℓ} (I : Type ℓ) → Type _ +has-products-indexed-by I = ∀ (F : I → C.Ob) → Indexed-product F + +has-indexed-products : ∀ ℓ → Type _ +has-indexed-products ℓ = ∀ {I : Type ℓ} → has-products-indexed-by I + +module Indexed-products + {κ : Level} + (has-ip : has-indexed-products κ) + where + module Π {Idx : Type κ} (F : Idx → C.Ob) = Indexed-product (has-ip F) + + open Π renaming (commute to π-commute; unique to tuple-unique) public +``` diff --git a/src/Cat/Diagram/Pullback.lagda.md b/src/Cat/Diagram/Pullback.lagda.md index cb68b0d37..c588925b7 100644 --- a/src/Cat/Diagram/Pullback.lagda.md +++ b/src/Cat/Diagram/Pullback.lagda.md @@ -152,6 +152,202 @@ 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) diff --git a/src/Cat/Instances/Sets/Congruences.lagda.md b/src/Cat/Instances/Sets/Congruences.lagda.md index 6de1e79c3..1e5e255fc 100644 --- a/src/Cat/Instances/Sets/Congruences.lagda.md +++ b/src/Cat/Instances/Sets/Congruences.lagda.md @@ -90,17 +90,17 @@ Sets-effective-congruences {A = A} R = epi where epi .has-quotient .unique {F = F} path = funext (Coeq-elim-prop (λ x → F .is-tr _ _) (happly path)) - epi .is-kernel-pair .square = funext λ { x → quot (x , refl) } + epi .has-kernel-pair .square = funext λ { x → quot (x , refl) } - epi .is-kernel-pair .universal path x = undo (happly path x) .fst + epi .has-kernel-pair .universal path x = undo (happly path x) .fst - epi .is-kernel-pair .p₁∘universal {p = path} = + epi .has-kernel-pair .p₁∘universal {p = path} = funext (λ x → ap fst (undo (happly path x) .snd)) - epi .is-kernel-pair .p₂∘universal {p = path} = + epi .has-kernel-pair .p₂∘universal {p = path} = funext (λ x → ap snd (undo (happly path x) .snd)) - epi .is-kernel-pair .unique {p = p} q r = funext λ x → + epi .has-kernel-pair .unique {p = p} q r = funext λ x → let p = sym ( undo (happly p x) .snd ∙ Σ-pathp (happly (sym q) _) (happly (sym r) _)) in happly (R.has-is-monic {c = unit} _ _ (funext λ _ → p)) _ diff --git a/src/Cat/Morphism.lagda.md b/src/Cat/Morphism.lagda.md index d1ad6efc2..9cde3bd4c 100644 --- a/src/Cat/Morphism.lagda.md +++ b/src/Cat/Morphism.lagda.md @@ -153,7 +153,7 @@ epic-precomp-embedding epic = injective→is-embedding (Hom-set _ _) _ (epic _ _) ``` -## Sections +## Sections {defines=section} A morphism $s : B \to A$ is a section of another morphism $r : A \to B$ when $r \cdot s = id$. The intuition for this name is that $s$ picks