StrictIsomorphisms.lean`

79 declarations, 0 contain sorry, 0 declared as axioms

The cosimplicial orientals

These are the strict realizations of the explicit normalized simplex complexes. The only hypotheses are the two classical normalized-chain identities specified below (Steiner, Orientals, 2007, Section 3 and Section 4 before Theorem 4.1). Functoriality, including maps with degenerate images, is proved here.

structure OAI.Thomason.Construction.NormalizedSimplexIdentities line 32
Source documentation
The classical normalized-chain identities.
```
structure NormalizedSimplexIdentities : Prop where
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.object line 41
def OAI.Thomason.Construction.NormalizedSimplexIdentities.map line 44
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.map_id line 48
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.map_comp line 56
def OAI.Thomason.Construction.NormalizedSimplexIdentities.cosimplicial line 65
Source documentation
The actual oriental cosimplicial object.
```
noncomputable def cosimplicial : SimplexCategory ⥤ StrictOmegaCategory.{0} where
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.chains_eq_zero_above line 72
Source documentation
There are no normalized p-simplices in an m-simplex when p > m.
```
theorem chains_eq_zero_above {m p : ℕ} (hmp : m < p) (x : SimplexComplex.Chains m p) :
    x = 0 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.top_faces_equal line 81
Source documentation
The top source and target coincide because the next chain group vanishes.
```
theorem top_faces_equal (m : ℕ) (x : h.object m) : x.table false m = x.table true m := by
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.isTruncated line 91
Source documentation
Each oriental has the expected finite dimension. This follows directly from the normalized-chain construction, without a freeness hypothesis.
```
theorem isTruncated (m : ℕ) : (h.object m).IsTruncated m := by
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.streetNerve line 132
Source documentation
Restrict Yoneda to the actual oriental cosimplicial object.
```
noncomputable def streetNerve : StrictOmegaCategory.{0} ⥤ SSet.{0} :=
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.streetNerve_obj line 136
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.streetNerve_map_app line 140
def OAI.Thomason.Construction.NormalizedSimplexIdentities.finiteStreetNerve line 145
Source documentation
The same Street nerve on strict finite-dimensional categories.
```
noncomputable def finiteStreetNerve (n : ℕ) :
    StrictOmegaCategory.Truncated.{0} n ⥤ SSet.{0} :=
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.streetWeakEquivalences line 151
Source documentation
The prescribed weak equivalences for strict omega-categories, defined through their Street nerves and geometric realization.
```
noncomputable def streetWeakEquivalences : MorphismProperty StrictOmegaCategory.{0} :=
…
```

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.streetWeakEquivalences_eq_ex_twice line 157

Source documentation

The Street comparison uses the two-out-of-three property for realization weak equivalences and the canonical extension equivalence of Goerss--Jardine III.4.6.

theorem streetWeakEquivalences_eq_ex_twice
    [realizationWeakEquivalences.{0}.HasTwoOutOfThreeProperty]
    (hj : ∀ X, realizationWeakEquivalences.{0} (canonicalExtension.app X)) :
    h.streetWeakEquivalences =
      realizationWeakEquivalences.inverseImage (h.streetNerve ⋙ SSet.ex ⋙ SSet.ex) :=
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finiteStreetWeakEquivalences_eq_ex_twice line 165

Source documentation

This equality is uniform in every finite dimension.

theorem finiteStreetWeakEquivalences_eq_ex_twice (n : ℕ)
    [realizationWeakEquivalences.{0}.HasTwoOutOfThreeProperty]
    (hj : ∀ X, realizationWeakEquivalences.{0} (canonicalExtension.app X)) :
    realizationWeakEquivalences.inverseImage (h.finiteStreetNerve n) =
      realizationWeakEquivalences.inverseImage (h.finiteStreetNerve n ⋙ SSet.ex ⋙ SSet.ex) :=
…

