The Coherent Isomorphism

We define the free walking isomorphism WalkingIso; the category with objects zero and one and unique morphisms zero ⟶ one and one ⟶ zero. We construct an equivalence WalkingIso.equiv between the type of functors from WalkingIso into any category C and the type Σ (X : C) (Y : C), (X ≅ Y) of isomorphisms in that category.

The simplicial set SSet.coherentIso is defined as the nerve of WalkingIso, with coherentIso.x₀ and coherentIso.x₁ the 0-simplices corresponding to WalkingIso.zero and WalkingIso.one respectively, and coherentIso.hom : Edge x₀ x₁ and coherentIso.inv : Edge x₁ x₀ forward and backward edges corresponding to the morphisms in WalkingIso. Given any simplicial set X, with a morphism g : coherentIso ⟶ X, 0-simplices x₀ x₁: X _⦋0⦌ and an edge between them f : Edge x₀ x₁, such that g sends coherentIso.hom to f, then f has an inverse (in the sense of Edge.InvStruct), see invStructOfEqMapHom.

@[reducible, inline]

abbrev CategoryTheory.WalkingIso : Type w

This is the free-living isomorphism as the codiscrete category on Bool.

Equations

• CategoryTheory.WalkingIso = CategoryTheory.Codiscrete (ULift.{?u.1, 0} Bool)

def CategoryTheory.WalkingIso.equivBool : WalkingIso ≃ Bool

The underlying type of WalkingIso is equivalent to Bool, since they both have 2 elements.

Equations

• CategoryTheory.WalkingIso.equivBool = CategoryTheory.codiscreteEquiv.trans Equiv.ulift

def CategoryTheory.WalkingIso.zero : WalkingIso

The domain of the isomorphism

Equations

• CategoryTheory.WalkingIso.zero = { as := { down := false } }

def CategoryTheory.WalkingIso.one : WalkingIso

The codomain of the isomorphism

Equations

• CategoryTheory.WalkingIso.one = { as := { down := true } }

def CategoryTheory.WalkingIso.iso : zero ≅ one

The isomorphism between zero and one in WalkingIso.

Equations

• CategoryTheory.WalkingIso.iso = CategoryTheory.Codiscrete.iso CategoryTheory.WalkingIso.zero CategoryTheory.WalkingIso.one

theorem CategoryTheory.WalkingIso.eq_iso_hom (f : zero ⟶ one) : f = iso.hom

theorem CategoryTheory.WalkingIso.eq_iso_inv (f : one ⟶ zero) : f = iso.inv

def CategoryTheory.WalkingIso.toIso {C : Type u} [Category.{v, u} C] (F : Functor WalkingIso C) : F.obj zero ≅ F.obj one

Functors out of WalkingIso define isomorphisms in the target category.

Equations

• CategoryTheory.WalkingIso.toIso F = F.mapIso CategoryTheory.WalkingIso.iso

@[simp]

theorem CategoryTheory.WalkingIso.toIso_hom {C : Type u} [Category.{v, u} C] (F : Functor WalkingIso C) : (toIso F).hom = F.map iso.hom

@[simp]

theorem CategoryTheory.WalkingIso.toIso_inv {C : Type u} [Category.{v, u} C] (F : Functor WalkingIso C) : (toIso F).inv = F.map iso.inv

def CategoryTheory.WalkingIso.rec {motive : WalkingIso → Sort u_1} (zero : motive zero) (one : motive one) (a : WalkingIso) : motive a

The recursor for WalkingIso, which constructs a term of ∏ (x : WalkingIso), A x from a term of A zero and a term of A one.

Equations

• CategoryTheory.WalkingIso.rec zero one { as := { down := false } } = zero
• CategoryTheory.WalkingIso.rec zero one { as := { down := true } } = one

@[simp]

theorem CategoryTheory.WalkingIso.rec_zero {motive : WalkingIso → Sort u_1} (zero : motive zero) (one : motive one) : WalkingIso.rec zero one WalkingIso.zero = zero

@[simp]

theorem CategoryTheory.WalkingIso.rec_one {motive : WalkingIso → Sort u_1} (zero : motive zero) (one : motive one) : WalkingIso.rec zero one WalkingIso.one = one

def CategoryTheory.WalkingIso.fromIso {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) : Functor WalkingIso C

From an isomorphism in a category, we can build a functor out of WalkingIso to that category.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.WalkingIso.fromIso_zero {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) : (fromIso e).obj zero = X

@[simp]

theorem CategoryTheory.WalkingIso.fromIso_one {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) : (fromIso e).obj one = Y

@[simp]

theorem CategoryTheory.WalkingIso.fromIso_map_zero_zero {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) (f : zero ⟶ zero) : (fromIso e).map f = CategoryStruct.id X

@[simp]

