def CategoryTheory.WalkingIso : Type u

This is the free-living isomorphism as a category with objects called zero and one. Perhaps these should have different names?

Equations

• CategoryTheory.WalkingIso = ULift.{?u.1, 0} (Fin 2)

@[match_pattern]

def CategoryTheory.WalkingIso.zero : WalkingIso

Equations

• CategoryTheory.WalkingIso.zero = { down := 0 }

@[match_pattern]

def CategoryTheory.WalkingIso.one : WalkingIso

Equations

• CategoryTheory.WalkingIso.one = { down := 1 }

instance CategoryTheory.WalkingIso.instCategory : Category.{0, u_1} WalkingIso

The free isomorphism is the codiscrete category on two objects. Can we make this a special case of the other definition?

Equations

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

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 = { hom := F.map PUnit.unit, inv := F.map PUnit.unit, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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, one can build a functor out of WalkingIso to that category.

Equations

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

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.

def CategoryTheory.WalkingIso.coev (i : WalkingIso) : Functor (Fin 1) WalkingIso

Equations

• i.coev = CategoryTheory.ComposableArrows.mk₀ i

def SSet.coherentIso : SSet

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

Equations

• SSet.coherentIso = CategoryTheory.nerve CategoryTheory.WalkingIso

def SSet.coherentIso.equivFun {n : ℕ} : coherentIso.obj (Opposite.op (SimplexCategory.mk n)) ≃ (Fin (n + 1) → Fin 2)

Since the morphisms in WalkingIso do not carry information, an n-simplex of coherentIso is equivalent to an (n + 1)-vector of the objects of WalkingIso.

Equations

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

instance SSet.coherentIso.instDecidableEqObjOppositeSimplexCategoryOpMk (n : ℕ) : DecidableEq (coherentIso.obj (Opposite.op (SimplexCategory.mk n)))

Since Fin 2 has decidable equality, the simplices of coherentIso have decidable equality as well.

Equations

• SSet.coherentIso.instDecidableEqObjOppositeSimplexCategoryOpMk n x✝¹ x✝ = decidable_of_iff (SSet.coherentIso.equivFun x✝¹ = SSet.coherentIso.equivFun x✝) ⋯

def SSet.coherentIso.x₀ : coherentIso.obj (Opposite.op (SimplexCategory.mk 0))

The source vertex of coherentIso.

Equations

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

def SSet.coherentIso.x₁ : coherentIso.obj (Opposite.op (SimplexCategory.mk 0))

The target edge 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₁ PUnit.unit, src_eq := SSet.coherentIso.hom._proof_4, tgt_eq := SSet.coherentIso.hom._proof_5 }

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

The backwards edge of coherentIso.

Equations

• SSet.coherentIso.inv = { edge := CategoryTheory.ComposableArrows.mk₁ PUnit.unit, 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.isIsoHom : hom.IsIso

The forwards edge of coherentIso is an isomorphism.

Equations

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

def SSet.coherentIso.isIsoMapHom {X : SSet} (g : coherentIso ⟶ X) : (hom.map g).IsIso

The image of hom under an SSet morphism is an isomorphism.

Equations

• SSet.coherentIso.isIsoMapHom g = SSet.coherentIso.isIsoHom.map g

def SSet.coherentIso.isIsoOfEqMapHom {X : SSet} {x₀ x₁ : X.obj (Opposite.op (SimplexCategory.mk 0))} {f : Edge x₀ x₁} {g : coherentIso ⟶ X} (hfg : f.edge = g.app (Opposite.op (SimplexCategory.mk 1)) hom.edge) : f.IsIso

If an edge is equal to the image of hom under an SSet morphism, this edge is an isomorphism.

Equations

• SSet.coherentIso.isIsoOfEqMapHom hfg = (SSet.coherentIso.isIsoMapHom g).ofEq ⋯