Grace/Cumulus/Category/Examples.g17

Open in Workbench Download source

Imports

Product · Set

Declarations

Source

1-- Examples of small categories2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Category.Examples8import Product9import Set1011theorem IsPreorder.relation (A r : Set)12  requires preorder : IsPreorder(A, r)13  shows RelationBetween(r, A, A)14proof15  obtain ⟨relation, reflexive, transitive⟩ := preorder16  exact relation1718theorem IsPreorder.reflexive (A r : Set)19  requires preorder : IsPreorder(A, r)20  shows ReflexiveOn(A, r)21proof22  obtain ⟨relation, reflexive, transitive⟩ := preorder23  exact reflexive2425theorem IsPreorder.transitive (A r : Set)26  requires preorder : IsPreorder(A, r)27  shows TransitiveOn(A, r)28proof29  obtain ⟨relation, reflexive, transitive⟩ := preorder30  exact transitive3132-- Every member of a relation on A is a related pair of members of A.33theorem RelationBetween.shape (A B r f : Set)34  requires relation : RelationBetween(r, A, B)35  requires fInR : f ∈ r36  shows ∃ x ∈ A, ∃ y ∈ B, f = (x, y) ∧ relates(r, x, y)37proof38  unfold RelationBetween at relation39  have bounded := relation with f, fInR40  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with bounded41  refine ⟨x, hx, y, hy, shape, ?_⟩42  unfold relates43  rwa ← shape4445-- A preorder (A, r) as a category: objects A, morphisms the related46-- pairs, composition by transitivity.47defgraph orderDom (A r : Set) (f ∈ r) : A := fst(f)48requires relation : RelationBetween(r, A, A)49proof50  obtain ⟨x, xInA, y, yInA, shape, related⟩ :=51    RelationBetween.shape with relation, member52  rw shape53  rw fst.pair54  exact xInA5556defgraph orderCod (A r : Set) (f ∈ r) : A := snd(f)57requires relation : RelationBetween(r, A, A)58proof59  obtain ⟨x, xInA, y, yInA, shape, related⟩ :=60    RelationBetween.shape with relation, member61  rw shape62  rw snd.pair63  exact yInA6465defgraph orderIdentity (A r : Set) (a ∈ A) : r := (a, a)66requires reflexive : ReflexiveOn(A, r)67proof68  have related := reflexive with a, member69  unfold relates at related70  exact related7172theorem orderDom.pair (A r x y : Set)73  requires relation : RelationBetween(r, A, A)74  requires related : relates(r, x, y)75  shows orderDom(A, r)((x, y)) = x76proof77  unfold relates at related78  have value := orderDom.value with relation, related79  rw value80  exact fst.pair at x, y8182theorem orderCod.pair (A r x y : Set)83  requires relation : RelationBetween(r, A, A)84  requires related : relates(r, x, y)85  shows orderCod(A, r)((x, y)) = y86proof87  unfold relates at related88  have value := orderCod.value with relation, related89  rw value90  exact snd.pair at x, y9192theorem orderIdentity.pair (A r a : Set)93  requires reflexive : ReflexiveOn(A, r)94  requires aInA : a ∈ A95  shows orderIdentity(A, r)(a) = (a, a)96proof97  exact orderIdentity.value with reflexive, aInA9899defgraph orderComposition (A r : Set)100    (p ∈ composablePairsOf(r, orderDom(A, r), orderCod(A, r))) : r :=101  (orderDom(A, r)(snd(p)), orderCod(A, r)(fst(p)))102requires preorder : IsPreorder(A, r)103proof104  have relation := IsPreorder.relation with preorder105  have transitive := IsPreorder.transitive with preorder106  obtain ⟨bounded, g, gInR, f, fInR, shape, composable⟩ :=107    composablePairsOf.membership.forward with member108  obtain ⟨y, yInA, z, zInA, gShape, gRelated⟩ :=109    RelationBetween.shape with relation, gInR110  obtain ⟨x, xInA, w, wInA, fShape, fRelated⟩ :=111    RelationBetween.shape with relation, fInR112  have domG := orderDom.pair with relation, gRelated113  have codF := orderCod.pair with relation, fRelated114  have domF := orderDom.pair with relation, fRelated115  have codG := orderCod.pair with relation, gRelated116  have middle : y = w by cc117  have related : relates(r, x, z)118    rw ← middle at fRelated119    exact transitive with x, xInA, y, yInA, z, zInA, fRelated, gRelated120  unfold relates at related121  rw shape122  rw [fst.pair, snd.pair, gShape, fShape, domF, codG]123  exact related124125theorem orderComposition.pair (A r x y z : Set)126  requires preorder : IsPreorder(A, r)127  requires first : relates(r, x, y)128  requires second : relates(r, y, z)129  shows orderComposition(A, r)((y, z), (x, y)) = (x, z)130proof131  have relation := IsPreorder.relation with preorder132  have gInR : (y, z) ∈ r := second133  have fInR : (x, y) ∈ r := first134  have domG := orderDom.pair with relation, second135  have codF := orderCod.pair with relation, first136  have domF := orderDom.pair with relation, first137  have codG := orderCod.pair with relation, second138  have composable : orderDom(A, r)((y, z)) = orderCod(A, r)((x, y)) by cc139  have pairIn := composablePairsOf.pair at r, orderDom(A, r), orderCod(A, r),140    (y, z), (x, y) with gInR, fInR, composable141  have value := orderComposition.value with preorder, pairIn142  have firstValue := fst.pair at (y, z), (x, y)143  have secondValue := snd.pair at (y, z), (x, y)144  unfold call2145  cc146147def orderCategory (A r : Set) : Set :=148  Category.mk(A, r, orderDom(A, r), orderCod(A, r), orderIdentity(A, r),149    orderComposition(A, r))150151theorem orderCategory.category (A r : Set)152  requires preorder : IsPreorder(A, r)153  shows Category(orderCategory(A, r))154proof155  have relation := IsPreorder.relation with preorder156  have reflexive := IsPreorder.reflexive with preorder157  have domFunction := orderDom.function with relation158  have codFunction := orderCod.function with relation159  have idFunction := orderIdentity.function with reflexive160  have compFunction := orderComposition.function with preorder161  unfold orderCategory162  apply Category.intro with domFunction, codFunction, idFunction, compFunction163  . intros a aInA164    have idValue := orderIdentity.pair with reflexive, aInA165    have related := reflexive with a, aInA166    have domValue := orderDom.pair with relation, related167    have codValue := orderCod.pair with relation, related168    rw idValue169    refine ⟨domValue, codValue⟩170  . intros g gInR f fInR composable171    obtain ⟨y, yInA, z, zInA, gShape, gRelated⟩ :=172      RelationBetween.shape with relation, gInR173    obtain ⟨x, xInA, w, wInA, fShape, fRelated⟩ :=174      RelationBetween.shape with relation, fInR175    have domG := orderDom.pair with relation, gRelated176    have codF := orderCod.pair with relation, fRelated177    have domF := orderDom.pair with relation, fRelated178    have codG := orderCod.pair with relation, gRelated179    have middle : y = w by cc180    rw ← middle at fRelated181    rw ← middle at fShape182    have composite := orderComposition.pair with preorder, fRelated, gRelated183    have transitive := IsPreorder.transitive with preorder184    have related := transitive with185      x, xInA, y, yInA, z, zInA, fRelated, gRelated186    have domComposite := orderDom.pair with relation, related187    have codComposite := orderCod.pair with relation, related188    rw [gShape, fShape, composite]189    refine ⟨?_, ?_⟩190    . cc191    . cc192  . intros f fInR193    obtain ⟨x, xInA, y, yInA, fShape, fRelated⟩ :=194      RelationBetween.shape with relation, fInR195    have domF := orderDom.pair with relation, fRelated196    have codF := orderCod.pair with relation, fRelated197    have xRelated := reflexive with x, xInA198    have yRelated := reflexive with y, yInA199    have xIdentity := orderIdentity.pair with reflexive, xInA200    have yIdentity := orderIdentity.pair with reflexive, yInA201    have leftComposite := orderComposition.pair with202      preorder, fRelated, yRelated203    have rightComposite := orderComposition.pair with204      preorder, xRelated, fRelated205    rw fShape206    rw [domF, codF, xIdentity, yIdentity]207    refine ⟨leftComposite, rightComposite⟩208  . intros h hInR g gInR f fInR outer inner209    obtain ⟨z, zInA, w, wInA, hShape, hRelated⟩ :=210      RelationBetween.shape with relation, hInR211    obtain ⟨y, yInA, v, vInA, gShape, gRelated⟩ :=212      RelationBetween.shape with relation, gInR213    obtain ⟨x, xInA, u, uInA, fShape, fRelated⟩ :=214      RelationBetween.shape with relation, fInR215    have domH := orderDom.pair with relation, hRelated216    have codG := orderCod.pair with relation, gRelated217    have domG := orderDom.pair with relation, gRelated218    have codF := orderCod.pair with relation, fRelated219    have outerMiddle : z = v by cc220    have innerMiddle : y = u by cc221    rw ← outerMiddle at gRelated222    rw ← outerMiddle at gShape223    rw ← innerMiddle at fRelated224    rw ← innerMiddle at fShape225    have transitive := IsPreorder.transitive with preorder226    have hgRelated := transitive with227      y, yInA, z, zInA, w, wInA, gRelated, hRelated228    have gfRelated := transitive with229      x, xInA, y, yInA, z, zInA, fRelated, gRelated230    have hg := orderComposition.pair with preorder, gRelated, hRelated231    have gf := orderComposition.pair with preorder, fRelated, gRelated232    have leftComposite := orderComposition.pair with233      preorder, fRelated, hgRelated234    have rightComposite := orderComposition.pair with235      preorder, gfRelated, hRelated236    rw [hShape, gShape, fShape, hg, gf, leftComposite, rightComposite]237    rfl238239-- The discrete category on a set: the identity relation is a preorder.240theorem identity.preorder (X : Set)241  shows IsPreorder(X, identity(X))242proof243  unfold IsPreorder244  refine ⟨identity.relation at X, ?_, ?_⟩245  . intros x xInX246    exact identity.relates with xInX247  . intros x xInX y yInX z zInX first second248    unfold relates at first249    obtain ⟨bound, a, aInX, shape⟩ := identity.membership.forward with first250    obtain ⟨xa, ya⟩ := orderedPair.injective with shape251    have same : x = y by cc252    rw same253    exact second254255def discreteCategory (X : Set) : Set := orderCategory(X, identity(X))256257theorem discreteCategory.category (X : Set)258  shows Category(discreteCategory(X))259proof260  have preorder := identity.preorder at X261  unfold discreteCategory262  exact orderCategory.category with preorder263264theorem discreteCategory.obj (X : Set)265  shows obj(discreteCategory(X)) = X266proof267  simp [discreteCategory, orderCategory, Category.mk.obj]268269theorem discreteCategory.mor (X : Set)270  shows mor(discreteCategory(X)) = identity(X)271proof272  simp [discreteCategory, orderCategory, Category.mk.mor]273274theorem discreteCategory.id (X : Set)275  shows id(discreteCategory(X)) = orderIdentity(X, identity(X))276proof277  simp [discreteCategory, orderCategory, Category.mk.id]278279theorem discreteCategory.morphism (X f : Set)280  requires fInM : f ∈ mor(discreteCategory(X))281  shows ∃ x ∈ X, f = id(discreteCategory(X))(x)282proof283  have preorder := identity.preorder at X284  have reflexive := IsPreorder.reflexive with preorder285  rw discreteCategory.mor at fInM286  obtain ⟨bound, x, xInX, shape⟩ := identity.membership.forward with fInM287  have idValue := orderIdentity.pair with reflexive, xInX288  refine ⟨x, xInX, ?_⟩289  rw [discreteCategory.id, idValue]290  exact shape291292theorem discreteCategory.isomorphism (X f : Set)293  requires fInM : f ∈ mor(discreteCategory(X))294  shows Isomorphism(discreteCategory(X), f)295proof296  have category := discreteCategory.category at X297  have xInObjects : ∀ x ∈ X, x ∈ obj(discreteCategory(X))298    intros x xInX299    rw discreteCategory.obj300    exact xInX301  obtain ⟨x, xInX, shape⟩ := discreteCategory.morphism with fInM302  have xInO := xInObjects with x, xInX303  rw shape304  exact Isomorphism.id with category, xInO305306-- A monoid as a category with one object, the carrier itself.307theorem composablePairsOf.constant (A c : Set)308  shows composablePairsOf(A, constantFunction(A, {A}, A),309    constantFunction(A, {A}, A)) = A × A310proof311  have selfIn := singleton.self at A312  ext p313  constructor314  . intro member315    obtain ⟨bounded, rest⟩ := composablePairsOf.membership.forward with member316    exact bounded317  . intro member318    obtain ⟨bound, g, gInA, f, fInA, shape⟩ := product.membership.forward with319      member320    have gValue := constantFunction.apply with gInA, selfIn321    have fValue := constantFunction.apply with fInA, selfIn322    have composable : constantFunction(A, {A}, A)(g) =323        constantFunction(A, {A}, A)(f) by cc324    rw shape325    exact composablePairsOf.pair with gInA, fInA, composable326327def monoidCategory (A op unit : Set) : Set :=328  Category.mk({A}, A, constantFunction(A, {A}, A), constantFunction(A, {A}, A),329    constantFunction({A}, A, unit), op)330331theorem monoidCategory.category (A op unit : Set)332  requires monoid : IsMonoid(A, op, unit)333  shows Category(monoidCategory(A, op, unit))334proof335  obtain ⟨semigroup, identity⟩ := monoid336  obtain ⟨magma, associative⟩ := semigroup337  obtain ⟨unitInA, identityLaws⟩ := identity338  unfold IsMagma at magma339  have selfIn := singleton.self at A340  have constant := constantFunction.function at A, {A}, A with selfIn341  have identities := constantFunction.function at {A}, A, unit with unitInA342  have pairs := composablePairsOf.constant at A, A343  have operation : op : composablePairsOf(A, constantFunction(A, {A}, A),344      constantFunction(A, {A}, A)) → A345    rw pairs346    exact magma347  have closed : ∀ g ∈ A, ∀ f ∈ A, op(g, f) ∈ A348    intros g gInA f fInA349    have pairIn := product.pair with gInA, fInA350    unfold call2351    exact FunctionBetween.apply_closed with magma, pairIn352  unfold monoidCategory353  apply Category.intro with constant, constant, identities, operation354  . intros a aInO355    have aValue := singleton.membership.forward with aInO356    have idValue := constantFunction.apply with aInO, unitInA357    have domValue := constantFunction.apply with unitInA, selfIn358    rw idValue359    rw domValue360    refine ⟨?_, ?_⟩361    . symm362      exact aValue363    . symm364      exact aValue365  . intros g gInA f fInA composable366    have gfInA := closed with g, gInA, f, fInA367    have gValue := constantFunction.apply with gInA, selfIn368    have fValue := constantFunction.apply with fInA, selfIn369    have gfValue := constantFunction.apply with gfInA, selfIn370    refine ⟨?_, ?_⟩371    . cc372    . cc373  . intros f fInA374    have fValue := constantFunction.apply with fInA, selfIn375    have idValue := constantFunction.apply with selfIn, unitInA376    obtain ⟨leftUnit, rightUnit⟩ := identityLaws with f, fInA377    rw fValue378    rw idValue379    refine ⟨leftUnit, rightUnit⟩380  . intros h hInA g gInA f fInA outer inner381    exact associative with h, hInA, g, gInA, f, fInA382