def OAI.Thomason.Construction.StrictOmegaCategory.MatchedPair line 191
Source documentation
A pair with its actual lower-dimensional matching equation.
```
def MatchedPair (C : StrictOmegaCategory.{0}) (m : ℕ) :=
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.MatchedPair.left line 198
def OAI.Thomason.Construction.StrictOmegaCategory.MatchedPair.right line 199
def OAI.Thomason.Construction.StrictOmegaCategory.MatchedPair.composite line 200
theorem OAI.Thomason.Construction.StrictOmegaCategory.compositeList_singleton_eq line 204
theorem OAI.Thomason.Construction.StrictOmegaCategory.compositeList_exchange line 211
Source documentation
Strict interchange applied simultaneously along two matching strings.
```
theorem compositeList_exchange {C : StrictOmegaCategory.{0}} {m r : ℕ}
    (hmr : m < r) (ps : List (MatchedPair C m)) {x y : C}
    (hx : CompositeList C r (ps.map MatchedPair.left) x)
    (hy : CompositeList C r (ps.map MatchedPair.right) y)
    (hxy : C.target m x = C.source m y) :
    CompositeList C r (ps.map MatchedPair.composite) (C.comp m x y hxy) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.MatchedPair, OAI.Thomason.Construction.StrictOmegaCategory.CompositeList, OAI.Thomason.Construction.StrictOmegaCategory.MatchedPair.left, OAI.Thomason.Construction.StrictOmegaCategory.MatchedPair.right, OAI.Thomason.Construction.StrictOmegaCategory.MatchedPair.composite
theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositeList.append_targets line 271
Source documentation
Appending any number of target identities retains the same composite.
```
theorem append_targets (h : CompositeList C r xs x) (k : ℕ) :
    CompositeList C r (xs ++ List.replicate k (C.target r x)) x := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.CompositeList
theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositeList.prepend_sources line 283
Source documentation
Prepending any number of source identities retains the same composite.
```
theorem prepend_sources (h : CompositeList C r xs x) (k : ℕ) :
    CompositeList C r (List.replicate k (C.source r x) ++ xs) x := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.CompositeList
theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositeList.dimensionLE line 295
Source documentation
A common dimension bound is preserved by every nonempty strict string.
```
theorem dimensionLE (h : CompositeList C r xs x) (n : ℕ)
    (hd : ∀ y ∈ xs, C.DimensionLE n y) : C.DimensionLE n x := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.CompositeList
abbrev OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.cells line 322
Source documentation
The underlying cells, with every strict functor acting by its actual function.
```
abbrev cells : StrictOmegaCategory.{0} ⥤ Type where
…
```
abbrev OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.cellDiagram line 328
abbrev OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.Carrier line 330
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι line 332
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι_map line 335
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.exists_representative line 339
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι_eq_iff line 346
Source documentation
Equality of original cells is witnessed at a common later stage.
```
theorem ι_eq_iff {j k : J} (x : F.obj j) (y : F.obj k) :
    ι F j x = ι F k y ↔
      ∃ (l : J) (f : j ⟶ l) (g : k ⟶ l), (F.map f).toFun x = (F.map g).toFun y :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι_eq_iff_same_stage line 351

theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.eventually_eq₂ line 357

Source documentation

Two equalities at a stage can be made literal at the same later stage.

theorem eventually_eq₂ {j : J} (x₁ y₁ x₂ y₂ : F.obj j)
    (h₁ : ι F j x₁ = ι F j y₁) (h₂ : ι F j x₂ = ι F j y₂) :
    ∃ (k : J) (f : j ⟶ k),
      (F.map f).toFun x₁ = (F.map f).toFun y₁ ∧
      (F.map f).toFun x₂ = (F.map f).toFun y₂ := by
…

Mentions: OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι

theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.exists_representatives₂ line 373
Source documentation
A pair of colimit cells has representatives in one common stage.
```
theorem exists_representatives₂ (x y : Carrier F) :
    ∃ (j : J) (a b : F.obj j), ι F j a = x ∧ ι F j b = y :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.Carrier, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.faceCocone line 378
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.face line 388
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.face_ι line 392
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.globular line 397
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.finite_dimension line 405
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.eventually_dimensionLE line 412
Source documentation
A dimension bound in the colimit becomes a literal bound on a later representative.
```
theorem eventually_dimensionLE {j : J} (n : ℕ) (x : F.obj j)
    (hs : face F false n (ι F j x) = ι F j x)
    (ht : face F true n (ι F j x) = ι F j x) :
    ∃ (k : J) (f : j ⟶ k), (F.obj k).DimensionLE n ((F.map f).toFun x) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.face, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι, OAI.Thomason.Construction.StrictOmegaCategory.DimensionLE
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.exists_composable_representatives line 424
Source documentation
Matching colimit boundaries have representatives with matching boundaries in a single original strict category.
```
theorem exists_composable_representatives (n : ℕ) (x y : Carrier F)
    (h : face F true n x = face F false n y) :
    ∃ (j : J) (a b : F.obj j),
      (F.obj j).target n a = (F.obj j).source n b ∧ ι F j a = x ∧ ι F j b = y := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.Carrier, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.face, OAI.Thomason.Construction.StrictOmegaCategory.target, OAI.Thomason.Construction.StrictOmegaCategory.source, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.exists_representatives_fin line 452
Source documentation
Every finite family of colimit cells is represented at one original stage.
```
theorem exists_representatives_fin (m : ℕ) (s : Fin m → Carrier F) :
    ∃ (j : J) (v : Fin m → F.obj j), ∀ a, ι F j (v a) = s a := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.Carrier, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.eventually_eq_fin line 472
