Ideals generated by subsets of rings
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Maša Žaucer.
Created on 2022-04-07.
Last modified on 2023-11-24.
module ring-theory.ideals-generated-by-subsets-rings where
Imports
open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.fibers-of-maps open import foundation.identity-types open import foundation.logical-equivalences open import foundation.powersets open import foundation.propositional-truncations open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.unions-subtypes open import foundation.universe-levels open import lists.concatenation-lists open import lists.functoriality-lists open import lists.lists open import order-theory.galois-connections-large-posets open import order-theory.least-upper-bounds-large-posets open import order-theory.order-preserving-maps-large-posets open import order-theory.order-preserving-maps-large-preorders open import order-theory.reflective-galois-connections-large-posets open import ring-theory.ideals-rings open import ring-theory.poset-of-ideals-rings open import ring-theory.rings open import ring-theory.subsets-rings
Idea
If S is a subset of a
ring R, then the (two-sided) ideal generated by
S is the least ideal containing S. This
idea expresses the universal property of the ideal generated by a subset of a
ring. We will construct it as the type of finite linear combinations of elements
in S. The operation S ↦ (S) which maps a subset S to the ideal generated
by S is the lower adjoint of a
galois connection between the
large poset of subsets of R and the large
poset of ideals of R.
Definitions
The universal property of ideals generated by a subset of a ring
module _ {l1 l2 l3 : Level} (R : Ring l1) (S : subset-Ring l2 R) (I : ideal-Ring l3 R) (H : S ⊆ subset-ideal-Ring R I) where is-ideal-generated-by-subset-Ring : UUω is-ideal-generated-by-subset-Ring = {l : Level} (J : ideal-Ring l R) → S ⊆ subset-ideal-Ring R J → leq-ideal-Ring R I J
The universal property of ideals generated by families of subsets of a ring
module _ {l1 l2 l3 l4 : Level} (R : Ring l1) {U : UU l2} (S : U → subset-Ring l3 R) (I : ideal-Ring l4 R) (H : (α : U) → S α ⊆ subset-ideal-Ring R I) where is-ideal-generated-by-family-of-subsets-Ring : UUω is-ideal-generated-by-family-of-subsets-Ring = {l : Level} (J : ideal-Ring l R) → ({α : U} → S α ⊆ subset-ideal-Ring R J) → leq-ideal-Ring R I J
The universal property of ideals generated by families of elements of a ring
module _ {l1 l2 l3 : Level} (R : Ring l1) {U : UU l2} (a : U → type-Ring R) (I : ideal-Ring l3 R) (H : (α : U) → is-in-ideal-Ring R I (a α)) where is-ideal-generated-by-family-of-elements-Ring : UUω is-ideal-generated-by-family-of-elements-Ring = {l : Level} (J : ideal-Ring l R) → ({α : U} → is-in-ideal-Ring R J (a α)) → leq-ideal-Ring R I J
Construction of the Galois connection of ideals generated by subsets
Ideals generated by subsets
module _ {l1 l2 : Level} (R : Ring l1) (S : subset-Ring l2 R) where formal-combination-subset-Ring : UU (l1 ⊔ l2) formal-combination-subset-Ring = list (type-Ring R × (type-subset-Ring R S × type-Ring R)) ev-formal-combination-subset-Ring : formal-combination-subset-Ring → type-Ring R ev-formal-combination-subset-Ring nil = zero-Ring R ev-formal-combination-subset-Ring (cons (x , s , y) l) = add-Ring R ( mul-Ring R (mul-Ring R x (inclusion-subset-Ring R S s)) y) ( ev-formal-combination-subset-Ring l) preserves-concat-ev-formal-combination-subset-Ring : (u v : formal-combination-subset-Ring) → ev-formal-combination-subset-Ring (concat-list u v) ＝ add-Ring R ( ev-formal-combination-subset-Ring u) ( ev-formal-combination-subset-Ring v) preserves-concat-ev-formal-combination-subset-Ring nil v = inv (left-unit-law-add-Ring R (ev-formal-combination-subset-Ring v)) preserves-concat-ev-formal-combination-subset-Ring (cons (x , s , y) u) v = ( ap ( add-Ring R ( mul-Ring R (mul-Ring R x (inclusion-subset-Ring R S s)) y)) ( preserves-concat-ev-formal-combination-subset-Ring u v)) ∙ ( inv ( associative-add-Ring R ( mul-Ring R (mul-Ring R x (inclusion-subset-Ring R S s)) y) ( ev-formal-combination-subset-Ring u) ( ev-formal-combination-subset-Ring v))) mul-formal-combination-subset-Ring : type-Ring R → formal-combination-subset-Ring → type-Ring R → formal-combination-subset-Ring mul-formal-combination-subset-Ring x l y = map-list (λ (u , s , v) → (mul-Ring R x u , s , mul-Ring R v y)) l preserves-mul-ev-formal-combination-subset-Ring : (x : type-Ring R) (u : formal-combination-subset-Ring) (y : type-Ring R) → ( ev-formal-combination-subset-Ring ( mul-formal-combination-subset-Ring x u y)) ＝ ( mul-Ring R (mul-Ring R x (ev-formal-combination-subset-Ring u)) y) preserves-mul-ev-formal-combination-subset-Ring x nil y = inv ( ( ap ( mul-Ring' R y) ( right-zero-law-mul-Ring R x)) ∙ ( left-zero-law-mul-Ring R y)) preserves-mul-ev-formal-combination-subset-Ring x ( cons (r , (s , H) , t) u) y = ( ap-add-Ring R ( ( inv ( associative-mul-Ring R ( mul-Ring R (mul-Ring R x r) s) ( t) ( y))) ∙ ( ap ( mul-Ring' R y) ( ( ap (mul-Ring' R t) (associative-mul-Ring R x r s)) ∙ ( associative-mul-Ring R x (mul-Ring R r s) t)))) ( preserves-mul-ev-formal-combination-subset-Ring x u y)) ∙ ( ( inv ( right-distributive-mul-add-Ring R ( mul-Ring R x ( mul-Ring R (mul-Ring R r s) t)) ( mul-Ring R x (ev-formal-combination-subset-Ring u)) ( y))) ∙ ( ap ( mul-Ring' R y) ( inv ( left-distributive-mul-add-Ring R x ( mul-Ring R (mul-Ring R r s) t) ( ev-formal-combination-subset-Ring u))))) subset-ideal-subset-Ring' : type-Ring R → UU (l1 ⊔ l2) subset-ideal-subset-Ring' x = fiber ev-formal-combination-subset-Ring x subset-ideal-subset-Ring : subset-Ring (l1 ⊔ l2) R subset-ideal-subset-Ring x = trunc-Prop (subset-ideal-subset-Ring' x) is-in-ideal-subset-Ring : type-Ring R → UU (l1 ⊔ l2) is-in-ideal-subset-Ring = is-in-subtype subset-ideal-subset-Ring contains-zero-ideal-subset-Ring : contains-zero-subset-Ring R subset-ideal-subset-Ring contains-zero-ideal-subset-Ring = unit-trunc-Prop (nil , refl) is-closed-under-addition-ideal-subset-Ring' : (x y : type-Ring R) → subset-ideal-subset-Ring' x → subset-ideal-subset-Ring' y → subset-ideal-subset-Ring' (add-Ring R x y) pr1 (is-closed-under-addition-ideal-subset-Ring' x y (l , H) (k , K)) = concat-list l k pr2 (is-closed-under-addition-ideal-subset-Ring' x y (l , H) (k , K)) = ( preserves-concat-ev-formal-combination-subset-Ring l k) ∙ ( ap-add-Ring R H K) is-closed-under-addition-ideal-subset-Ring : is-closed-under-addition-subset-Ring R subset-ideal-subset-Ring is-closed-under-addition-ideal-subset-Ring {x} {y} H K = apply-universal-property-trunc-Prop H ( subset-ideal-subset-Ring (add-Ring R x y)) ( λ H' → apply-universal-property-trunc-Prop K ( subset-ideal-subset-Ring (add-Ring R x y)) ( λ K' → unit-trunc-Prop ( is-closed-under-addition-ideal-subset-Ring' x y H' K'))) is-closed-under-multiplication-ideal-subset-Ring' : (r s t : type-Ring R) → subset-ideal-subset-Ring' s → subset-ideal-subset-Ring' (mul-Ring R (mul-Ring R r s) t) pr1 (is-closed-under-multiplication-ideal-subset-Ring' r s t (l , p)) = mul-formal-combination-subset-Ring r l t pr2 (is-closed-under-multiplication-ideal-subset-Ring' r s t (l , p)) = ( preserves-mul-ev-formal-combination-subset-Ring r l t) ∙ ( ap (λ u → mul-Ring R (mul-Ring R r u) t) p) is-closed-under-left-multiplication-ideal-subset-Ring : is-closed-under-left-multiplication-subset-Ring R subset-ideal-subset-Ring is-closed-under-left-multiplication-ideal-subset-Ring x r H = apply-universal-property-trunc-Prop H ( subset-ideal-subset-Ring (mul-Ring R x r)) ( λ H' → unit-trunc-Prop ( tr ( subset-ideal-subset-Ring') ( right-unit-law-mul-Ring R (mul-Ring R x r)) ( is-closed-under-multiplication-ideal-subset-Ring' x r ( one-Ring R) ( H')))) is-closed-under-right-multiplication-ideal-subset-Ring : is-closed-under-right-multiplication-subset-Ring R subset-ideal-subset-Ring is-closed-under-right-multiplication-ideal-subset-Ring x r H = apply-universal-property-trunc-Prop H ( subset-ideal-subset-Ring (mul-Ring R x r)) ( λ H' → unit-trunc-Prop ( tr ( subset-ideal-subset-Ring') ( ap ( mul-Ring' R r) ( left-unit-law-mul-Ring R x)) ( is-closed-under-multiplication-ideal-subset-Ring' ( one-Ring R) ( x) ( r) ( H')))) is-closed-under-negatives-ideal-subset-Ring : is-closed-under-negatives-subset-Ring R subset-ideal-subset-Ring is-closed-under-negatives-ideal-subset-Ring {x} H = tr ( is-in-ideal-subset-Ring) ( mul-neg-one-Ring R x) ( is-closed-under-left-multiplication-ideal-subset-Ring ( neg-one-Ring R) ( x) ( H)) ideal-subset-Ring : ideal-Ring (l1 ⊔ l2) R pr1 ideal-subset-Ring = subset-ideal-subset-Ring pr1 (pr1 (pr2 ideal-subset-Ring)) = contains-zero-ideal-subset-Ring pr1 (pr2 (pr1 (pr2 ideal-subset-Ring))) = is-closed-under-addition-ideal-subset-Ring pr2 (pr2 (pr1 (pr2 ideal-subset-Ring))) = is-closed-under-negatives-ideal-subset-Ring pr1 (pr2 (pr2 ideal-subset-Ring)) = is-closed-under-left-multiplication-ideal-subset-Ring pr2 (pr2 (pr2 ideal-subset-Ring)) = is-closed-under-right-multiplication-ideal-subset-Ring contains-subset-ideal-subset-Ring : S ⊆ subset-ideal-subset-Ring contains-subset-ideal-subset-Ring s H = unit-trunc-Prop ( ( cons (one-Ring R , (s , H) , one-Ring R) nil) , ( ( right-unit-law-add-Ring R _) ∙ ( right-unit-law-mul-Ring R _ ∙ left-unit-law-mul-Ring R _))) contains-formal-combinations-ideal-subset-Ring : {l3 : Level} (I : ideal-Ring l3 R) → S ⊆ subset-ideal-Ring R I → (x : formal-combination-subset-Ring) → is-in-ideal-Ring R I (ev-formal-combination-subset-Ring x) contains-formal-combinations-ideal-subset-Ring I H nil = contains-zero-ideal-Ring R I contains-formal-combinations-ideal-subset-Ring I H ( cons (r , (s , K) , t) c) = is-closed-under-addition-ideal-Ring R I ( is-closed-under-right-multiplication-ideal-Ring R I ( mul-Ring R r s) ( t) ( is-closed-under-left-multiplication-ideal-Ring R I r s (H s K))) ( contains-formal-combinations-ideal-subset-Ring I H c) is-ideal-generated-by-subset-ideal-subset-Ring : is-ideal-generated-by-subset-Ring R S ( ideal-subset-Ring) ( contains-subset-ideal-subset-Ring) is-ideal-generated-by-subset-ideal-subset-Ring J K x H = apply-universal-property-trunc-Prop H (subset-ideal-Ring R J x) P where P : subset-ideal-subset-Ring' x → is-in-ideal-Ring R J x P (c , refl) = contains-formal-combinations-ideal-subset-Ring J K c is-closed-under-eq-ideal-subset-Ring : {x y : type-Ring R} → is-in-ideal-subset-Ring x → (x ＝ y) → is-in-ideal-subset-Ring y is-closed-under-eq-ideal-subset-Ring = is-closed-under-eq-ideal-Ring R ideal-subset-Ring is-closed-under-eq-ideal-subset-Ring' : {x y : type-Ring R} → is-in-ideal-subset-Ring y → (x ＝ y) → is-in-ideal-subset-Ring x is-closed-under-eq-ideal-subset-Ring' = is-closed-under-eq-ideal-Ring' R ideal-subset-Ring
The subset relation is preserved by generating ideals
module _ {l1 : Level} (A : Ring l1) where preserves-order-ideal-subset-Ring : {l2 l3 : Level} (S : subset-Ring l2 A) (T : subset-Ring l3 A) → S ⊆ T → leq-ideal-Ring A ( ideal-subset-Ring A S) ( ideal-subset-Ring A T) preserves-order-ideal-subset-Ring S T H = is-ideal-generated-by-subset-ideal-subset-Ring A S ( ideal-subset-Ring A T) ( transitive-leq-subtype S T ( subset-ideal-subset-Ring A T) ( contains-subset-ideal-subset-Ring A T) ( H)) ideal-subset-hom-large-poset-Ring : hom-Large-Poset ( λ l2 → l1 ⊔ l2) ( powerset-Large-Poset (type-Ring A)) ( ideal-Ring-Large-Poset A) map-hom-Large-Preorder ideal-subset-hom-large-poset-Ring = ideal-subset-Ring A preserves-order-hom-Large-Preorder ideal-subset-hom-large-poset-Ring = preserves-order-ideal-subset-Ring
The Galois connection S ↦ (S)
module _ {l1 : Level} (A : Ring l1) where adjoint-relation-ideal-subset-Ring : {l2 l3 : Level} (S : subset-Ring l2 A) (I : ideal-Ring l3 A) → leq-ideal-Ring A (ideal-subset-Ring A S) I ↔ (S ⊆ subset-ideal-Ring A I) pr1 (adjoint-relation-ideal-subset-Ring S I) H = transitive-leq-subtype S ( subset-ideal-subset-Ring A S) ( subset-ideal-Ring A I) ( H) ( contains-subset-ideal-subset-Ring A S) pr2 (adjoint-relation-ideal-subset-Ring S I) = is-ideal-generated-by-subset-ideal-subset-Ring A S I ideal-subset-galois-connection-Ring : galois-connection-Large-Poset ( _⊔_ l1) (λ l → l) ( powerset-Large-Poset (type-Ring A)) ( ideal-Ring-Large-Poset A) lower-adjoint-galois-connection-Large-Poset ideal-subset-galois-connection-Ring = ideal-subset-hom-large-poset-Ring A upper-adjoint-galois-connection-Large-Poset ideal-subset-galois-connection-Ring = subset-ideal-hom-large-poset-Ring A adjoint-relation-galois-connection-Large-Poset ideal-subset-galois-connection-Ring = adjoint-relation-ideal-subset-Ring
The reflective Galois connection S ↦ (S)
module _ {l1 : Level} (A : Ring l1) where forward-inclusion-is-reflective-ideal-subset-galois-connection-Ring : {l2 : Level} (I : ideal-Ring l2 A) → leq-ideal-Ring A (ideal-subset-Ring A (subset-ideal-Ring A I)) I forward-inclusion-is-reflective-ideal-subset-galois-connection-Ring I = is-ideal-generated-by-subset-ideal-subset-Ring A ( subset-ideal-Ring A I) ( I) ( refl-leq-ideal-Ring A I) backward-inclusion-is-reflective-ideal-subset-galois-connection-Ring : {l2 : Level} (I : ideal-Ring l2 A) → leq-ideal-Ring A I (ideal-subset-Ring A (subset-ideal-Ring A I)) backward-inclusion-is-reflective-ideal-subset-galois-connection-Ring I = contains-subset-ideal-subset-Ring A (subset-ideal-Ring A I) is-reflective-ideal-subset-galois-connection-Ring : is-reflective-galois-connection-Large-Poset ( powerset-Large-Poset (type-Ring A)) ( ideal-Ring-Large-Poset A) ( ideal-subset-galois-connection-Ring A) pr1 (is-reflective-ideal-subset-galois-connection-Ring I) = forward-inclusion-is-reflective-ideal-subset-galois-connection-Ring I pr2 (is-reflective-ideal-subset-galois-connection-Ring I) = backward-inclusion-is-reflective-ideal-subset-galois-connection-Ring I ideal-subset-reflective-galois-connection-Ring : reflective-galois-connection-Large-Poset ( powerset-Large-Poset (type-Ring A)) ( ideal-Ring-Large-Poset A) galois-connection-reflective-galois-connection-Large-Poset ideal-subset-reflective-galois-connection-Ring = ideal-subset-galois-connection-Ring A is-reflective-reflective-galois-connection-Large-Poset ideal-subset-reflective-galois-connection-Ring = is-reflective-ideal-subset-galois-connection-Ring
The ideal generated by a family of subsets of a ring
module _ {l1 l2 l3 : Level} (R : Ring l1) {U : UU l2} (S : U → subset-Ring l3 R) where generating-subset-ideal-family-of-subsets-Ring : subset-Ring (l2 ⊔ l3) R generating-subset-ideal-family-of-subsets-Ring x = union-family-of-subtypes S x ideal-family-of-subsets-Ring : ideal-Ring (l1 ⊔ l2 ⊔ l3) R ideal-family-of-subsets-Ring = ideal-subset-Ring R generating-subset-ideal-family-of-subsets-Ring subset-ideal-family-of-subsets-Ring : subset-Ring (l1 ⊔ l2 ⊔ l3) R subset-ideal-family-of-subsets-Ring = subset-ideal-subset-Ring R generating-subset-ideal-family-of-subsets-Ring is-in-ideal-family-of-subsets-Ring : type-Ring R → UU (l1 ⊔ l2 ⊔ l3) is-in-ideal-family-of-subsets-Ring = is-in-ideal-subset-Ring R generating-subset-ideal-family-of-subsets-Ring contains-subset-ideal-family-of-subsets-Ring : {α : U} → (S α) ⊆ subset-ideal-family-of-subsets-Ring contains-subset-ideal-family-of-subsets-Ring {α} x H = contains-subset-ideal-subset-Ring R ( generating-subset-ideal-family-of-subsets-Ring) ( x) ( unit-trunc-Prop (α , H)) is-ideal-generated-by-family-of-subsets-ideal-family-of-subsets-Ring : is-ideal-generated-by-family-of-subsets-Ring R S ( ideal-family-of-subsets-Ring) ( λ α → contains-subset-ideal-family-of-subsets-Ring) is-ideal-generated-by-family-of-subsets-ideal-family-of-subsets-Ring J H = is-ideal-generated-by-subset-ideal-subset-Ring R ( generating-subset-ideal-family-of-subsets-Ring) ( J) ( λ y q → apply-universal-property-trunc-Prop q ( subset-ideal-Ring R J y) ( λ (α , K) → H y K))
The ideal generated by a family of elements in a ring
module _ {l1 l2 : Level} (R : Ring l1) {I : UU l1} (a : I → type-Ring R) where generating-subset-ideal-family-of-elements-Ring : subset-Ring l1 R generating-subset-ideal-family-of-elements-Ring x = trunc-Prop (fiber a x) ideal-family-of-elements-Ring : ideal-Ring l1 R ideal-family-of-elements-Ring = ideal-subset-Ring R generating-subset-ideal-family-of-elements-Ring subset-ideal-family-of-elements-Ring : subset-Ring l1 R subset-ideal-family-of-elements-Ring = subset-ideal-subset-Ring R generating-subset-ideal-family-of-elements-Ring is-in-ideal-family-of-elements-Ring : type-Ring R → UU l1 is-in-ideal-family-of-elements-Ring = is-in-ideal-subset-Ring R generating-subset-ideal-family-of-elements-Ring contains-element-ideal-family-of-elements-Ring : (i : I) → is-in-ideal-family-of-elements-Ring (a i) contains-element-ideal-family-of-elements-Ring i = contains-subset-ideal-subset-Ring R ( generating-subset-ideal-family-of-elements-Ring) ( a i) ( unit-trunc-Prop (i , refl)) abstract is-ideal-generated-by-family-of-elements-ideal-family-of-elements-Ring : is-ideal-generated-by-family-of-elements-Ring R a ideal-family-of-elements-Ring contains-element-ideal-family-of-elements-Ring is-ideal-generated-by-family-of-elements-ideal-family-of-elements-Ring J H = is-ideal-generated-by-subset-ideal-subset-Ring R ( generating-subset-ideal-family-of-elements-Ring) ( J) ( λ x p → apply-universal-property-trunc-Prop p ( subset-ideal-Ring R J x) ( λ where (i , refl) → H))
Properties
The ideal generated by the underlying subset of an ideal I is I itself
module _ {l1 l2 : Level} (R : Ring l1) (I : ideal-Ring l2 R) where cases-forward-inclusion-idempotent-ideal-subset-Ring : (l : formal-combination-subset-Ring R (subset-ideal-Ring R I)) → is-in-ideal-Ring R I ( ev-formal-combination-subset-Ring R (subset-ideal-Ring R I) ( l)) cases-forward-inclusion-idempotent-ideal-subset-Ring nil = contains-zero-ideal-Ring R I cases-forward-inclusion-idempotent-ideal-subset-Ring (cons (x , u , y) l) = is-closed-under-addition-ideal-Ring R I ( is-closed-under-right-multiplication-ideal-Ring R I _ _ ( is-closed-under-left-multiplication-ideal-Ring R I _ _ (pr2 u))) ( cases-forward-inclusion-idempotent-ideal-subset-Ring l) abstract forward-inclusion-idempotent-ideal-subset-Ring : leq-ideal-Ring R ( ideal-subset-Ring R (subset-ideal-Ring R I)) ( I) forward-inclusion-idempotent-ideal-subset-Ring x H = apply-universal-property-trunc-Prop H ( subset-ideal-Ring R I x) ( λ where ( l , refl) → cases-forward-inclusion-idempotent-ideal-subset-Ring l) backward-inclusion-idempotent-ideal-subset-Ring : leq-ideal-Ring R ( I) ( ideal-subset-Ring R (subset-ideal-Ring R I)) backward-inclusion-idempotent-ideal-subset-Ring = contains-subset-ideal-subset-Ring R (subset-ideal-Ring R I) idempotent-ideal-subset-Ring : has-same-elements-ideal-Ring R ( ideal-subset-Ring R (subset-ideal-Ring R I)) ( I) pr1 (idempotent-ideal-subset-Ring x) = forward-inclusion-idempotent-ideal-subset-Ring x pr2 (idempotent-ideal-subset-Ring x) = backward-inclusion-idempotent-ideal-subset-Ring x
The operation S ↦ (S) preserves least upper bounds
In ring-theory.joins-ideals-rings we will
convert this fact to the fact that S ↦ (S) preserves joins.
module _ {l1 l2 l3 : Level} (R : Ring l1) {U : UU l2} (S : U → subset-Ring l3 R) where preserves-least-upper-bounds-ideal-subset-Ring : {l4 : Level} (T : subset-Ring l4 R) → is-least-upper-bound-family-of-elements-Large-Poset ( powerset-Large-Poset (type-Ring R)) ( S) ( T) → is-least-upper-bound-family-of-elements-Large-Poset ( ideal-Ring-Large-Poset R) ( λ α → ideal-subset-Ring R (S α)) ( ideal-subset-Ring R T) preserves-least-upper-bounds-ideal-subset-Ring = preserves-join-lower-adjoint-galois-connection-Large-Poset ( powerset-Large-Poset (type-Ring R)) ( ideal-Ring-Large-Poset R) ( ideal-subset-galois-connection-Ring R) ( S)
Recent changes
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-11-24. Egbert Rijke. Abelianization (#877).
- 2023-10-19. Fredrik Bakke. Level-universe compatibility patch (#862).
- 2023-10-09. Fredrik Bakke and Egbert Rijke. Refactor library to use
λ where(#809). - 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).