Grace/Cumulus/Category/SetMorphism.g17

Open in Workbench Download source

Imports

Examples

Declarations

Source

1-- The category of sets below a universe2-- 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.SetMorphism8import Examples910-- Sets(U) is the category of the subsets of a universe set U with all11-- functions between them. A morphism f : A ⟶ B is the function graph of f12-- together with the entry (U ↦ B), which records the codomain: U is not a13-- member of any subset of U, so the entry leaves the values on A untouched,14-- and the codomain is read back as the value at U. A morphism therefore15-- applies to its arguments as an ordinary function, f(x), and composition16-- is composition of functions.17def setArrow (U B f : Set) : Set := adjoinMap(f, U, B)1819-- The underlying function of a morphism: its graph without the codomain20-- entry.21def setsMap (U m : Set) : Set := m ∖ {(U ↦ m(U))}2223theorem setArrow.membership (U B f p : Set)24  shows p ∈ setArrow(U, B, f) ↔ (p = (U ↦ B) ∨ p ∈ f)25proof26  simp [setArrow, adjoinMap, insert.membership]2728theorem universe.not_member (U A : Set)29  requires subset : A ⊆ U30  shows ¬U ∈ A31proof32  intro member33  have inSelf := subset with U, member34  have irreflexive := membership.irreflexive at U35  exact irreflexive with inSelf3637theorem setArrow.function (U A B f : Set)38  requires subset : A ⊆ U39  requires function : f : A → B40  shows setArrow(U, B, f) : insert(U, A) → insert(B, B)41proof42  have notIn := universe.not_member with subset43  unfold setArrow44  exact adjoinMap.function with function, notIn4546theorem setArrow.apply (U A B f x : Set)47  requires subset : A ⊆ U48  requires function : f : A → B49  requires xIn : x ∈ A50  shows setArrow(U, B, f)(x) = f(x)51proof52  have arrow := setArrow.function with subset, function53  have xInserted : x ∈ insert(U, A) := insert.contains with xIn54  have related := FunctionBetween.relates_apply with function, xIn55  have lifted := adjoinMap.relates_old at f, U, B, x, f(x) with related56  unfold setArrow at arrow57  unfold setArrow58  exact FunctionBetween.apply_value with arrow, xInserted, lifted5960theorem setArrow.codomain (U A B f : Set)61  requires subset : A ⊆ U62  requires function : f : A → B63  shows setArrow(U, B, f)(U) = B64proof65  have arrow := setArrow.function with subset, function66  have uInserted : U ∈ insert(U, A) := insert.self at U, A67  have related := adjoinMap.relates_new at f, U, B68  unfold setArrow at arrow69  unfold setArrow70  exact FunctionBetween.apply_value with arrow, uInserted, related7172theorem setArrow.map (U A B f : Set)73  requires subset : A ⊆ U74  requires function : f : A → B75  shows setsMap(U, setArrow(U, B, f)) = f76proof77  have codomain := setArrow.codomain with subset, function78  have notIn := universe.not_member with subset79  unfold setsMap80  rw codomain81  ext p82  constructor83  . intro member84    obtain ⟨inArrow, notEntry⟩ := difference.membership.forward with member85    have shape := setArrow.membership.forward with inArrow86    cases shape with entry | old87    . exfalso88      have isEntry : p ∈ {(U ↦ B)} by simp [entry]89      exact notEntry with isEntry90    . exact old91  . intro member92    apply difference.membership.backward93    constructor94    . apply setArrow.membership.backward95      right96      exact member97    . intro isEntry98      have entry : p = (U ↦ B) := singleton.membership.forward with isEntry99      obtain ⟨x, xInA, y, yInB, shape, related⟩ :=100        FunctionBetween.member_shape with function, member101      have same : (U, B) = (x, y) by cc102      have uIsX : U = x := orderedPair.first with same103      rw ← uIsX at xInA104      exact notIn with xInA105106-- A function with a two-sided inverse is a bijection.107theorem Bijective.of_two_sided_inverse (f g A B : Set)108  requires function : f : A → B109  requires inverse : g : B → A110  requires leftLaw : ∀ x ∈ A, g(f(x)) = x111  requires rightLaw : ∀ y ∈ B, f(g(y)) = y112  shows BijectiveBetween(f, A, B)113proof114  unfold BijectiveBetween115  constructor116  . unfold InjectiveBetween117    refine ⟨function, ?_⟩118    intros x hx y hy z hz relatesX relatesY119    have valueX := FunctionBetween.apply_value with function, hx, relatesX120    have valueY := FunctionBetween.apply_value with function, hy, relatesY121    have leftX := leftLaw with x, hx122    have leftY := leftLaw with y, hy123    cc124  . unfold SurjectiveBetween125    refine ⟨function, ?_⟩126    intros y hy127    have preimage := FunctionBetween.apply_closed with inverse, hy128    have edge := FunctionBetween.relates_apply with function, preimage129    have value := rightLaw with y, hy130    refine ⟨g(y), preimage, ?_⟩131    rwa value at edge132133-- The domain of a function graph is its domain of definition.134theorem FunctionBetween.domain (f A B : Set)135  requires function : f : A → B136  shows domain(f) = A137proof138  ext x139  constructor140  . intro member141    obtain ⟨bounded, y, pairIn⟩ := domain.membership.forward with member142    have related : relates(f, x, y) := pairIn143    obtain ⟨xInA, yInB⟩ := FunctionBetween.bounds with function, related144    exact xInA145  . intro xInA146    obtain ⟨y, yInB, related⟩ := FunctionBetween.exists_value with function, xInA147    have pairIn : (x, y) ∈ f := related148    have singletonIn : {x} ∈ (x, y) by simp [orderedPair, singleton, pair.membership]149    have inUnion : {x} ∈ ⋃ f := union.contains with pairIn, singletonIn150    have selfIn : x ∈ {x} := singleton.self at x151    have inBound : x ∈ ⋃ ⋃ f := union.contains with inUnion, selfIn152    have inCoordinates : x ∈ coordinateBound(f)153      unfold coordinateBound154      exact inBound155    apply domain.membership.backward156    refine ⟨inCoordinates, y, pairIn⟩157158theorem functionSpace.bounded (U A B f : Set)159  requires aIn : A ∈ 𝒫(U)160  requires bIn : B ∈ 𝒫(U)161  requires fIn : f ∈ functionSpace(A, B)162  shows f ∈ 𝒫(U × U)163proof164  have function := functionSpace.mem_iff.forward with fIn165  have graph : f ⊆ A × B := function.left166  have aSubset := powerset.membership_iff.forward with aIn167  have bSubset := powerset.membership_iff.forward with bIn168  have products := product.monotone with aSubset, bSubset169  have bounded := Subset.transitive with graph, products170  exact powerset.membership_iff.backward with bounded171172def setsBound (U : Set) : Set := (U × U) ∪ ({U} × 𝒫(U))173174def setsMorphisms (U : Set) : Set :=175  { m ∈ 𝒫(setsBound(U)) | ∃ A ∈ 𝒫(U), ∃ B ∈ 𝒫(U),176    ∃ f ∈ functionSpace(A, B), m = setArrow(U, B, f) }177178theorem setArrow.bounded (U A B f : Set)179  requires aIn : A ∈ 𝒫(U)180  requires bIn : B ∈ 𝒫(U)181  requires fIn : f ∈ functionSpace(A, B)182  shows setArrow(U, B, f) ∈ 𝒫(setsBound(U))183proof184  have fBounded := functionSpace.bounded with aIn, bIn, fIn185  have fSubset := powerset.membership_iff.forward with fBounded186  have selfIn := singleton.self at U187  have entryIn : (U, B) ∈ {U} × 𝒫(U) := product.pair with selfIn, bIn188  apply powerset.membership_iff.backward189  intros p member190  have shape := setArrow.membership.forward with member191  unfold setsBound192  apply union2.membership.backward193  cases shape with entry | old194  . right195    rw entry196    exact entryIn197  . left198    exact fSubset with p, old199200theorem setsMorphisms.arrow (U A B f : Set)201  requires aIn : A ∈ 𝒫(U)202  requires bIn : B ∈ 𝒫(U)203  requires fIn : f ∈ functionSpace(A, B)204  shows setArrow(U, B, f) ∈ setsMorphisms(U)205proof206  have bounded := setArrow.bounded with aIn, bIn, fIn207  apply setsMorphisms.membership.backward208  constructor209  . exact bounded210  . refine ⟨A, aIn, B, bIn, f, fIn, rfl⟩211212theorem setsMorphisms.shape (U m : Set)213  requires member : m ∈ setsMorphisms(U)214  shows ∃ A ∈ 𝒫(U), ∃ B ∈ 𝒫(U), ∃ f ∈ functionSpace(A, B), m = setArrow(U, B, f)215proof216  obtain ⟨bounded, rest⟩ := setsMorphisms.membership.forward with member217  exact rest218219-- The codomain of a morphism is its value at U; its domain is the domain220-- of its underlying function.221defgraph setsCod (U : Set) (m ∈ setsMorphisms(U)) : 𝒫(U) := m(U)222proof223  obtain ⟨A, aIn, B, bIn, f, fIn, shape⟩ := setsMorphisms.shape with member224  have subset := powerset.membership_iff.forward with aIn225  have function := functionSpace.mem_iff.forward with fIn226  have value := setArrow.codomain with subset, function227  rw shape228  rw value229  exact bIn230231defgraph setsDom (U : Set) (m ∈ setsMorphisms(U)) : 𝒫(U) := domain(setsMap(U, m))232proof233  obtain ⟨A, aIn, B, bIn, f, fIn, shape⟩ := setsMorphisms.shape with member234  have subset := powerset.membership_iff.forward with aIn235  have function := functionSpace.mem_iff.forward with fIn236  have underlying := setArrow.map with subset, function237  have domainValue := FunctionBetween.domain with function238  rw shape239  rw [underlying, domainValue]240  exact aIn241242theorem setsCod.arrow (U A B f : Set)243  requires aIn : A ∈ 𝒫(U)244  requires bIn : B ∈ 𝒫(U)245  requires fIn : f ∈ functionSpace(A, B)246  shows setsCod(U)(setArrow(U, B, f)) = B247proof248  have member := setsMorphisms.arrow with aIn, bIn, fIn249  have subset := powerset.membership_iff.forward with aIn250  have function := functionSpace.mem_iff.forward with fIn251  have value := setsCod.value with member252  have codomain := setArrow.codomain with subset, function253  rw value254  exact codomain255256theorem setsDom.arrow (U A B f : Set)257  requires aIn : A ∈ 𝒫(U)258  requires bIn : B ∈ 𝒫(U)259  requires fIn : f ∈ functionSpace(A, B)260  shows setsDom(U)(setArrow(U, B, f)) = A261proof262  have member := setsMorphisms.arrow with aIn, bIn, fIn263  have subset := powerset.membership_iff.forward with aIn264  have function := functionSpace.mem_iff.forward with fIn265  have value := setsDom.value with member266  have underlying := setArrow.map with subset, function267  have domainValue := FunctionBetween.domain with function268  rw value269  rw underlying270  exact domainValue271272theorem setsMap.arrow (U A B f : Set)273  requires aIn : A ∈ 𝒫(U)274  requires fIn : f ∈ functionSpace(A, B)275  shows setsMap(U, setArrow(U, B, f)) = f276proof277  have subset := powerset.membership_iff.forward with aIn278  have function := functionSpace.mem_iff.forward with fIn279  exact setArrow.map with subset, function280281-- Identities and composition.282defgraph setsIdentity (U : Set) (A ∈ 𝒫(U)) : setsMorphisms(U) :=283  setArrow(U, A, identity(A))284proof285  have identityIn := functionSpace.identity at A286  exact setsMorphisms.arrow with member, member, identityIn287288defgraph setsComposition (U : Set)289    (p ∈ composablePairsOf(setsMorphisms(U), setsDom(U), setsCod(U))) :290    setsMorphisms(U) :=291  setArrow(U, setsCod(U)(fst(p)),292    compose(setsMap(U, fst(p)), setsMap(U, snd(p)), setsDom(U)(snd(p)),293      setsCod(U)(snd(p)), setsCod(U)(fst(p))))294proof295  obtain ⟨bounded, g, gIn, f, fIn, shape, composable⟩ :=296    composablePairsOf.membership.forward with member297  obtain ⟨B, bIn, C, cIn, gMap, gMapIn, gShape⟩ := setsMorphisms.shape with gIn298  obtain ⟨A, aIn, D, dIn, fMap, fMapIn, fShape⟩ := setsMorphisms.shape with fIn299  have domG := setsDom.arrow with bIn, cIn, gMapIn300  have codG := setsCod.arrow with bIn, cIn, gMapIn301  have mapG := setsMap.arrow with bIn, gMapIn302  have codF0 := setsCod.arrow with aIn, dIn, fMapIn303  have middle : B = D by cc304  rw ← middle at fMapIn305  rw ← middle at fShape306  have domF := setsDom.arrow with aIn, bIn, fMapIn307  have codF := setsCod.arrow with aIn, bIn, fMapIn308  have mapF := setsMap.arrow with aIn, fMapIn309  have composed := functionSpace.compose with fMapIn, gMapIn310  rw shape311  rw [fst.pair, snd.pair, gShape, fShape, codG, codF, domF, mapG, mapF]312  exact setsMorphisms.arrow with aIn, cIn, composed313314theorem setsComposition.arrow (U A B C f g : Set)315  requires aIn : A ∈ 𝒫(U)316  requires bIn : B ∈ 𝒫(U)317  requires cIn : C ∈ 𝒫(U)318  requires fIn : f ∈ functionSpace(A, B)319  requires gIn : g ∈ functionSpace(B, C)320  shows setsComposition(U)(setArrow(U, C, g), setArrow(U, B, f)) =321    setArrow(U, C, compose(g, f, A, B, C))322proof323  have gMember := setsMorphisms.arrow with bIn, cIn, gIn324  have fMember := setsMorphisms.arrow with aIn, bIn, fIn325  have domG := setsDom.arrow with bIn, cIn, gIn326  have codF := setsCod.arrow with aIn, bIn, fIn327  have domF := setsDom.arrow with aIn, bIn, fIn328  have codG := setsCod.arrow with bIn, cIn, gIn329  have mapG := setsMap.arrow with bIn, gIn330  have mapF := setsMap.arrow with aIn, fIn331  have composable : setsDom(U)(setArrow(U, C, g)) = setsCod(U)(setArrow(U, B, f))332    cc333  have pairIn := composablePairsOf.pair at setsMorphisms(U), setsDom(U),334    setsCod(U), setArrow(U, C, g), setArrow(U, B, f) with335    gMember, fMember, composable336  have value := setsComposition.value with pairIn337  have firstValue := fst.pair at setArrow(U, C, g), setArrow(U, B, f)338  have secondValue := snd.pair at setArrow(U, C, g), setArrow(U, B, f)339  simp [call2]340341def Sets (U : Set) : Set :=342  Category.mk(𝒫(U), setsMorphisms(U), setsDom(U), setsCod(U), setsIdentity(U),343    setsComposition(U))344345theorem Sets.obj (U : Set)346  shows obj(Sets(U)) = 𝒫(U)347proof348  simp [Sets, Category.mk.obj]349350theorem Sets.mor (U : Set)351  shows mor(Sets(U)) = setsMorphisms(U)352proof353  simp [Sets, Category.mk.mor]354355theorem Sets.dom (U : Set)356  shows dom(Sets(U)) = setsDom(U)357proof358  simp [Sets, Category.mk.dom]359360theorem Sets.cod (U : Set)361  shows cod(Sets(U)) = setsCod(U)362proof363  simp [Sets, Category.mk.cod]364365theorem Sets.comp (U : Set)366  shows comp(Sets(U)) = setsComposition(U)367proof368  simp [Sets, Category.mk.comp]369370theorem Sets.id (U : Set)371  shows id(Sets(U)) = setsIdentity(U)372proof373  simp [Sets, Category.mk.id]374375tactic sets_projections := simp [Sets.obj, Sets.mor, Sets.dom, Sets.cod, Sets.comp, Sets.id]376377theorem Sets.category (U : Set)378  shows Category(Sets(U))379proof380  have domFunction := setsDom.function at U381  have codFunction := setsCod.function at U382  have idFunction := setsIdentity.function at U383  have compFunction := setsComposition.function at U384  unfold Sets385  apply Category.intro with domFunction, codFunction, idFunction, compFunction386  . intros A aIn387    have idValue := setsIdentity.value with aIn388    have identityIn := functionSpace.identity at A389    have domValue := setsDom.arrow with aIn, aIn, identityIn390    have codValue := setsCod.arrow with aIn, aIn, identityIn391    rw idValue392    refine ⟨domValue, codValue⟩393  . intros g gIn f fIn composable394    obtain ⟨B, bIn, C, cIn, gMap, gMapIn, gShape⟩ := setsMorphisms.shape with gIn395    obtain ⟨A, aIn, D, dIn, fMap, fMapIn, fShape⟩ := setsMorphisms.shape with fIn396    have domG := setsDom.arrow with bIn, cIn, gMapIn397    have codF := setsCod.arrow with aIn, dIn, fMapIn398    have middle : B = D by cc399    rw ← middle at fMapIn400    rw ← middle at fShape401    have composite := setsComposition.arrow with aIn, bIn, cIn, fMapIn, gMapIn402    have composed := functionSpace.compose with fMapIn, gMapIn403    have domComposite := setsDom.arrow with aIn, cIn, composed404    have codComposite := setsCod.arrow with aIn, cIn, composed405    have domF := setsDom.arrow with aIn, bIn, fMapIn406    have codG := setsCod.arrow with bIn, cIn, gMapIn407    rw [gShape, fShape, composite]408    refine ⟨?_, ?_⟩409    . cc410    . cc411  . intros f fIn412    obtain ⟨A, aIn, B, bIn, fMap, fMapIn, fShape⟩ := setsMorphisms.shape with fIn413    have domF := setsDom.arrow with aIn, bIn, fMapIn414    have codF := setsCod.arrow with aIn, bIn, fMapIn415    have aIdentity := setsIdentity.value with aIn416    have bIdentity := setsIdentity.value with bIn417    have aIdentityIn := functionSpace.identity at A418    have bIdentityIn := functionSpace.identity at B419    have leftComposite := setsComposition.arrow with420      aIn, bIn, bIn, fMapIn, bIdentityIn421    have rightComposite := setsComposition.arrow with422      aIn, aIn, bIn, aIdentityIn, fMapIn423    have function := functionSpace.mem_iff.forward with fMapIn424    have leftUnit := compose.identity_left with function425    have rightUnit := compose.identity_right with function426    rw fShape427    rw [domF, codF, aIdentity, bIdentity, leftComposite, rightComposite]428    rw [leftUnit, rightUnit]429    refine ⟨rfl, rfl⟩430  . intros h hIn g gIn f fIn outer inner431    obtain ⟨C, cIn, D, dIn, hMap, hMapIn, hShape⟩ := setsMorphisms.shape with hIn432    obtain ⟨B, bIn, E, eIn, gMap, gMapIn, gShape⟩ := setsMorphisms.shape with gIn433    obtain ⟨A, aIn, K, kIn, fMap, fMapIn, fShape⟩ := setsMorphisms.shape with fIn434    have domH := setsDom.arrow with cIn, dIn, hMapIn435    have codG := setsCod.arrow with bIn, eIn, gMapIn436    have domG := setsDom.arrow with bIn, eIn, gMapIn437    have codF := setsCod.arrow with aIn, kIn, fMapIn438    have outerMiddle : C = E by cc439    have innerMiddle : B = K by cc440    rw ← outerMiddle at gMapIn441    rw ← outerMiddle at gShape442    rw ← innerMiddle at fMapIn443    rw ← innerMiddle at fShape444    have hg := setsComposition.arrow with bIn, cIn, dIn, gMapIn, hMapIn445    have gf := setsComposition.arrow with aIn, bIn, cIn, fMapIn, gMapIn446    have hgIn := functionSpace.compose with gMapIn, hMapIn447    have gfIn := functionSpace.compose with fMapIn, gMapIn448    have leftComposite := setsComposition.arrow with aIn, bIn, dIn, fMapIn, hgIn449    have rightComposite := setsComposition.arrow with450      aIn, cIn, dIn, gfIn, hMapIn451    have fFunction := functionSpace.mem_iff.forward with fMapIn452    have gFunction := functionSpace.mem_iff.forward with gMapIn453    have hFunction := functionSpace.mem_iff.forward with hMapIn454    have associative := compose.associative with fFunction, gFunction, hFunction455    rw [hShape, gShape, fShape, hg, gf, leftComposite, rightComposite]456    rw associative457    rfl458459-- Morphisms of Sets(U) as functions: a hom-set is the function space, up460-- to the codomain entry, and a morphism applies as a function.461section SetsLaws462variable (U : Set)463hypothesis sets : Category(Sets(U))464465theorem Sets.hom_shape (A B m : Set)466  requires mHom : m ∈ hom(Sets(U), A, B)467  shows ∃ f ∈ functionSpace(A, B), m = setArrow(U, B, f)468proof469  obtain ⟨mIn, domM, codM⟩ := hom.membership.forward with mHom470  simp [Sets.obj, Sets.mor, Sets.dom, Sets.cod, Sets.comp, Sets.id] at mIn471  simp [Sets.obj, Sets.mor, Sets.dom, Sets.cod, Sets.comp, Sets.id] at domM472  simp [Sets.obj, Sets.mor, Sets.dom, Sets.cod, Sets.comp, Sets.id] at codM473  obtain ⟨A2, aIn, B2, bIn, f, fIn, shape⟩ := setsMorphisms.shape with mIn474  have domValue := setsDom.arrow with aIn, bIn, fIn475  have codValue := setsCod.arrow with aIn, bIn, fIn476  have sameA : A2 = A by cc477  have sameB : B2 = B by cc478  rw [sameA, sameB] at fIn479  rw sameB at shape480  refine ⟨f, fIn, shape⟩481482theorem Sets.arrow_hom (A B f : Set)483  requires aIn : A ∈ 𝒫(U)484  requires bIn : B ∈ 𝒫(U)485  requires function : f : A → B486  shows setArrow(U, B, f) : A ⟶ B487proof488  have fIn := functionSpace.mem_iff.backward with function489  have member := setsMorphisms.arrow with aIn, bIn, fIn490  have domValue := setsDom.arrow with aIn, bIn, fIn491  have codValue := setsCod.arrow with aIn, bIn, fIn492  unfold Morphism493  rw [Sets.mor, Sets.dom, Sets.cod]494  refine ⟨member, domValue, codValue⟩495496theorem Sets.object (A B : Set) (f : A ⟶ B)497  shows A ∈ 𝒫(U)498proof499  have aIn : A ∈ obj(Sets(U)) := Morphism.dom_object with *500  simp [Sets.obj, Sets.mor, Sets.dom, Sets.cod, Sets.comp, Sets.id] at aIn501  exact aIn502503theorem Sets.target (A B : Set) (f : A ⟶ B)504  shows B ∈ 𝒫(U)505proof506  have bIn : B ∈ obj(Sets(U)) := Morphism.cod_object with *507  simp [Sets.obj, Sets.mor, Sets.dom, Sets.cod, Sets.comp, Sets.id] at bIn508  exact bIn509510theorem Sets.function (A B : Set) (f : A ⟶ B)511  shows setsMap(U, f) : A → B512proof513  have fHom : f ∈ hom(Sets(U), A, B) := Morphism.hom with *514  have aIn := Sets.object with *515  obtain ⟨f0, f0In, shape⟩ := Sets.hom_shape with sets, fHom516  have function := functionSpace.mem_iff.forward with f0In517  have underlying := setsMap.arrow with aIn, f0In518  rw shape519  rw underlying520  exact function521522theorem Sets.arrow_apply (A B f x : Set)523  requires aIn : A ∈ 𝒫(U)524  requires function : f : A → B525  requires xIn : x ∈ A526  shows setArrow(U, B, f)(x) = f(x)527proof528  have subset := powerset.membership_iff.forward with aIn529  exact setArrow.apply with subset, function, xIn530531theorem Sets.apply_map (A B : Set) (f : A ⟶ B) (x : Set)532  requires xIn : x ∈ A533  shows f(x) = setsMap(U, f)(x)534proof535  have fHom : f ∈ hom(Sets(U), A, B) := Morphism.hom with *536  have aIn := Sets.object with *537  obtain ⟨f0, f0In, shape⟩ := Sets.hom_shape with sets, fHom538  have function := functionSpace.mem_iff.forward with f0In539  have underlying := setsMap.arrow with aIn, f0In540  have value := Sets.arrow_apply with sets, aIn, function, xIn541  rw shape542  rw [underlying, value]543  rfl544545theorem Sets.apply_closed (A B : Set) (f : A ⟶ B) (x : Set)546  requires xIn : x ∈ A547  shows f(x) ∈ B548proof549  have function := Sets.function with *550  have value := Sets.apply_map with *551  rw value552  exact FunctionBetween.apply_closed with function, xIn553554theorem Sets.id_apply (A x : Set)555  requires aIn : A ∈ 𝒫(U)556  requires xIn : x ∈ A557  shows id(Sets(U))(A)(x) = x558proof559  have idValue := setsIdentity.value with aIn560  have identityFunction := identity.function at A561  have applied := identity.apply with xIn562  have arrowValue := Sets.arrow_apply with sets, aIn, identityFunction, xIn563  rw [Sets.id, idValue, arrowValue]564  exact applied565566theorem Sets.comp_apply (A B C : Set) (f : A ⟶ B) (g : B ⟶ C) (x : Set)567  requires xIn : x ∈ A568  shows (g ∘ f)(x) = g(f(x))569proof570  have fHom : f ∈ hom(Sets(U), A, B) := Morphism.hom with *571  have gHom : g ∈ hom(Sets(U), B, C) := Morphism.hom with *572  have fTyped := Morphism.of_hom with fHom573  have gTyped := Morphism.of_hom with gHom574  have aIn : A ∈ obj(Sets(U)) := Morphism.dom_object with sets, fTyped575  have bIn : B ∈ obj(Sets(U)) := Morphism.cod_object with sets, fTyped576  have cIn : C ∈ obj(Sets(U)) := Morphism.cod_object with sets, gTyped577  rw Sets.obj at aIn578  rw Sets.obj at bIn579  rw Sets.obj at cIn580  obtain ⟨f0, f0In, fShape⟩ := Sets.hom_shape with sets, fHom581  obtain ⟨g0, g0In, gShape⟩ := Sets.hom_shape with sets, gHom582  have fFunction := functionSpace.mem_iff.forward with f0In583  have gFunction := functionSpace.mem_iff.forward with g0In584  have composite := setsComposition.arrow with aIn, bIn, cIn, f0In, g0In585  have composed := compose.function with fFunction, gFunction586  have composedValue := compose.apply with fFunction, gFunction, xIn587  have fValue := Sets.arrow_apply with sets, aIn, fFunction, xIn588  have fxIn := FunctionBetween.apply_closed with fFunction, xIn589  have gValue := Sets.arrow_apply with sets, bIn, gFunction, fxIn590  have compositeValue := Sets.arrow_apply with sets, aIn, composed, xIn591  have operation := Sets.comp at U592  rw [fShape, gShape]593  rw [operation, composite, compositeValue, fValue, gValue]594  exact composedValue595596theorem Sets.ext (A B : Set) (f g : A ⟶ B)597  requires same : ∀ x ∈ A, f(x) = g(x)598  shows f = g599proof600  have fHom : f ∈ hom(Sets(U), A, B) := Morphism.hom with *601  have gHom : g ∈ hom(Sets(U), A, B) := Morphism.hom with *602  have fTyped := Morphism.of_hom with fHom603  have aIn : A ∈ obj(Sets(U)) := Morphism.dom_object with sets, fTyped604  rw Sets.obj at aIn605  obtain ⟨f0, f0In, fShape⟩ := Sets.hom_shape with sets, fHom606  obtain ⟨g0, g0In, gShape⟩ := Sets.hom_shape with sets, gHom607  have fFunction := functionSpace.mem_iff.forward with f0In608  have gFunction := functionSpace.mem_iff.forward with g0In609  have agree : ∀ x ∈ A, f0(x) = g0(x)610    intros x xIn611    have fValue := Sets.arrow_apply with sets, aIn, fFunction, xIn612    have gValue := Sets.arrow_apply with sets, aIn, gFunction, xIn613    have equal := same with x, xIn614    rw [fShape, gShape] at equal615    rw [fValue, gValue] at equal616    exact equal617  have underlying := FunctionBetween.ext with fFunction, gFunction, agree618  rw [fShape, gShape, underlying]619  rfl620621end SetsLaws622623-- The rewrite set for values of morphisms of Sets(U): composites and624-- identities apply pointwise, and an arrow built from a function applies625-- as that function.626tactic sets_simp := simp [Sets.comp_apply, Sets.id_apply, Sets.arrow_apply]627