LeanPool.DirectedTopologyLean4.FundamentalCategory

theorem Dipath.Dihomotopy.transAssocReparamAux_directed : DirectedMap.Directed { toFun := fun (t : ↑unitInterval) => ⟨Path.Homotopy.transAssocReparamAux t, ⋯⟩, continuous_toFun := ⋯ }

noncomputable def Dipath.Dihomotopy.transAssocReparamAuxMap : D(↑unitInterval,↑unitInterval)

The directed self-map of the unit interval used to associate triple concatenations of dipaths.

Equations

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

theorem Dipath.Dihomotopy.trans_assoc_reparam_directed {X : Type u} [DirectedSpace X] {x₀ x₁ x₂ x₃ : X} (p : Dipath x₀ x₁) (q : Dipath x₁ x₂) (r : Dipath x₂ x₃) : (p.trans q).trans r = (p.trans (q.trans r)).reparam transAssocReparamAuxMap ⋯ ⋯

theorem Dipath.Dihomotopy.trans_assoc {X : Type u} [DirectedSpace X] {x₀ x₁ x₂ x₃ : X} (p : Dipath x₀ x₁) (q : Dipath x₁ x₂) (r : Dipath x₂ x₃) : ((p.trans q).trans r).Dihomotopic (p.trans (q.trans r))

For any three dipaths p q r, (p.trans q).trans r is dihomotopic with p.trans (q.trans r).

structure FundamentalCategory (X : Type u) : Type u

The fundamental category of a type, wrapping the underlying element as as.

• as : X

  The underlying element of the type.

theorem FundamentalCategory.ext {X : Type u} {x y : FundamentalCategory X} (as : x.as = y.as) : x = y

theorem FundamentalCategory.ext_iff {X : Type u} {x y : FundamentalCategory X} : x = y ↔ x.as = y.as

def FundamentalCategory.equiv (X : Type u_1) : FundamentalCategory X ≃ X

The fundamental-category wrapper is type-equivalent to the underlying type.

Equations

• FundamentalCategory.equiv X = { toFun := fun (x : FundamentalCategory X) => x.as, invFun := fun (x : X) => { as := x }, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem FundamentalCategory.equiv_symm_apply_as (X : Type u_1) (x : X) : ((equiv X).symm x).as = x

@[simp]

theorem FundamentalCategory.equiv_apply (X : Type u_1) (x : FundamentalCategory X) : (equiv X) x = x.as

@[simp]

theorem FundamentalCategory.isEmpty_iff (X : Type u_1) : IsEmpty (FundamentalCategory X) ↔ IsEmpty X

instance FundamentalCategory.instIsEmpty (X : Type u_1) [IsEmpty X] : IsEmpty (FundamentalCategory X)

@[simp]

theorem FundamentalCategory.nonempty_iff (X : Type u_1) : Nonempty (FundamentalCategory X) ↔ Nonempty X

instance FundamentalCategory.instNonempty (X : Type u_1) [Nonempty X] : Nonempty (FundamentalCategory X)

@[simp]

theorem FundamentalCategory.subsingleton_iff (X : Type u_1) : Subsingleton (FundamentalCategory X) ↔ Subsingleton X

instance FundamentalCategory.instSubsingleton (X : Type u_1) [Subsingleton X] : Subsingleton (FundamentalCategory X)

@[implicit_reducible]

instance FundamentalCategory.instInhabited {X : Type u} [Inhabited X] : Inhabited (FundamentalCategory X)

Equations

• FundamentalCategory.instInhabited = { default := { as := default } }

@[implicit_reducible]

noncomputable instance FundamentalCategory.instCategory {X : Type u} [DirectedSpace X] : CategoryTheory.Category.{u, u} (FundamentalCategory X)

Equations

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

theorem FundamentalCategory.comp_eq {X : Type u} [DirectedSpace X] (x y z : FundamentalCategory X) (p : x ⟶ y) (q : y ⟶ z) : CategoryTheory.CategoryStruct.comp p q = Dipath.Dihomotopic.Quotient.comp p q

theorem FundamentalCategory.id_eq_path_refl {X : Type u} [DirectedSpace X] (x : FundamentalCategory X) : CategoryTheory.CategoryStruct.id x = ⟦Dipath.refl x.as⟧

def FundamentalCategory.mapFunctor {X : Type u_1} {Y : Type u_2} [DirectedSpace X] [DirectedSpace Y] (f : D(X,Y)) : CategoryTheory.Functor (FundamentalCategory X) (FundamentalCategory Y)

The functor on fundamental categories induced by a directed map.

Equations

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

@[simp]

theorem FundamentalCategory.mapFunctor_map {X : Type u_1} {Y : Type u_2} [DirectedSpace X] [DirectedSpace Y] (f : D(X,Y)) {x✝ x✝¹ : FundamentalCategory X} (p : x✝ ⟶ x✝¹) : (mapFunctor f).map p = Dipath.Dihomotopic.Quotient.mapFn p f

@[simp]

theorem FundamentalCategory.mapFunctor_obj_as {X : Type u_1} {Y : Type u_2} [DirectedSpace X] [DirectedSpace Y] (f : D(X,Y)) (x : FundamentalCategory X) : ((mapFunctor f).obj x).as = f x.as

@[simp]

theorem FundamentalCategory.mapFunctor_id (X : Type u_1) [DirectedSpace X] : mapFunctor (DirectedMap.id X) = CategoryTheory.Functor.id (FundamentalCategory X)

@[simp]

theorem FundamentalCategory.mapFunctor_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DirectedSpace X] [DirectedSpace Y] [DirectedSpace Z] (f : D(X,Y)) (g : D(Y,Z)) : mapFunctor (g.comp f) = (mapFunctor f).comp (mapFunctor g)

noncomputable def FundamentalCategory.fundamentalCategoryFunctor : CategoryTheory.Functor dTopCat CategoryTheory.Cat

The fundamental-category functor dTopCat ⥤ Cat sending a directed space to its fundamental category.

Equations

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

def FundamentalCategory.termDπ : Lean.ParserDescr

Notation for the fundamental-category functor dTopCat ⥤ Cat.

Equations

• FundamentalCategory.termDπ = Lean.ParserDescr.node `FundamentalCategory.termDπ 1024 (Lean.ParserDescr.symbol "dπ")

def FundamentalCategory.termDπₓ : Lean.ParserDescr

Notation for the object part of the fundamental-category functor.

Equations

• FundamentalCategory.termDπₓ = Lean.ParserDescr.node `FundamentalCategory.termDπₓ 1024 (Lean.ParserDescr.symbol "dπₓ")

@[reducible]

noncomputable def FundamentalCategory.fundamentalCategoryMap {X Y : dTopCat} (f : X ⟶ Y) : CategoryTheory.Functor ↑(fundamentalCategoryFunctor.obj X) ↑(fundamentalCategoryFunctor.obj Y)

The underlying functor (not just Cat.Hom) induced by a dTopCat map.

Equations

• FundamentalCategory.fundamentalCategoryMap f = (FundamentalCategory.fundamentalCategoryFunctor.map f).toFunctor

def FundamentalCategory.termDπₘ : Lean.ParserDescr

Notation for the underlying functor on fundamental categories induced by a dTopCat map.

Equations

• FundamentalCategory.termDπₘ = Lean.ParserDescr.node `FundamentalCategory.termDπₘ 1024 (Lean.ParserDescr.symbol "dπₘ")

theorem FundamentalCategory.map_eq {X Y : dTopCat} {x₀ x₁ : ↑X} (f : X ⟶ Y) (p : Dipath.Dihomotopic.Quotient x₀ x₁) : (fundamentalCategoryMap f).map p = p.mapFn (dTopCat.Hom.hom f)

@[reducible]

def FundamentalCategory.toTop {X : dTopCat} (x : ↑(fundamentalCategoryFunctor.obj X)) : ↑X

Help the typechecker by converting a point in the fundamental category back to a point in the underlying directed space.

Equations

• FundamentalCategory.toTop x = x.as

@[reducible]

def FundamentalCategory.fromTop {X : dTopCat} (x : ↑X) : ↑(fundamentalCategoryFunctor.obj X)

Help the typechecker by converting a point in a directed space to a point in the fundamental category of that space

Equations

• FundamentalCategory.fromTop x = { as := x }

@[reducible]

def FundamentalCategory.toPath {X : dTopCat} {x₀ x₁ : ↑(fundamentalCategoryFunctor.obj X)} (p : x₀ ⟶ x₁) : Dipath.Dihomotopic.Quotient x₀.as x₁.as

Help the typechecker by converting an arrow in the fundamental category of a directed space back to a directed path in that space (i.e., Dipath.Dihomotopic.Quotient).

Equations

• FundamentalCategory.toPath p = p

@[reducible]

def FundamentalCategory.fromPath {X : dTopCat} {x₀ x₁ : ↑X} (p : Dipath.Dihomotopic.Quotient x₀ x₁) : { as := x₀ } ⟶ { as := x₁ }

Help the typechecker by convering a directed path in a directed space to an arrow in the fundamental category of that space.

Equations

• FundamentalCategory.fromPath p = p