Grace/Cumulus/Category/Isomorphism.g17

Open in Workbench Download source

Imports

Core

Declarations

Source

1-- Isomorphisms in a small category2-- 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.Isomorphism8import Core910-- g is a two-sided inverse of f.11predicate InversePair (C f g : Set) :=12  f ∈ mor(C) ∧ g ∈ mor(C) ∧ dom(C)(g) = cod(C)(f) ∧ cod(C)(g) = dom(C)(f) ∧13  comp(C)(g, f) = id(C)(dom(C)(f)) ∧ comp(C)(f, g) = id(C)(cod(C)(f))1415notation infixr 70 "∘" => call2(C.comp, _, _) via hypothesis InversePair(C, f, g) for C.mor1617predicate Isomorphism (C f : Set) :=18  ∃ g, InversePair(C, f, g)1920predicate Isomorphic (C a b : Set) :=21  ∃ f ∈ hom(C, a, b), Isomorphism(C, f)2223theorem InversePair.morphism (C f g : Set)24  requires pair : InversePair(C, f, g)25  shows f ∈ mor(C)26proof27  simp [InversePair]2829theorem InversePair.inverse_morphism (C f g : Set)30  requires pair : InversePair(C, f, g)31  shows g ∈ mor(C)32proof33  simp [InversePair]3435theorem InversePair.dom (C f g : Set)36  requires pair : InversePair(C, f, g)37  shows dom(C)(g) = cod(C)(f)38proof39  obtain ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩ := pair40  exact domG4142theorem InversePair.cod (C f g : Set)43  requires pair : InversePair(C, f, g)44  shows cod(C)(g) = dom(C)(f)45proof46  obtain ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩ := pair47  exact codG4849theorem InversePair.left (C f g : Set)50  requires pair : InversePair(C, f, g)51  shows g ∘ f = id(C)(dom(C)(f))52proof53  obtain ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩ := pair54  exact leftLaw5556theorem InversePair.right (C f g : Set)57  requires pair : InversePair(C, f, g)58  shows f ∘ g = id(C)(cod(C)(f))59proof60  obtain ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩ := pair61  exact rightLaw6263theorem InversePair.symmetric (C f g : Set)64  requires pair : InversePair(C, f, g)65  shows InversePair(C, g, f)66proof67  obtain ⟨fInM, gInM, domG, codG, leftLaw, rightLaw⟩ := pair68  unfold InversePair69  refine ⟨gInM, fInM, ?_, ?_, ?_, ?_⟩70  . cc71  . cc72  . cc73  . cc7475section InverseLaws76variable (C : Set)77hypothesis category : Category(C)7879theorem InversePair.hom (f g : Set)80  requires pair : InversePair(C, f, g)81  shows f : dom(C)(f) ⟶ cod(C)(f)82proof83  have fInM := InversePair.morphism with pair84  exact Morphism.of_morphism with category, fInM8586theorem InversePair.inverse_hom (f g : Set)87  requires pair : InversePair(C, f, g)88  shows g : cod(C)(f) ⟶ dom(C)(f)89proof90  obtain ⟨fInM, gInM, domG, codG, gf, fg⟩ := pair91  unfold Morphism92  refine ⟨gInM, domG, codG⟩9394theorem InversePair.inverse_of_hom (a b : Set) (f : a ⟶ b) (g : Set)95  requires pair : InversePair(C, f, g)96  shows g : b ⟶ a97proof98  have gHom : g : cod(C)(f) ⟶ dom(C)(f) := InversePair.inverse_hom with category, pair99  have domF : dom(C)(f) = a by cc100  have codF : cod(C)(f) = b by cc101  rw [domF, codF] at gHom102  exact gHom103104theorem InversePair.left_hom (a b : Set) (f : a ⟶ b) (g : Set)105  requires pair : InversePair(C, f, g)106  shows g ∘ f = id(C)(a)107proof108  have law : g ∘ f = id(C)(dom(C)(f)) := InversePair.left with pair109  have domF : dom(C)(f) = a by cc110  rwa domF at law111112theorem InversePair.right_hom (a b : Set) (f : a ⟶ b) (g : Set)113  requires pair : InversePair(C, f, g)114  shows f ∘ g = id(C)(b)115proof116  have law : f ∘ g = id(C)(cod(C)(f)) := InversePair.right with pair117  have codF : cod(C)(f) = b by cc118  rwa codF at law119120-- Inverses are unique: a left inverse equals a right inverse.121theorem InversePair.unique (a b : Set) (f : a ⟶ b) (g k : b ⟶ a)122  requires gf : g ∘ f = id(C)(a)123  requires fk : f ∘ k = id(C)(b)124  shows g = k125proof126  calc127    g = g ∘ id(C)(b) := by simp [Category.id_right]128    _ = g ∘ (f ∘ k) := by rw fk129    _ = (g ∘ f) ∘ k := by rw Category.assoc130    _ = id(C)(a) ∘ k := by rw gf131    _ = k := by simp [Category.id_left]132133theorem InversePair.eq_of_pairs (f g k : Set)134  requires first : InversePair(C, f, g)135  requires second : InversePair(C, f, k)136  shows g = k137proof138  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := InversePair.hom with category, first139  have gHom : g : cod(C)(f) ⟶ dom(C)(f) := InversePair.inverse_hom with category, first140  have kHom : k : cod(C)(f) ⟶ dom(C)(f) := InversePair.inverse_hom with category, second141  have gf : g ∘ f = id(C)(dom(C)(f)) := InversePair.left with first142  have fk : f ∘ k = id(C)(cod(C)(f)) := InversePair.right with second143  exact InversePair.unique with category, fHom, gHom, kHom, gf, fk144145end InverseLaws146147theorem InversePair.in_hom (C a b f g : Set)148  requires pair : InversePair(C, f, g)149  requires fHom : f ∈ hom(C, a, b)150  shows g ∈ hom(C, b, a)151proof152  obtain ⟨fInM, gInM, domG, codG, gf, fg⟩ := pair153  obtain ⟨fInM2, domF, codF⟩ := hom.membership.forward with fHom154  apply hom.membership.backward155  refine ⟨gInM, ?_, ?_⟩156  . cc157  . cc158159theorem InversePair.id (C a : Set)160  requires category : Category(C)161  requires aInO : a ∈ obj(C)162  shows InversePair(C, id(C)(a), id(C)(a))163proof164  have idInM := Category.id_closed with category, aInO165  have domId := Category.id_dom with category, aInO166  have codId := Category.id_cod with category, aInO167  have idId := Category.id_id with category, aInO168  unfold InversePair169  refine ⟨idInM, idInM, ?_, ?_, ?_, ?_⟩170  . cc171  . cc172  . cc173  . cc174175section InverseComposition176variable (C : Set)177hypothesis category : Category(C)178179-- The inverse of a composite is the composite of the inverses, reversed.180theorem InversePair.comp (a b c : Set) (f : a ⟶ b) (g : b ⟶ c) (k l : Set)181  requires gPair : InversePair(C, g, k)182  requires fPair : InversePair(C, f, l)183  shows InversePair(C, g ∘ f, l ∘ k)184proof185  have kHom : k : c ⟶ b := InversePair.inverse_of_hom with category, gPair186  have lHom : l : b ⟶ a := InversePair.inverse_of_hom with category, fPair187  have gfHom : g ∘ f : a ⟶ c by synthesize188  have lkHom : l ∘ k : c ⟶ a by synthesize189  have kg : k ∘ g = id(C)(b) := InversePair.left_hom with category, gPair190  have gk : g ∘ k = id(C)(c) := InversePair.right_hom with category, gPair191  have lf : l ∘ f = id(C)(a) := InversePair.left_hom with category, fPair192  have fl : f ∘ l = id(C)(b) := InversePair.right_hom with category, fPair193  have leftLaw : (l ∘ k) ∘ (g ∘ f) = id(C)(a)194    calc195      (l ∘ k) ∘ (g ∘ f) = l ∘ (k ∘ (g ∘ f)) := by rw Category.assoc196      _ = l ∘ ((k ∘ g) ∘ f) := by rw Category.assoc197      _ = l ∘ (id(C)(b) ∘ f) := by rw kg198      _ = l ∘ f := by rw Category.id_left199      _ = id(C)(a) := lf200  have rightLaw : (g ∘ f) ∘ (l ∘ k) = id(C)(c)201    calc202      (g ∘ f) ∘ (l ∘ k) = g ∘ (f ∘ (l ∘ k)) := by rw Category.assoc203      _ = g ∘ ((f ∘ l) ∘ k) := by rw Category.assoc204      _ = g ∘ (id(C)(b) ∘ k) := by rw fl205      _ = g ∘ k := by rw Category.id_left206      _ = id(C)(c) := gk207  unfold InversePair208  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩209  . assumption210  . assumption211  . cc212  . cc213  . cc214  . cc215216end InverseComposition217218theorem Isomorphism.morphism (C f : Set)219  requires iso : Isomorphism(C, f)220  shows f ∈ mor(C)221proof222  obtain ⟨g, pair⟩ := iso223  exact InversePair.morphism with pair224225theorem Isomorphism.of_pair (C f g : Set)226  requires pair : InversePair(C, f, g)227  shows Isomorphism(C, f)228proof229  refine ⟨g, pair⟩230231theorem Isomorphism.inverse (C f g : Set)232  requires pair : InversePair(C, f, g)233  shows Isomorphism(C, g)234proof235  have symmetric := InversePair.symmetric with pair236  exact Isomorphism.of_pair with symmetric237238theorem Isomorphism.id (C a : Set)239  requires category : Category(C)240  requires aInO : a ∈ obj(C)241  shows Isomorphism(C, id(C)(a))242proof243  have pair := InversePair.id with category, aInO244  exact Isomorphism.of_pair with pair245246theorem Isomorphism.comp (C g f : Set)247  requires category : Category(C)248  requires gIso : Isomorphism(C, g)249  requires fIso : Isomorphism(C, f)250  requires composable : dom(C)(g) = cod(C)(f)251  shows Isomorphism(C, g ∘ f)252proof253  obtain ⟨k, gPair⟩ := gIso254  obtain ⟨l, fPair⟩ := fIso255  have gInM := InversePair.morphism with gPair256  have fInM := InversePair.morphism with fPair257  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *258  have gHom : g : cod(C)(f) ⟶ cod(C)(g) := Morphism.of_composable with *259  have pair := InversePair.comp with category, fHom, gHom, gPair, fPair260  exact Isomorphism.of_pair with pair261262-- Cancellation against an isomorphism.263theorem InversePair.cancel_left (C f g u v : Set)264  requires category : Category(C)265  requires pair : InversePair(C, f, g)266  requires uInM : u ∈ mor(C)267  requires vInM : v ∈ mor(C)268  requires uComposable : dom(C)(f) = cod(C)(u)269  requires vComposable : dom(C)(f) = cod(C)(v)270  requires same : f ∘ u = f ∘ v271  shows u = v272proof273  obtain ⟨fInM, gInM, domG, codG, gf, fg⟩ := pair274  have unitU : id(C)(dom(C)(f)) ∘ u = u275    have law := Category.left_unit with category, uInM276    rwa ← uComposable at law277  have unitV : id(C)(dom(C)(f)) ∘ v = v278    have law := Category.left_unit with category, vInM279    rwa ← vComposable at law280  have assocU := Category.associative with281    category, gInM, fInM, uInM, domG, uComposable282  have assocV := Category.associative with283    category, gInM, fInM, vInM, domG, vComposable284  calc285    u = id(C)(dom(C)(f)) ∘ u := by rw unitU286    _ = (g ∘ f) ∘ u := by rw gf287    _ = g ∘ (f ∘ u) := assocU288    _ = g ∘ (f ∘ v) := by rw same289    _ = (g ∘ f) ∘ v := by rw assocV290    _ = id(C)(dom(C)(f)) ∘ v := by rw gf291    _ = v := unitV292293theorem InversePair.cancel_right (C f g u v : Set)294  requires category : Category(C)295  requires pair : InversePair(C, f, g)296  requires uInM : u ∈ mor(C)297  requires vInM : v ∈ mor(C)298  requires uComposable : dom(C)(u) = cod(C)(f)299  requires vComposable : dom(C)(v) = cod(C)(f)300  requires same : u ∘ f = v ∘ f301  shows u = v302proof303  obtain ⟨fInM, gInM, domG, codG, gf, fg⟩ := pair304  have unitU := Category.id_right_of_dom with category, uInM, uComposable305  have unitV := Category.id_right_of_dom with category, vInM, vComposable306  have fgComposable : dom(C)(f) = cod(C)(g) by cc307  have assocU := Category.associative with308    category, uInM, fInM, gInM, uComposable, fgComposable309  have assocV := Category.associative with310    category, vInM, fInM, gInM, vComposable, fgComposable311  calc312    u = u ∘ id(C)(cod(C)(f)) := by rw unitU313    _ = u ∘ (f ∘ g) := by rw fg314    _ = (u ∘ f) ∘ g := by rw assocU315    _ = (v ∘ f) ∘ g := by rw same316    _ = v ∘ (f ∘ g) := assocV317    _ = v ∘ id(C)(cod(C)(f)) := by rw fg318    _ = v := unitV319320-- A morphism that is inverted on both sides by the same morphism of each321-- side is an isomorphism; in particular a left and a right inverse agree.322theorem InversePair.of_left_right (C f g k : Set)323  requires category : Category(C)324  requires fInM : f ∈ mor(C)325  requires gInM : g ∈ mor(C)326  requires kInM : k ∈ mor(C)327  requires domG : dom(C)(g) = cod(C)(f)328  requires codK : cod(C)(k) = dom(C)(f)329  requires left : g ∘ f = id(C)(dom(C)(f))330  requires right : f ∘ k = id(C)(cod(C)(f))331  shows g = k ∧ InversePair(C, f, k)332proof333  have unitG := Category.id_right_of_dom with category, gInM, domG334  have unitK := Category.id_left_of_cod with category, kInM, codK335  have fkComposable : dom(C)(f) = cod(C)(k) by cc336  have assoc := Category.associative with337    category, gInM, fInM, kInM, domG, fkComposable338  have equal : g = k339    calc340      g = g ∘ id(C)(cod(C)(f)) := by rw unitG341      _ = g ∘ (f ∘ k) := by rw right342      _ = (g ∘ f) ∘ k := by rw assoc343      _ = id(C)(dom(C)(f)) ∘ k := by rw left344      _ = k := unitK345  constructor346  . exact equal347  . unfold InversePair348    refine ⟨fInM, kInM, ?_, codK, ?_, right⟩349    . cc350    . rw ← equal351      exact left352353theorem Isomorphic.of_hom (C a b f : Set)354  requires fHom : f ∈ hom(C, a, b)355  requires iso : Isomorphism(C, f)356  shows Isomorphic(C, a, b)357proof358  refine ⟨f, fHom, iso⟩359360theorem Isomorphic.reflexive (C a : Set)361  requires category : Category(C)362  requires aInO : a ∈ obj(C)363  shows Isomorphic(C, a, a)364proof365  have idHom := hom.id with category, aInO366  have iso := Isomorphism.id with category, aInO367  exact Isomorphic.of_hom with idHom, iso368369theorem Isomorphic.symmetric (C a b : Set)370  requires h : Isomorphic(C, a, b)371  shows Isomorphic(C, b, a)372proof373  obtain ⟨f, fHom, g, pair⟩ := h374  have gHom := InversePair.in_hom with pair, fHom375  have gIso := Isomorphism.inverse with pair376  exact Isomorphic.of_hom with gHom, gIso377378theorem Isomorphic.transitive (C a b c : Set)379  requires category : Category(C)380  requires first : Isomorphic(C, a, b)381  requires second : Isomorphic(C, b, c)382  shows Isomorphic(C, a, c)383proof384  obtain ⟨f, fHom, fIso⟩ := first385  obtain ⟨g, gHom, gIso⟩ := second386  have composable := hom.composable with gHom, fHom387  have compHom := hom.comp with category, gHom, fHom388  have compIso := Isomorphism.comp with category, gIso, fIso, composable389  exact Isomorphic.of_hom with compHom, compIso390391-- Inverses transpose a commutative square: if e2 ∘ u = v ∘ e1 for392-- isomorphisms e1 : a → b and e2 : c → d with inverses k1 and k2, then393-- k2 ∘ v = u ∘ k1.394theorem InversePair.transpose (C a b c d e1 k1 e2 k2 u v : Set)395  requires category : Category(C)396  requires firstPair : InversePair(C, e1, k1)397  requires secondPair : InversePair(C, e2, k2)398  requires e1Hom : e1 ∈ hom(C, a, b)399  requires e2Hom : e2 ∈ hom(C, c, d)400  requires uHom : u ∈ hom(C, a, c)401  requires vHom : v ∈ hom(C, b, d)402  requires square : e2 ∘ u = v ∘ e1403  shows k2 ∘ v = u ∘ k1404proof405  have k1Hom := InversePair.in_hom with firstPair, e1Hom406  have k2Hom := InversePair.in_hom with secondPair, e2Hom407  have e1k1 : e1 ∘ k1 = id(C)(b)408    have law := InversePair.right with firstPair409    have codE := hom.cod with e1Hom410    rwa codE at law411  have k2e2 : k2 ∘ e2 = id(C)(c)412    have law := InversePair.left with secondPair413    have domE := hom.dom with e2Hom414    rwa domE at law415  have uk1Hom := hom.comp with category, uHom, k1Hom416  have unitV := Category.id_right_hom with category, vHom417  have unitUK := Category.id_left_hom with category, uk1Hom418  have assocOne := Category.assoc_hom with category, vHom, e1Hom, k1Hom419  have assocTwo := Category.assoc_hom with category, e2Hom, uHom, k1Hom420  have assocThree := Category.assoc_hom with category, k2Hom, e2Hom, uk1Hom421  calc422    k2 ∘ v = k2 ∘ (v ∘ id(C)(b)) := by rw unitV423    _ = k2 ∘ (v ∘ (e1 ∘ k1)) := by rw e1k1424    _ = k2 ∘ ((v ∘ e1) ∘ k1) := by rw assocOne425    _ = k2 ∘ ((e2 ∘ u) ∘ k1) := by rw square426    _ = k2 ∘ (e2 ∘ (u ∘ k1)) := by rw assocTwo427    _ = (k2 ∘ e2) ∘ (u ∘ k1) := by rw assocThree428    _ = id(C)(c) ∘ (u ∘ k1) := by rw k2e2429    _ = u ∘ k1 := unitUK430431-- Isomorphism as a relation on the objects.432def isomorphismRelation (C : Set) : Set :=433  { p ∈ obj(C) × obj(C) | ∃ a ∈ obj(C), ∃ b ∈ obj(C), p = (a, b) ∧434    Isomorphic(C, a, b) }435436theorem isomorphismRelation.relates (C a b : Set)437  requires aInO : a ∈ obj(C)438  requires bInO : b ∈ obj(C)439  requires iso : Isomorphic(C, a, b)440  shows relates(isomorphismRelation(C), a, b)441proof442  unfold relates443  apply isomorphismRelation.membership.backward444  constructor445  . exact product.pair with aInO, bInO446  . refine ⟨a, aInO, b, bInO, rfl, iso⟩447448theorem isomorphismRelation.reflects (C a b : Set)449  requires related : relates(isomorphismRelation(C),450    a, b)451  shows Isomorphic(C, a, b)452proof453  unfold relates at related454  obtain ⟨bounded, c, cInO, d, dInO, shape, iso⟩ :=455    isomorphismRelation.membership.forward with related456  obtain ⟨aEqual, bEqual⟩ := orderedPair.injective with shape457  rw [aEqual, bEqual]458  exact iso459460theorem isomorphismRelation.relation (C : Set)461  shows RelationOn(isomorphismRelation(C), obj(C))462proof463  unfold RelationOn464  unfold RelationBetween465  intros p member466  obtain ⟨bounded, rest⟩ := isomorphismRelation.membership.forward with member467  exact bounded468469theorem isomorphismRelation.equivalence (C : Set)470  requires category : Category(C)471  shows Equivalence(obj(C), isomorphismRelation(C))472proof473  have relation := isomorphismRelation.relation at C474  unfold Equivalence475  refine ⟨relation, ?_, ?_, ?_⟩476  . intros a aInO477    have iso := Isomorphic.reflexive with category, aInO478    exact isomorphismRelation.relates with aInO, aInO, iso479  . intros a aInO b bInO related480    have iso := isomorphismRelation.reflects with related481    have back := Isomorphic.symmetric with iso482    exact isomorphismRelation.relates with bInO, aInO, back483  . intros a aInO b bInO c cInO first second484    have firstIso := isomorphismRelation.reflects with first485    have secondIso := isomorphismRelation.reflects with second486    have iso := Isomorphic.transitive with category, firstIso, secondIso487    exact isomorphismRelation.relates with aInO, cInO, iso488489-- The isomorphism class of an object.490def isomorphismClass (C a : Set) : Set :=491  { b ∈ obj(C) | Isomorphic(C, a, b) }492493theorem isomorphismClass.subset (C a : Set)494  shows isomorphismClass(C, a) ⊆ obj(C)495proof496  intros b member497  obtain ⟨bInO, iso⟩ := isomorphismClass.membership.forward with member498  exact bInO499500theorem isomorphismClass.self (C a : Set)501  requires category : Category(C)502  requires aInO : a ∈ obj(C)503  shows a ∈ isomorphismClass(C, a)504proof505  have iso := Isomorphic.reflexive with category, aInO506  apply isomorphismClass.membership.backward507  refine ⟨aInO, iso⟩508509theorem isomorphismClass.symmetric (C a b : Set)510  requires aInO : a ∈ obj(C)511  requires member : b ∈ isomorphismClass(C, a)512  shows a ∈ isomorphismClass(C, b)513proof514  obtain ⟨bInO, iso⟩ := isomorphismClass.membership.forward with member515  have back := Isomorphic.symmetric with iso516  apply isomorphismClass.membership.backward517  refine ⟨aInO, back⟩518519theorem isomorphismClass.subset_of_isomorphic (C a b : Set)520  requires category : Category(C)521  requires iso : Isomorphic(C, a, b)522  shows isomorphismClass(C, b) ⊆523    isomorphismClass(C, a)524proof525  intros c member526  obtain ⟨cInO, second⟩ := isomorphismClass.membership.forward with member527  have chain := Isomorphic.transitive with category, iso, second528  apply isomorphismClass.membership.backward529  refine ⟨cInO, chain⟩530531theorem isomorphismClass.eq_of_isomorphic (C a b : Set)532  requires category : Category(C)533  requires iso : Isomorphic(C, a, b)534  shows isomorphismClass(C, a) =535    isomorphismClass(C, b)536proof537  have back := Isomorphic.symmetric with iso538  have forward := isomorphismClass.subset_of_isomorphic with category, iso539  have backward := isomorphismClass.subset_of_isomorphic with category, back540  exact Subset.antisymmetric with backward, forward541542theorem isomorphismClass.eq_of_member (C a b : Set)543  requires category : Category(C)544  requires member : b ∈ isomorphismClass(C, a)545  shows isomorphismClass(C, a) =546    isomorphismClass(C, b)547proof548  obtain ⟨bInO, iso⟩ := isomorphismClass.membership.forward with member549  exact isomorphismClass.eq_of_isomorphic with category, iso550551theorem isomorphismClass.disjoint_or_equal (C a b : Set)552  requires category : Category(C)553  requires aInO : a ∈ obj(C)554  requires bInO : b ∈ obj(C)555  shows Disjoint(isomorphismClass(C, a),556    isomorphismClass(C, b)) ∨557    isomorphismClass(C, a) =558    isomorphismClass(C, b)559proof560  by_contra negated561  have notDisjoint : ¬Disjoint(isomorphismClass(C, a),562      isomorphismClass(C, b))563    intro disjoint564    apply negated565    left566    exact disjoint567  have common : Nonempty(isomorphismClass(C, a) ∩568      isomorphismClass(C, b))569    apply Nonempty.of_ne_empty570    intro emptyMeet571    apply notDisjoint572    unfold Disjoint573    exact emptyMeet574  obtain ⟨c, cInMeet⟩ := common575  obtain ⟨cInA, cInB⟩ := intersection.membership.forward with cInMeet576  have aClass := isomorphismClass.eq_of_member with category, cInA577  have bClass := isomorphismClass.eq_of_member with category, cInB578  apply negated579  right580  cc581582-- The inverse of an isomorphism, as the unique morphism inverting it.583defunique inverseMorphism (C f : Set) (g ∈ mor(C)) :=584  InversePair(C, f, g)585requires category : Category(C)586requires iso : Isomorphism(C, f)587proof588  obtain ⟨g, pair⟩ := iso589  have gInM := InversePair.inverse_morphism with pair590  refine ⟨g, gInM, pair⟩591uniqueness592  intros u hu first v hv second593  exact InversePair.eq_of_pairs with category, first, second594595theorem inverseMorphism.pair (C f : Set)596  requires category : Category(C)597  requires iso : Isomorphism(C, f)598  shows InversePair(C, f,599    inverseMorphism(C, f))600proof601  have selected := inverseMorphism.selected at C, f with602    category, iso603  exact selected.right604605theorem inverseMorphism.morphism (C f : Set)606  requires category : Category(C)607  requires iso : Isomorphism(C, f)608  shows inverseMorphism(C, f) ∈ mor(C)609proof610  have selected := inverseMorphism.selected at C, f with611    category, iso612  exact selected.left613614theorem inverseMorphism.eq (C f g : Set)615  requires category : Category(C)616  requires pair : InversePair(C, f, g)617  shows inverseMorphism(C, f) = g618proof619  have iso := Isomorphism.of_pair with pair620  have canonical := inverseMorphism.pair with category, iso621  exact InversePair.eq_of_pairs with category, canonical, pair622623theorem inverseMorphism.in_hom (C a b f : Set)624  requires category : Category(C)625  requires iso : Isomorphism(C, f)626  requires fHom : f ∈ hom(C, a, b)627  shows inverseMorphism(C, f) ∈ hom(C, b, a)628proof629  have pair := inverseMorphism.pair with category, iso630  exact InversePair.in_hom with pair, fHom631632theorem inverseMorphism.isomorphism (C f : Set)633  requires category : Category(C)634  requires iso : Isomorphism(C, f)635  shows Isomorphism(C, inverseMorphism(C, f))636proof637  have pair := inverseMorphism.pair with category, iso638  exact Isomorphism.inverse with pair639640theorem inverseMorphism.involutive (C f : Set)641  requires category : Category(C)642  requires iso : Isomorphism(C, f)643  shows inverseMorphism(C, inverseMorphism(C, f)) = f644proof645  have pair := inverseMorphism.pair with category, iso646  have symmetric := InversePair.symmetric with pair647  exact inverseMorphism.eq with category, symmetric648649theorem inverseMorphism.id (C a : Set)650  requires category : Category(C)651  requires aInO : a ∈ obj(C)652  shows inverseMorphism(C, id(C)(a)) = id(C)(a)653proof654  have pair := InversePair.id with category, aInO655  exact inverseMorphism.eq with category, pair656657theorem inverseMorphism.comp (C g f : Set)658  requires category : Category(C)659  requires gIso : Isomorphism(C, g)660  requires fIso : Isomorphism(C, f)661  requires composable : dom(C)(g) = cod(C)(f)662  shows inverseMorphism(C, g ∘ f) =663    inverseMorphism(C, f) ∘664      inverseMorphism(C, g)665proof666  have gPair := inverseMorphism.pair with category, gIso667  have fPair := inverseMorphism.pair with category, fIso668  have gInM := Isomorphism.morphism with gIso669  have fInM := Isomorphism.morphism with fIso670  have fHom : f : dom(C)(f) ⟶ cod(C)(f) := Morphism.of_morphism with *671  have gHom : g : cod(C)(f) ⟶ cod(C)(g) := Morphism.of_composable with *672  have pair := InversePair.comp with category, fHom, gHom, gPair, fPair673  exact inverseMorphism.eq with category, pair674675theorem inverseMorphism.left (C f : Set)676  requires category : Category(C)677  requires iso : Isomorphism(C, f)678  shows inverseMorphism(C, f) ∘ f = id(C)(dom(C)(f))679proof680  have pair := inverseMorphism.pair with category, iso681  exact InversePair.left with pair682683theorem inverseMorphism.right (C f : Set)684  requires category : Category(C)685  requires iso : Isomorphism(C, f)686  shows f ∘ inverseMorphism(C, f) = id(C)(cod(C)(f))687proof688  have pair := inverseMorphism.pair with category, iso689  exact InversePair.right with pair690