[aa4262]: thys / Category2 / Category.thy  Maximize  Restore  History

Download this file

450 lines (376 with data), 19.6 kB

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
(*
Author: Alexander Katovsky
*)
header "Category"
theory Category imports FuncSet begin
record ('o,'m) Category =
Obj :: "'o set" ("obj\<index>" 70)
Mor :: "'m set" ("mor\<index>" 70)
Dom :: "'m \<Rightarrow> 'o" ("dom\<index> _" [80] 70)
Cod :: "'m \<Rightarrow> 'o" ("cod\<index> _" [80] 70)
Id :: "'o \<Rightarrow> 'm" ("id\<index> _" [80] 75)
Comp :: "'m \<Rightarrow> 'm \<Rightarrow> 'm" (infixl ";;\<index>" 70)
definition
MapsTo :: "('o,'m,'a) Category_scheme \<Rightarrow> 'm \<Rightarrow> 'o \<Rightarrow> 'o \<Rightarrow> bool" ("_ maps\<index> _ to _" [60, 60, 60] 65) where
"MapsTo CC f X Y \<equiv> f \<in> Mor CC \<and> Dom CC f = X \<and> Cod CC f = Y"
definition
CompDefined :: "('o,'m,'a) Category_scheme \<Rightarrow> 'm \<Rightarrow> 'm \<Rightarrow> bool" (infixl "\<approx>>\<index>" 65) where
"CompDefined CC f g \<equiv> f \<in> Mor CC \<and> g \<in> Mor CC \<and> Cod CC f = Dom CC g"
locale ExtCategory =
fixes C :: "('o,'m,'a) Category_scheme" (structure)
assumes CdomExt: "(Dom C) \<in> extensional (Mor C)"
and CcodExt: "(Cod C) \<in> extensional (Mor C)"
and CidExt: "(Id C) \<in> extensional (Obj C)"
and CcompExt: "(split (Comp C)) \<in> extensional ({(f,g) | f g . f \<approx>> g})"
locale Category = ExtCategory +
assumes Cdom : "f \<in> mor \<Longrightarrow> dom f \<in> obj"
and Ccod : "f \<in> mor \<Longrightarrow> cod f \<in> obj"
and Cidm [dest]: "X \<in> obj \<Longrightarrow> (id X) maps X to X"
and Cidl : "f \<in> mor \<Longrightarrow> id (dom f) ;; f = f"
and Cidr : "f \<in> mor \<Longrightarrow> f ;; id (cod f) = f"
and Cassoc : "\<lbrakk>f \<approx>> g ; g \<approx>> h\<rbrakk> \<Longrightarrow> (f ;; g) ;; h = f ;; (g ;; h)"
and Ccompt : "\<lbrakk>f maps X to Y ; g maps Y to Z\<rbrakk> \<Longrightarrow> (f ;; g) maps X to Z"
definition
MakeCat :: "('o,'m,'a) Category_scheme \<Rightarrow> ('o,'m,'a) Category_scheme" where
"MakeCat C \<equiv> \<lparr>
Obj = Obj C ,
Mor = Mor C ,
Dom = restrict (Dom C) (Mor C) ,
Cod = restrict (Cod C) (Mor C) ,
Id = restrict (Id C) (Obj C) ,
Comp = \<lambda> f g . (restrict (split (Comp C)) ({(f,g) | f g . f \<approx>>\<^bsub>C\<^esub> g})) (f,g),
\<dots> = Category.more C
\<rparr>"
lemma MakeCatMapsTo: "f maps\<^bsub>C\<^esub> X to Y \<Longrightarrow> f maps\<^bsub>MakeCat C\<^esub> X to Y"
by (auto simp add: MapsTo_def MakeCat_def)
lemma MakeCatComp: "f \<approx>>\<^bsub>C\<^esub> g \<Longrightarrow> f ;;\<^bsub>MakeCat C\<^esub> g = f ;;\<^bsub>C\<^esub> g"
by (auto simp add: MapsTo_def MakeCat_def)
lemma MakeCatId: "X \<in> obj\<^bsub>C\<^esub> \<Longrightarrow> id\<^bsub>C\<^esub> X = id\<^bsub>MakeCat C\<^esub> X"
by (auto simp add: MapsTo_def MakeCat_def)
lemma MakeCatObj: "obj\<^bsub>MakeCat C\<^esub> = obj\<^bsub>C\<^esub>"
by (simp add: MakeCat_def)
lemma MakeCatMor: "mor\<^bsub>MakeCat C\<^esub> = mor\<^bsub>C\<^esub>"
by (simp add: MakeCat_def)
lemma MakeCatDom: "f \<in> mor\<^bsub>C\<^esub> \<Longrightarrow> dom\<^bsub>C\<^esub> f = dom\<^bsub>MakeCat C\<^esub> f"
by (simp add: MakeCat_def)
lemma MakeCatCod: "f \<in> mor\<^bsub>C\<^esub> \<Longrightarrow> cod\<^bsub>C\<^esub> f = cod\<^bsub>MakeCat C\<^esub> f"
by (simp add: MakeCat_def)
lemma MakeCatCompDef: "f \<approx>>\<^bsub>MakeCat C\<^esub> g = f \<approx>>\<^bsub>C\<^esub> g"
by (auto simp add: CompDefined_def MakeCat_def)
lemma MakeCatComp2: "f \<approx>>\<^bsub>MakeCat C\<^esub> g \<Longrightarrow> f ;;\<^bsub>MakeCat C\<^esub> g = f ;;\<^bsub>C\<^esub> g"
by (simp add: MakeCatCompDef MakeCatComp)
lemma ExtCategoryMakeCat: "ExtCategory (MakeCat C)"
by (unfold_locales, simp_all add: MakeCat_def extensional_def CompDefined_def)
lemma MakeCat: "Category_axioms C \<Longrightarrow> Category (MakeCat C)"
apply(intro_locales, simp add: ExtCategoryMakeCat)
apply (simp add: Category_axioms_def)
apply (auto simp add: MakeCat_def CompDefined_def MapsTo_def)
done
lemma MapsToE[elim]: "\<lbrakk>f maps\<^bsub>C\<^esub> X to Y ; \<lbrakk>f \<in> mor\<^bsub>C\<^esub> ; dom\<^bsub>C\<^esub> f = X ; cod\<^bsub>C\<^esub> f = Y\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
by (auto simp add: MapsTo_def)
lemma MapsToI[intro]: "\<lbrakk>f \<in> mor\<^bsub>C\<^esub> ; dom\<^bsub>C\<^esub> f = X ; cod\<^bsub>C\<^esub> f = Y\<rbrakk> \<Longrightarrow> f maps\<^bsub>C\<^esub> X to Y"
by (auto simp add: MapsTo_def)
lemma CompDefinedE[elim]: "\<lbrakk>f \<approx>>\<^bsub>C\<^esub> g ; \<lbrakk>f \<in> mor\<^bsub>C\<^esub> ; g \<in> mor\<^bsub>C\<^esub> ; cod\<^bsub>C\<^esub> f = dom\<^bsub>C\<^esub> g\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
by (auto simp add: CompDefined_def)
lemma CompDefinedI[intro]: "\<lbrakk>f \<in> mor\<^bsub>C\<^esub> ; g \<in> mor\<^bsub>C\<^esub> ; cod\<^bsub>C\<^esub> f = dom\<^bsub>C\<^esub> g\<rbrakk> \<Longrightarrow> f \<approx>>\<^bsub>C\<^esub> g"
by (auto simp add: CompDefined_def)
lemma (in Category) MapsToCompI: assumes "f \<approx>> g" shows "(f ;; g) maps (dom f) to (cod g)"
proof-
have "f maps (dom f) to (dom g)"
and "g maps (dom g) to (cod g)" using assms by auto
thus ?thesis by (simp add: Ccompt[of f "dom f" "dom g" g "cod g"])
qed
lemma MapsToCompDef:
assumes "f maps\<^bsub>C\<^esub> X to Y" and "g maps\<^bsub>C\<^esub> Y to Z"
shows "f \<approx>>\<^bsub>C\<^esub> g"
proof(rule CompDefinedI)
show "f \<in> mor\<^bsub>C\<^esub>" and "g \<in> mor\<^bsub>C\<^esub>" using assms by auto
have "cod\<^bsub>C\<^esub> f = Y" and "dom\<^bsub>C\<^esub> g = Y" using assms by auto
thus "cod\<^bsub>C\<^esub> f = dom\<^bsub>C\<^esub> g" by simp
qed
lemma (in Category) MapsToMorDomCod:
assumes "f \<approx>> g"
shows "f ;; g \<in> mor" and "dom (f ;; g) = dom f" and "cod (f ;; g) = cod g"
proof-
have "(f ;; g) maps (dom f) to (cod g)" using assms by (simp add: MapsToCompI)
thus "f ;; g \<in> mor" and "dom (f ;; g) = dom f" and "cod (f ;; g) = cod g" by auto
qed
lemma (in Category) MapsToObj:
assumes "f maps X to Y"
shows "X \<in> obj" and "Y \<in> obj"
proof-
have "dom f = X" and "cod f = Y" and "f \<in> mor" using assms by auto
thus "X \<in> obj" and "Y \<in> obj" by (auto simp add: Cdom Ccod)
qed
lemma (in Category) IdInj:
assumes "X \<in> obj" and "Y \<in> obj" and "id X = id Y"
shows "X = Y"
proof-
have "dom (id X) = dom (id Y)" using assms by simp
moreover have "dom (id X) = X" and "dom (id Y) = Y" using assms by (auto simp add: MapsTo_def)
ultimately show ?thesis by simp
qed
lemma (in Category) CompDefComp:
assumes "f \<approx>> g" and "g \<approx>> h"
shows "f \<approx>> (g ;; h)" and "(f ;; g) \<approx>> h"
proof(auto simp add: CompDefined_def)
show "f \<in> mor" and "h \<in> mor" using assms by auto
have 1: "g ;; h maps (dom g) to (cod h)"
and 2: "f ;; g maps (dom f) to (cod g)" using assms by (simp add: MapsToCompI)+
thus "g ;; h \<in> mor" and "f ;; g \<in> mor" by auto
have "cod f = dom g" using assms by auto
also have "... = dom (g ;; h)" using 1 by auto
finally show "cod f = dom (g ;; h)" .
have "dom h = cod g" using assms by auto
also have "... = cod (f ;; g)" using 2 by auto
finally show "cod (f ;; g) = dom h" by simp
qed
lemma (in Category) CatIdInMor: "X \<in> obj \<Longrightarrow> id X \<in> mor"
by (auto simp add: Cidm)
lemma (in Category) MapsToId: assumes "X \<in> obj" shows "id X \<approx>> id X"
proof(rule CompDefinedI)
have "id X maps X to X" using assms by (simp add: Cidm)
thus "id X \<in> mor" and "id X \<in> mor" and "cod (id X) = dom (id X)" by auto
qed
lemmas (in Category) Simps = Cdom Ccod Cidm Cidl Cidr MapsToCompI IdInj MapsToId
lemma (in Category) LeftRightInvUniq:
assumes 0: "h \<approx>> f" and z: "f \<approx>> g"
assumes 1: "f ;; g = id (dom f)"
and 2: "h ;; f = id (cod f)"
shows "h = g"
proof-
have mor: "h \<in> mor \<and> g \<in> mor"
and dc : "dom f = cod h \<and> cod f = dom g" using 0 z by auto
then have "h = h ;; id (dom f)" by (auto simp add: Simps)
also have "... = h ;; (f ;; g)" using 1 by simp+
also have "... = (h ;; f) ;; g" using 0 z by (simp add: Cassoc)
also have "... = (id (cod f)) ;; g" using 2 by simp+
also have "... = g" using mor dc by (auto simp add: Simps)
finally show ?thesis .
qed
lemma (in Category) CatIdDomCod:
assumes "X \<in> obj"
shows "dom (id X) = X" and "cod (id X) = X"
proof-
have "id X maps X to X" using assms
by (simp add: Simps)
thus "dom (id X) = X" and "cod (id X) = X" by auto
qed
lemma (in Category) CatIdCompId:
assumes "X \<in> obj"
shows "id X ;; id X = id X"
proof-
have 0: "id X \<in> mor" using assms by (auto simp add: Simps)
moreover have "cod (id X) = X" using assms by auto
moreover have "id X ;; id (cod (id X)) = id X" using 0 by (simp add: Simps)
ultimately show ?thesis by simp
qed
(*lemmas (in Category) simps2 = simps CatIdCompId Cassoc CatIdDomCod*)
lemma (in Category) CatIdUniqR:
assumes iota: "\<iota> maps X to X"
and rid: "\<forall> f . f \<approx>> \<iota> \<longrightarrow> f ;; \<iota> = f"
shows "id X = \<iota>"
proof(rule LeftRightInvUniq [of "id X" "id X" \<iota> ])
have 0: "X \<in> obj" using iota by (auto simp add: Simps)
hence "id X maps X to X" by (simp add: Cidm)
thus 1: "id X \<approx>> \<iota>" using iota by (auto simp add: Simps)
show "id X \<approx>> id X" using 0 by (auto simp add: Simps)
show "(id X) ;; \<iota> = (id (dom (id X)))" using 0 1 rid by (auto simp add: Simps CompDefined_def MapsTo_def)
show "(id X) ;; (id X) = (id (cod (id X)))" using 0 by (auto simp add: CatIdCompId CompDefined_def MapsTo_def)
qed
definition
inverse_rel :: "('o,'m,'a) Category_scheme \<Rightarrow> 'm \<Rightarrow> 'm \<Rightarrow> bool" ("cinv\<index> _ _" 60) where
"inverse_rel C f g \<equiv> (f \<approx>>\<^bsub>C\<^esub> g) \<and> (f ;;\<^bsub>C\<^esub> g) = (id\<^bsub>C\<^esub> (dom\<^bsub>C\<^esub> f)) \<and> (g ;;\<^bsub>C\<^esub> f) = (id\<^bsub>C\<^esub> (cod\<^bsub>C\<^esub> f))"
definition
isomorphism :: "('o,'m,'a) Category_scheme \<Rightarrow> 'm \<Rightarrow> bool" ("ciso\<index> _" [70]) where
"isomorphism C f \<equiv> \<exists> g . inverse_rel C f g"
lemma (in Category) Inverse_relI: "\<lbrakk>f \<approx>> g ; f ;; g = id (dom f) ; g ;; f = id (cod f)\<rbrakk> \<Longrightarrow> (cinv f g)"
by (auto simp add: inverse_rel_def)
lemma (in Category) Inverse_relE[elim]: "\<lbrakk>cinv f g ; \<lbrakk>f \<approx>> g ; f ;; g = id (dom f) ; g ;; f = id (cod f)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (auto simp add: inverse_rel_def)
lemma (in Category) Inverse_relSym:
assumes "cinv f g"
shows "cinv g f"
proof(rule Inverse_relI)
have 1: "f \<approx>> g" using assms by auto
show 2: "g \<approx>> f"
proof(rule CompDefinedI)
show "g \<in> mor" and 0: "f \<in> mor" using assms by auto
have "f ;; g maps dom f to cod g" using 1 by (simp add: MapsToCompI)
hence "cod g = cod (f ;; g)" by auto
also have "... = cod (id (dom f))" using assms by (auto simp add: inverse_rel_def)
also have "... = dom f"
proof-
have "dom f \<in> obj" using 0 by (simp add: Simps)
hence "id (dom f) maps (dom f) to (dom f)" by (simp add: Simps)
thus ?thesis by auto
qed
finally show 2: "cod g = dom f" by simp
qed
show "g ;; f = id (dom g)" using assms by (auto simp add: inverse_rel_def)
show "f ;; g = id (cod g)"using assms 1 2 by (auto simp add: inverse_rel_def)
qed
lemma (in Category) InverseUnique:
assumes 1: "cinv f g"
and 2: "cinv f h"
shows "g = h"
proof(rule LeftRightInvUniq [of g f h])
have "cinv g f" using 1 2 by (simp only: Inverse_relSym[of f g])
thus "g \<approx>> f" and
"g ;; f = id (cod f)" using 1 by auto
show "f \<approx>> h" using 2 by auto
show "f ;; h = id (dom f)" using 2 by auto
qed
lemma (in Category) InvId: assumes "X \<in> obj" shows "(cinv (id X) (id X))"
proof(rule Inverse_relI)
show "id X \<approx>> id X" using assms by (simp add: Simps)
have "dom (id X) = X" and "dom (id X) = X" using assms by (simp add: CatIdDomCod)+
thus "id X ;; id X = id (dom (id X))" and "id X ;; id X = id (cod (id X))"
using assms by (simp add: CatIdCompId CatIdDomCod)+
qed
definition
inverse :: "('o,'m,'a) Category_scheme \<Rightarrow> 'm \<Rightarrow> 'm" ("Cinv\<index> _" [70]) where
"inverse C f \<equiv> THE g . inverse_rel C f g"
lemma (in Category) inv2Inv:
assumes "cinv f g"
shows "ciso f" and "Cinv f = g"
proof-
show "ciso f" using assms by (auto simp add: isomorphism_def)
hence "\<exists>! g . cinv f g" using assms by (auto simp add: InverseUnique)
thus "Cinv f = g" using assms by (auto simp add: inverse_def)
qed
lemma (in Category) iso2Inv:
assumes "ciso f"
shows "cinv f (Cinv f)"
proof-
have "\<exists>! g . cinv f g" using assms by (auto simp add: InverseUnique isomorphism_def)
thus ?thesis by (auto simp add: inverse_def intro:theI')
qed
lemma (in Category) InvInv:
assumes "ciso f"
shows "ciso (Cinv f)" and "(Cinv (Cinv f)) = f"
proof-
have "cinv f (Cinv f)" using assms by (simp add: iso2Inv)
hence "cinv (Cinv f) f" by (simp add: Inverse_relSym[of f])
thus "ciso (Cinv f)" and "Cinv (Cinv f) = f" by (auto simp add: inv2Inv)
qed
lemma (in Category) InvIsMor: "(cinv f g) \<Longrightarrow> (f \<in> mor \<and> g \<in> mor)"
by (auto simp add: inverse_rel_def)
lemma (in Category) IsoIsMor: "ciso f \<Longrightarrow> f \<in> mor"
by (auto simp add: InvIsMor dest: iso2Inv)
lemma (in Category) InvDomCod:
assumes "ciso f"
shows "dom (Cinv f) = cod f" and "cod (Cinv f) = dom f" and "Cinv f \<in> mor"
proof-
have 1: "cinv f (Cinv f)" using assms by (auto simp add: iso2Inv)
thus "dom (Cinv f) = cod f" by (auto simp add: inverse_rel_def)
from 1 have "cinv (Cinv f) f" by (auto simp add: Inverse_relSym[of f])
thus "cod (Cinv f) = dom f" by (auto simp add: inverse_rel_def)
show "Cinv f \<in> mor" using 1 by (auto simp add: inverse_rel_def)
qed
lemma (in Category) IsoCompInv: "ciso f \<Longrightarrow> f \<approx>> Cinv f"
by (auto simp add: IsoIsMor InvDomCod)
lemma (in Category) InvCompIso: "ciso f \<Longrightarrow> Cinv f \<approx>> f"
by (auto simp add: IsoIsMor InvDomCod)
lemma (in Category) IsoInvId1 : "ciso f \<Longrightarrow> (Cinv f) ;; f = (id (cod f))"
by (auto dest: iso2Inv)
lemma (in Category) IsoInvId2 : "ciso f \<Longrightarrow> f ;; (Cinv f) = (id (dom f))"
by (auto dest: iso2Inv)
lemma (in Category) IsoCompDef:
assumes 1: "f \<approx>> g" and 2: "ciso f" and 3: "ciso g"
shows "(Cinv g) \<approx>> (Cinv f)"
proof(rule CompDefinedI)
show "Cinv g \<in> mor" and "Cinv f \<in> mor" using assms by (auto simp add: InvDomCod)
have "cod (Cinv g) = dom g" using 3 by (simp add: InvDomCod)
also have "... = cod f" using 1 by auto
also have "... = dom (Cinv f)" using 2 by (simp add: InvDomCod)
finally show "cod (Cinv g) = dom (Cinv f)" .
qed
lemma (in Category) IsoCompose:
assumes 1: "f \<approx>> g" and 2: "ciso f" and 3: "ciso g"
shows "ciso (f ;; g)" and "Cinv (f ;; g) = (Cinv g) ;; (Cinv f)"
proof-
have a: "(Cinv g) \<approx>> (Cinv f)" using assms by (simp add: IsoCompDef)
hence b: "(Cinv g) ;; (Cinv f) maps (dom (Cinv g)) to (cod (Cinv f))" by (simp add: MapsToCompI)
hence c: "(Cinv g) ;; (Cinv f) maps (cod g) to (dom f)" using 2 3 by (simp add: InvDomCod)
have d: "f ;; g maps (dom f) to (cod g)" using 1 by (simp add: Simps)
have "cinv (f ;; g) ((Cinv g) ;; (Cinv f))"
proof(auto simp add: inverse_rel_def)
show "f ;; g \<approx>> (Cinv g) ;; (Cinv f)"
proof(rule CompDefinedI)
show "f ;; g \<in> mor" using d by auto
show "(Cinv g) ;; (Cinv f) \<in> mor" using c by auto
have "cod (f ;; g) = cod g" using d by auto
also have "... = dom (Cinv g)" using assms by (simp add: InvDomCod)
also have "... = dom ((Cinv g) ;; (Cinv f))" using b by auto
finally show "cod (f ;; g) = dom ((Cinv g) ;; (Cinv f))" .
qed
show "f ;; g ;; ((Cinv g) ;; (Cinv f)) = id (dom (f ;; g))"
proof-
have e: "g \<approx>> (Cinv g)" using assms by (simp add: IsoCompInv)
have f: "f \<in> mor" using 1 by auto
have "(f ;; g) ;; ((Cinv g) ;; (Cinv f)) = (f ;; (g ;; (Cinv g))) ;; (Cinv f)"
using 1 e a by (auto simp add: Cassoc CompDefComp)
also have "... = f ;; (id (dom g)) ;; (Cinv f)" using 3 by (simp add: IsoInvId2)
also have "... = f ;; id (cod f) ;; (Cinv f)" using 1 by (auto simp add: Simps)
also have "... = f ;; (Cinv f)" using f by (auto simp add: Cidr)
also have "... = id (dom f)" using 2 by (simp add: IsoInvId2)
also have "... = id (dom (f ;; g))" using d by auto
finally show ?thesis by simp
qed
show "((Cinv g) ;; (Cinv f)) ;; (f ;; g) = id (cod (f ;; g))"
proof-
have e: "(Cinv f) \<approx>> f" using assms by (simp add: InvCompIso)
have f: "g \<in> mor" using 1 by auto
have "((Cinv g) ;; (Cinv f)) ;; (f ;; g) = (Cinv g) ;; (((Cinv f) ;; f) ;; g)"
using 1 e a by (auto simp add: Cassoc CompDefComp)
also have "... = (Cinv g) ;; ((id (cod f)) ;; g)" using 2 by (simp add: IsoInvId1)
also have "... = (Cinv g) ;; ((id (dom g)) ;; g)" using 1 by (auto simp add: Simps)
also have "... = (Cinv g) ;; g" using f by (auto simp add: Cidl)
also have "... = id (cod g)" using 3 by (simp add: IsoInvId1)
also have "... = id (cod (f ;; g))" using d by auto
finally show ?thesis by simp
qed
qed
thus "ciso (f ;; g)" and "Cinv (f ;; g) = (Cinv g) ;; (Cinv f)" by (auto simp add: inv2Inv)
qed
definition "ObjIso C A B \<equiv> \<exists> k . (k maps\<^bsub>C\<^esub> A to B) \<and> ciso\<^bsub>C \<^esub>k"
definition
UnitCategory :: "(unit, unit) Category" where
"UnitCategory = MakeCat \<lparr>
Obj = {()} ,
Mor = {()} ,
Dom = (\<lambda>f.()) ,
Cod = (\<lambda>f.()) ,
Id = (\<lambda>f.()) ,
Comp = (\<lambda>f g. ())
\<rparr>"
lemma [simp]: "Category(UnitCategory)"
apply (simp add: UnitCategory_def, rule MakeCat)
by (unfold_locales, auto simp add: UnitCategory_def)
definition
OppositeCategory :: "('o,'m,'a) Category_scheme \<Rightarrow> ('o,'m,'a) Category_scheme" ("Op _" [65] 65) where
"OppositeCategory C \<equiv> \<lparr>
Obj = Obj C ,
Mor = Mor C ,
Dom = Cod C ,
Cod = Dom C ,
Id = Id C ,
Comp = (\<lambda>f g. g ;;\<^bsub>C\<^esub> f),
\<dots> = Category.more C
\<rparr>"
lemma OpCatOpCat: "Op (Op C) = C"
by (simp add: OppositeCategory_def)
lemma OpCatCatAx: "Category_axioms C \<Longrightarrow> Category_axioms (Op C)"
by (simp add: OppositeCategory_def Category_axioms_def MapsTo_def CompDefined_def)
lemma OpCatCatExt: "ExtCategory C \<Longrightarrow> ExtCategory (Op C)"
by (auto simp add: OppositeCategory_def ExtCategory_def MapsTo_def CompDefined_def extensional_def)
lemma OpCatCat: "Category C \<Longrightarrow> Category (Op C)"
by (intro_locales, simp_all add: Category_def OpCatCatAx OpCatCatExt)
lemma MapsToOp: "f maps\<^bsub>C \<^esub>X to Y \<Longrightarrow> f maps\<^bsub>Op C \<^esub>Y to X"
by (simp add: MapsTo_def OppositeCategory_def)
lemma MapsToOpOp: "f maps\<^bsub>Op C \<^esub>X to Y \<Longrightarrow> f maps\<^bsub>C \<^esub>Y to X"
by (simp add: MapsTo_def OppositeCategory_def)
lemma CompDefOp: "f \<approx>>\<^bsub>C\<^esub> g \<Longrightarrow> g \<approx>>\<^bsub>Op C\<^esub> f"
by (simp add: CompDefined_def OppositeCategory_def)
end

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks