structure Category.Isomorphism {O : Sort u_1} [𝓒 : Category O] (A B : O) : Sort (max 1 u_2)

An isomorphism demonstrates that two objects cannot be distinguished in this category.

From a category-theoretic point of view, it's really uncouth to say anything more than that two objects are isomorphic. Lean equality depends on the particular encoding of the category, and not on the essence of the object we're studying.

• out : Category.Struct.Mor A B
• inv : Category.Struct.Mor B A
• pre_inv : self.inv ≫ self.out = Category.Struct.id
• post_inv : self.out ≫ self.inv = Category.Struct.id

theorem Category.Isomorphism.ext {O : Sort u_1} {𝓒 : Category O} {A B : O} {x y : A ≅ B} (out : x.out = y.out) (inv : x.inv = y.inv) : x = y

def Category.«term_≅_» : Lean.TrailingParserDescr

Notation to be able to write A ≅ B instead of Isomorphism A B

Equations

• Category.«term_≅_» = Lean.ParserDescr.trailingNode `Category.«term_≅_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≅ ") (Lean.ParserDescr.cat `term 101))

theorem Category.Isomorphism.out_eq_then_inv_eq {O : Sort u_1} [𝓒 : Category O] {A B : O} {f g : A ≅ B} : f.out = g.out → f.inv = g.inv

If two isomorphisms have the same main function, their inverses must also match.

This is a useful technical lemma, since we can then use it to prove identities about isomorphisms without having to prove the same result for both the carrier and the inverse.

@[simp]

theorem Category.Isomorphism.eq_iff_out_eq {O : Sort u_1} [𝓒 : Category O] {A B : O} {f g : A ≅ B} : f = g ↔ f.out = g.out

To prove that two isomorphisms are equal, it suffices to show their carriers are equal.

This is a key simplifier for equalities of isomorphisims.

def Category.Isomorphism.flip {O : Sort u_1} [𝓒 : Category O] {A B : O} (i : A ≅ B) : B ≅ A

An isomorphism can be flipped, and considered in the other direction.

Equations

• i.flip = { out := i.inv, inv := i.out, pre_inv := ⋯, post_inv := ⋯ }

@[simp]

def Category.Isomorphism.flip_flip_eq {O : Sort u_1} [𝓒 : Category O] {A B : O} (i : A ≅ B) : i.flip.flip = i

Flipping an isomorphism twice produces the original isomorphism.

Equations

• ⋯ = ⋯

def Category.Isomorphism.comp {O : Sort u_1} [𝓒 : Category O] {A B C : O} (i0 : A ≅ B) (i1 : B ≅ C) : A ≅ C

Isomorphisms can be composed together.

Equations

• i0.comp i1 = { out := i0.out ≫ i1.out, inv := i1.inv ≫ i0.inv, pre_inv := ⋯, post_inv := ⋯ }

@[simp]

theorem Category.Isomorphism.comp_out_eq_comp {O : Sort u_1} [𝓒 : Category O] {A B C : O} {F : A ≅ B} {G : B ≅ C} : (F.comp G).out = F.out ≫ G.out

When showing that the composition of isomorphisms

def Category.Isomorphism.id {O : Sort u_1} [𝓒 : Category O] {A : O} : A ≅ A

Any object is isomorphic to itself, as demonstrated by the identity function.

Equations

• Category.Isomorphism.id = { out := Category.Struct.id, inv := Category.Struct.id, pre_inv := ⋯, post_inv := ⋯ }

@[simp]

theorem Category.Isomorphism.id_out_eq_id {O : Sort u_2} [𝓒 : Category O] {A : O} : Category.Isomorphism.id.out = Category.Struct.id

Simplifying the identity isomorphism to the identity morphism.

This is useful because proving identities about isomorphisms boils down to proving identities about the carrier functions.

structure OfIso (α : Sort u_1) : Sort (max 1 u_1)

A wrapper structure to define the category of isomorphisms.

• unOfIso : α

def Category.Iso {O : Sort u_1} [𝓒 : Category O] : Category (OfIso O)

Isomorphisms form a category.

Equations

• Category.Iso = Category.mk ⋯ ⋯ ⋯

def Category.is_mono {O : Sort u_1} [𝓒 : Category O] {B C : O} (f : Category.Struct.Mor B C) : Prop

The property of being a monomorphism, i.e. preserving equalities by post-composition.

Equations

• Category.is_mono f = ∀ {A : O} {g h : Category.Struct.Mor A B}, g ≫ f = h ≫ f → g = h

def Category.is_epi {O : Sort u_1} [𝓒 : Category O] {A B : O} (f : Category.Struct.Mor A B) : Prop

The property of being an epimorphism, i.e. being a monomorphism in the opposite category.

Equations

• Category.is_epi f = Category.is_mono f

class Category.Mono {O : Sort u_1} [𝓒 : Category O] {A B : O} (f : Category.Struct.Mor A B) : Prop

The claass of functions that are monomorphisms

• w_mono : Category.is_mono f

class Category.Epi {O : Sort u_1} [𝓒 : Category O] {A B : O} (f : Category.Struct.Mor A B) : Prop

• w_epi : Category.is_epi f