theorem CategoryTheory.WalkingIso.fromIso_hom {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) (f : zero ⟶ one) : (fromIso e).map f = e.hom

@[simp]

theorem CategoryTheory.WalkingIso.fromIso_inv {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) (f : one ⟶ zero) : (fromIso e).map f = e.inv

@[simp]

theorem CategoryTheory.WalkingIso.fromIso_map_one_one {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) (f : one ⟶ one) : (fromIso e).map f = CategoryStruct.id Y

def CategoryTheory.WalkingIso.equiv {C : Type u} [Category.{v, u} C] : Functor WalkingIso C ≃ (X : C) × (Y : C) × (X ≅ Y)

An equivalence between the type of WalkingIsos in C and the type of isomorphisms in C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.WalkingIso.equiv_symm_apply {C : Type u} [Category.{v, u} C] (p : (X : C) × (Y : C) × (X ≅ Y)) : equiv.symm p = fromIso p.snd.snd

@[simp]

theorem CategoryTheory.WalkingIso.equiv_apply_snd_fst {C : Type u} [Category.{v, u} C] (F : Functor WalkingIso C) : (equiv F).snd.fst = F.obj one

@[simp]

theorem CategoryTheory.WalkingIso.equiv_apply_fst {C : Type u} [Category.{v, u} C] (F : Functor WalkingIso C) : (equiv F).fst = F.obj zero

@[simp]

theorem CategoryTheory.WalkingIso.equiv_apply_snd_snd {C : Type u} [Category.{v, u} C] (F : Functor WalkingIso C) : (equiv F).snd.snd = toIso F

@[reducible, inline]

abbrev SSet.coherentIso : SSet

The simplicial set that encodes a single isomorphism. Its n-simplices are formal compositions of arrows in WalkingIso.

Equations

• SSet.coherentIso = CategoryTheory.nerve CategoryTheory.WalkingIso

def SSet.coherentIso.x₀ : coherentIso.obj (Opposite.op { len := 0 })

The source vertex of coherentIso.

Equations

• SSet.coherentIso.x₀ = CategoryTheory.ComposableArrows.mk₀ CategoryTheory.WalkingIso.zero

def SSet.coherentIso.x₁ : coherentIso.obj (Opposite.op { len := 0 })

The target vertex of coherentIso.

Equations

• SSet.coherentIso.x₁ = CategoryTheory.ComposableArrows.mk₀ CategoryTheory.WalkingIso.one

def SSet.coherentIso.hom : Edge x₀ x₁

The forwards edge of coherentIso.

Equations

• SSet.coherentIso.hom = { edge := CategoryTheory.ComposableArrows.mk₁ CategoryTheory.WalkingIso.iso.hom, src_eq := SSet.coherentIso.hom._proof_1, tgt_eq := SSet.coherentIso.hom._proof_2 }

def SSet.coherentIso.inv : Edge x₁ x₀

The backwards edge of coherentIso.

Equations

• SSet.coherentIso.inv = { edge := CategoryTheory.ComposableArrows.mk₁ CategoryTheory.WalkingIso.iso.inv, src_eq := SSet.coherentIso.inv._proof_1, tgt_eq := SSet.coherentIso.inv._proof_2 }

def SSet.coherentIso.homInvId : hom.CompStruct inv (Edge.id x₀)

The forwards and backwards edge of coherentIso compose to the identity.

Equations

• One or more equations did not get rendered due to their size.

def SSet.coherentIso.invHomId : inv.CompStruct hom (Edge.id x₁)

The backwards and forwards edge of coherentIso compose to the identity.

Equations

• One or more equations did not get rendered due to their size.

def SSet.coherentIso.invStructHom : hom.InvStruct

The forwards edge of coherentIso has an inverse.

Equations

• SSet.coherentIso.invStructHom = { inv := SSet.coherentIso.inv, homInvId := SSet.coherentIso.homInvId, invHomId := SSet.coherentIso.invHomId }

@[simp]

theorem SSet.coherentIso.invStructHom_homInvId : invStructHom.homInvId = homInvId

@[simp]

theorem SSet.coherentIso.invStructHom_invHomId : invStructHom.invHomId = invHomId

@[simp]

theorem SSet.coherentIso.invStructHom_inv : invStructHom.inv = inv

@[reducible, inline]

abbrev SSet.coherentIso.invStructOfEqMapHom {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {f : Edge x₀ x₁} {g : coherentIso ⟶ X} (hfg : f.edge = (CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op { len := 1 }))) hom.edge) : f.InvStruct

For a simplicial set X, if an edge in X is equal to the image of hom under a morphism of simplicial sets, this edge has an inverse.

Equations

• SSet.coherentIso.invStructOfEqMapHom hfg = (SSet.coherentIso.invStructHom.map g).ofEq ⋯