Source documentation
Any finite list of colimit equalities holds literally after one map.
```
theorem eventually_eq_fin {j : J} (m : ℕ) (x y : Fin m → F.obj j)
    (h : ∀ a, ι F j (x a) = ι F j (y a)) :
    ∃ (k : J) (f : j ⟶ k), ∀ a, (F.map f).toFun (x a) = (F.map f).toFun (y a) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.eventually_eq_fin_different line 492
Source documentation
Two finite lists from different stages are identified by two maps to one later stage exactly when all their colimit images agree.
```
theorem eventually_eq_fin_different {j k : J} (m : ℕ)
    (x : Fin m → F.obj j) (y : Fin m → F.obj k)
    (h : ∀ a, ι F j (x a) = ι F k (y a)) :
    ∃ (l : J) (f : j ⟶ l) (g : k ⟶ l),
      ∀ a, (F.map f).toFun (x a) = (F.map g).toFun (y a) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.exists_representatives_with_faces line 510
Source documentation
Any finite list of matching-boundary conditions can be imposed at the same stage as a finite family of representatives.
```
theorem exists_representatives_with_faces (m r : ℕ) (x : Fin m → Carrier F)
    (left right : Fin r → Fin m) (dim : Fin r → ℕ)
    (h : ∀ a, face F true (dim a) (x (left a)) =
      face F false (dim a) (x (right a))) :
    ∃ (j : J) (v : Fin m → F.obj j), (∀ a, ι F j (v a) = x a) ∧
      ∀ a, (F.obj j).target (dim a) (v (left a)) =
        (F.obj j).source (dim a) (v (right a)) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.Carrier, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.face, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι, OAI.Thomason.Construction.StrictOmegaCategory.target, OAI.Thomason.Construction.StrictOmegaCategory.source
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.map_matching line 550
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.composite_representatives_eq line 559
Source documentation
Composites of two representatives of the same matching pair have the same image in the ordinary cell colimit.
```
theorem composite_representatives_eq {j k : J} (n : ℕ)
    (x y : F.obj j) (x' y' : F.obj k)
    (h : (F.obj j).target n x = (F.obj j).source n y)
    (h' : (F.obj k).target n x' = (F.obj k).source n y')
    (hx : ι F j x = ι F k x') (hy : ι F j y = ι F k y') :
    ι F j ((F.obj j).comp n x y h) = ι F k ((F.obj k).comp n x' y' h') := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.target, OAI.Thomason.Construction.StrictOmegaCategory.source, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.comp
structure OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.CompositionRepresentative line 581
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.compositionRepresentative line 589
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.comp line 595
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.comp_ι line 601
Source documentation
The colimit composite agrees with every composable original pair.
```
theorem comp_ι (n : ℕ) (j : J) (x y : F.obj j)
    (h : (F.obj j).target n x = (F.obj j).source n y)
    (h' : face F true n (ι F j x) = face F false n (ι F j y)) :
    comp F n (ι F j x) (ι F j y) h' = ι F j ((F.obj j).comp n x y h) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.target, OAI.Thomason.Construction.StrictOmegaCategory.source, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.face, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.ι, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.comp
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.source_comp line 627
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.target_comp line 633
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.face_comp line 639
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.left_unit line 650
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.right_unit line 657
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.assoc line 664
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.lower_face_comp line 689
Source documentation
Below a composite's composition level, either boundary agrees with the corresponding boundary of its first factor.
```
theorem lower_face_comp (C : StrictOmegaCategory.{0}) (a : Bool) (m n : ℕ)
    (hmn : m < n) (x y : C) (h : C.target n x = C.source n y) :
    C.face a m (C.comp n x y h) = C.face a m x := by
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.interchange line 696
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.category line 745
Source documentation
The ordinary filtered cell colimit, equipped with its constructed strict operations and all the original strict laws.
```
noncomputable def category : StrictOmegaCategory.{0} where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.leg line 778
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.cocone line 783
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.descFunction line 792
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.descFunction_ι line 796
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.desc line 800
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.isColimit line 816
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.cellsIsColimit line 830
Source documentation
Forgetting to cells preserves the constructed filtered colimit exactly.
```
noncomputable def cellsIsColimit : IsColimit (cells.mapCocone (cocone F)) :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.cocone
instance OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.cells_preservesFilteredColimitsOfShape line 834
Source documentation
The actual underlying-cell functor preserves every small filtered colimit.
```
instance cells_preservesFilteredColimitsOfShape : PreservesColimitsOfShape J cells where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.cells
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.cocone_cell_representative line 839
Source documentation
Every cell of any strict colimit of the filtered diagram comes from a stage.
```
theorem cocone_cell_representative {s : Cocone F} (hs : IsColimit s) (x : s.pt) :
    ∃ (j : J) (y : F.obj j), (s.ι.app j).toFun y = x :=
…
```

theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.cocone_cell_eq_iff line 844

Source documentation

Equality in any strict filtered colimit is exactly eventual stage equality.

theorem cocone_cell_eq_iff {s : Cocone F} (hs : IsColimit s)
    {i j : J} (x : F.obj i) (y : F.obj j) :
    (s.ι.app i).toFun x = (s.ι.app j).toFun y ↔
      ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
        (F.map f).toFun x = (F.map g).toFun y :=
…

theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.cocone_eventually_dimensionLE line 853
Source documentation
A dimension bound on the image of an original cell holds at some later stage.
```
theorem cocone_eventually_dimensionLE {s : Cocone F} (hs : IsColimit s)
    {j : J} (n : ℕ) (x : F.obj j) (hx : s.pt.DimensionLE n ((s.ι.app j).toFun x)) :
    ∃ (k : J) (f : j ⟶ k), (F.obj k).DimensionLE n ((F.map f).toFun x) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.DimensionLE
theorem OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.cocone_bounded_representative line 878
Source documentation
Bounded cells in a filtered colimit have bounded original representatives.
```
theorem cocone_bounded_representative {s : Cocone F} (hs : IsColimit s)
    (n : ℕ) (x : s.pt) (hx : s.pt.DimensionLE n x) :
    ∃ (j : J) (y : F.obj j), (F.obj j).DimensionLE n y ∧ (s.ι.app j).toFun y = x := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.DimensionLE
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.boundedCells line 899
Source documentation
The cells fixed by both n-dimensional boundary maps.
```
def boundedCells (n : ℕ) : StrictOmegaCategory.{0} ⥤ Type where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.boundedCellsIsColimit line 907
Source documentation
A filtered strict colimit is a colimit on each bounded-cell set.
```
noncomputable def boundedCellsIsColimit (n : ℕ) (hs : IsColimit s) :
    IsColimit ((boundedCells n).mapCocone s) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.boundedCells
instance OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.boundedCells_preservesFilteredColimitsOfShape line 920
def OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.globeCoyonedaIso line 926
Source documentation
The free globe represents this bounded-cell functor, naturally.
```
def globeCoyonedaIso (n : ℕ) :
    coyoneda.obj (Opposite.op (Globe.category n)) ≅ boundedCells n :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.boundedCells
instance OAI.Thomason.Construction.StrictOmegaCategory.FilteredColimit.globeCoyoneda_preservesFilteredColimitsOfShape line 935
Source documentation
Mapping out of a globe commutes with every small filtered colimit.
```
instance globeCoyoneda_preservesFilteredColimitsOfShape (n : ℕ) :
    PreservesColimitsOfShape J (coyoneda.obj (Opposite.op (Globe.category n))) :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category
def OAI.Thomason.Construction.StrictOmegaCategory.isoOfBijective line 952
Source documentation
A cellwise bijective strict functor has a strict inverse.
```
noncomputable def isoOfBijective {C D : StrictOmegaCategory.{0}} (f : C ⟶ D)
    (hf : Function.Bijective f.toFun) : C ≅ D := by
…
```