LeanPool.DirectedTopologyLean4.DirectedVanKampen

theorem DirectedVanKampen.PushoutFunctor.subset_functor_trans {C : CategoryTheory.Cat} {Y : dTopCat} {Y₀ : Set ↑Y} {F : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑Y₀)) ↑C} {x y z : ↑Y} {γ₁ : Dipath x y} {γ₂ : Dipath y z} (hγ : Set.range ⇑(γ₁.trans γ₂) ⊆ Y₀) : CategoryTheory.CategoryStruct.comp (F.map ⟦DiSubtype.SubtypeDipath γ₁ ⋯⟧) (F.map ⟦DiSubtype.SubtypeDipath γ₂ ⋯⟧) = F.map ⟦DiSubtype.SubtypeDipath (γ₁.trans γ₂) hγ⟧

theorem DirectedVanKampen.PushoutFunctor.subset_functor_reparam {C : CategoryTheory.Cat} {Y : dTopCat} {Y₀ : Set ↑Y} {F : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑Y₀)) ↑C} {x y : ↑Y} {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ Y₀) {f : D(↑unitInterval,↑unitInterval)} (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : F.map ⟦DiSubtype.SubtypeDipath (γ.reparam f hf₀ hf₁) ⋯⟧ = F.map ⟦DiSubtype.SubtypeDipath γ hγ⟧

theorem DirectedVanKampen.PushoutFunctor.functor_cast {C : CategoryTheory.Cat} {X : dTopCat} (F : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj X) ↑C) {x y x' y' : ↑X} (γ : Dipath x y) (hx : x' = x) (hy : y' = y) : F.map ⟦γ.cast hx hy⟧ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (F.map ⟦γ⟧) (CategoryTheory.eqToHom ⋯))

@[simp]

theorem DirectedVanKampen.PushoutFunctor.functor_cast_heq {C : CategoryTheory.Cat} {X : dTopCat} (F : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj X) ↑C) {x y x' y' : ↑X} (γ : Dipath x y) (hx : x' = x) (hy : y' = y) : F.map ⟦γ.cast hx hy⟧ ≍ F.map ⟦γ⟧

noncomputable def DirectedVanKampen.PushoutFunctor.FunctorOnObj {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} (F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C) (F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C) (x : ↑(FundamentalCategory.fundamentalCategoryFunctor.obj X)) : ↑C

Object map for the pushout functor induced by the covering square.

Equations

• DirectedVanKampen.PushoutFunctor.FunctorOnObj hX F₁ F₂ x = ⋯.by_cases (fun (hx : x.as ∈ X₁) => F₁.obj { as := ⟨x.as, hx⟩ }) fun (hx : x.as ∈ X₂) => F₂.obj { as := ⟨x.as, hx⟩ }

theorem DirectedVanKampen.PushoutFunctor.functorOnObj_apply_one {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x : ↑X} (hx : x ∈ X₁) : F₁.obj { as := ⟨x, hx⟩ } = FunctorOnObj hX F₁ F₂ { as := x }

theorem DirectedVanKampen.PushoutFunctor.functorOnObj_apply_two {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x : ↑X} (hx₂ : x ∈ X₂) : F₂.obj { as := ⟨x, hx₂⟩ } = FunctorOnObj hX F₁ F₂ { as := x }

noncomputable def DirectedVanKampen.PushoutFunctor.FunctorOnHomOfCoveredAux₁ {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₁) : FunctorOnObj hX F₁ F₂ { as := x } ⟶ FunctorOnObj hX F₁ F₂ { as := y }

Map assigned to a path whose image lies in the first open subset.

Equations

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

noncomputable def DirectedVanKampen.PushoutFunctor.FunctorOnHomOfCoveredAux₂ {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₂) : FunctorOnObj hX F₁ F₂ { as := x } ⟶ FunctorOnObj hX F₁ F₂ { as := y }

Map assigned to a path whose image lies in the second open subset.

Equations

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

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredAux₁_trans {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y z : ↑X} {γ₁ : Dipath x y} {γ₂ : Dipath y z} (hγ : Set.range ⇑(γ₁.trans γ₂) ⊆ X₁) : FunctorOnHomOfCoveredAux₁ hX h_comm hγ = CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCoveredAux₁ hX h_comm ⋯) (FunctorOnHomOfCoveredAux₁ hX h_comm ⋯)

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredAux₂_trans {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y z : ↑X} {γ₁ : Dipath x y} {γ₂ : Dipath y z} (hγ : Set.range ⇑(γ₁.trans γ₂) ⊆ X₂) : FunctorOnHomOfCoveredAux₂ hX h_comm hγ = CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCoveredAux₂ hX h_comm ⋯) (FunctorOnHomOfCoveredAux₂ hX h_comm ⋯)

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredAux₁_reparam {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y : ↑X} {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₁) {f : D(↑unitInterval,↑unitInterval)} (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : FunctorOnHomOfCoveredAux₁ hX h_comm hγ = FunctorOnHomOfCoveredAux₁ hX h_comm ⋯

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredAux₂_reparam {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y : ↑X} {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₂) {f : D(↑unitInterval,↑unitInterval)} (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : FunctorOnHomOfCoveredAux₂ hX h_comm hγ = FunctorOnHomOfCoveredAux₂ hX h_comm ⋯

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredAux₁_refl {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x : ↑X} (hx : x ∈ X₁) : FunctorOnHomOfCoveredAux₁ hX h_comm ⋯ = CategoryTheory.CategoryStruct.id (FunctorOnObj hX F₁ F₂ { as := x })

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredAux₂_refl {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x : ↑X} (hx : x ∈ X₂) : FunctorOnHomOfCoveredAux₂ hX h_comm ⋯ = CategoryTheory.CategoryStruct.id (FunctorOnObj hX F₁ F₂ { as := x })

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredAux_equal {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {γ : Dipath x y} (hγ₁ : Set.range ⇑γ ⊆ X₁) (hγ₂ : Set.range ⇑γ ⊆ X₂) : FunctorOnHomOfCoveredAux₁ hX h_comm hγ₁ = FunctorOnHomOfCoveredAux₂ hX h_comm hγ₂

noncomputable def DirectedVanKampen.PushoutFunctor.FunctorOnHomOfCovered {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {γ : Dipath x y} (hγ : Dipath.covered hX γ) : FunctorOnObj hX F₁ F₂ { as := x } ⟶ FunctorOnObj hX F₁ F₂ { as := y }

Map assigned to a path covered by one of the two open subsets.

Equations

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

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_apply_left {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₁) : FunctorOnHomOfCovered hX h_comm ⋯ = FunctorOnHomOfCoveredAux₁ hX h_comm hγ

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_apply_left' {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₁) : FunctorOnHomOfCovered hX h_comm ⋯ = FunctorOnHomOfCoveredAux₁ hX h_comm hγ

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_apply_right {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₂) : FunctorOnHomOfCovered hX h_comm ⋯ = FunctorOnHomOfCoveredAux₂ hX h_comm hγ

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_equal {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {γ₁ γ₂ : Dipath x y} (h : γ₁ = γ₂) (hγ₁ : Dipath.covered hX γ₁) (hγ₂ : Dipath.covered hX γ₂) : FunctorOnHomOfCovered hX h_comm hγ₁ = FunctorOnHomOfCovered hX h_comm hγ₂

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_heq_of_ext {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y x' y' : ↑X} {γ : Dipath x y} {γ' : Dipath x' y'} (h : ∀ (t : ↑unitInterval), γ t = γ' t) (hγ : Dipath.covered hX γ) (hγ' : Dipath.covered hX γ') : FunctorOnHomOfCovered hX h_comm hγ ≍ FunctorOnHomOfCovered hX h_comm hγ'

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_refl {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) : FunctorOnHomOfCovered hX h_comm ⋯ = CategoryTheory.CategoryStruct.id (FunctorOnObj hX F₁ F₂ { as := x })

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_apply_right' {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {γ : Dipath x y} (hγ : Set.range ⇑γ ⊆ X₂) : FunctorOnHomOfCovered hX h_comm ⋯ = FunctorOnHomOfCoveredAux₂ hX h_comm hγ

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_trans {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y z : ↑X} {γ₁ : Dipath x y} {γ₂ : Dipath y z} (hγ : Dipath.covered hX (γ₁.trans γ₂)) : FunctorOnHomOfCovered hX h_comm hγ = CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCovered hX h_comm ⋯) (FunctorOnHomOfCovered hX h_comm ⋯)

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_reparam {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y : ↑X} {γ : Dipath x y} (hγ : Dipath.covered hX γ) {f : D(↑unitInterval,↑unitInterval)} (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : FunctorOnHomOfCovered hX h_comm hγ = FunctorOnHomOfCovered hX h_comm ⋯

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_cast {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y x' y' : ↑X} {γ : Dipath x y} (hγ : Dipath.covered hX γ) (hx : x' = x) (hy : y' = y) : FunctorOnHomOfCovered hX h_comm ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCovered hX h_comm hγ) (CategoryTheory.eqToHom ⋯))

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_cast_left {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y x' : ↑X} {γ : Dipath x y} (hγ : Dipath.covered hX γ) (hx : x' = x) : FunctorOnHomOfCovered hX h_comm ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (FunctorOnHomOfCovered hX h_comm hγ)

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_cast_right {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y y' : ↑X} {γ : Dipath x y} (hγ : Dipath.covered hX γ) (hy : y' = y) : FunctorOnHomOfCovered hX h_comm ⋯ = CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCovered hX h_comm hγ) (CategoryTheory.eqToHom ⋯)

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_split_comp {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y : ↑X} {γ : Dipath x y} (hγ : Dipath.covered hX γ) {T : ↑unitInterval} (hT₀ : 0 < T) (hT₁ : T < 1) : FunctorOnHomOfCovered hX h_comm hγ = CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCovered hX h_comm ⋯) (FunctorOnHomOfCovered hX h_comm ⋯)

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCovered_dihomotopic {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y : ↑X} {γ γ' : Dipath x y} {F : γ.Dihomotopy γ'} (hF : Dipath.Dihomotopy.covered hX F) : FunctorOnHomOfCovered hX h_comm ⋯ = FunctorOnHomOfCovered hX h_comm ⋯

noncomputable def DirectedVanKampen.PushoutFunctor.FunctorOnHomOfCoveredPartwiseAux {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {n : ℕ} (x y : ↑X) (γ : Dipath x y) : Dipath.coveredPartwise hX γ n → (FunctorOnObj hX F₁ F₂ { as := x } ⟶ FunctorOnObj hX F₁ F₂ { as := y })

Recursive map on paths split into finitely many covered pieces.

Equations

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

@[reducible, inline]

noncomputable abbrev DirectedVanKampen.PushoutFunctor.FunctorOnHomOfCoveredPartwise {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {n : ℕ} {x y : ↑X} {γ : Dipath x y} (hγ : Dipath.coveredPartwise hX γ n) : FunctorOnObj hX F₁ F₂ { as := x } ⟶ FunctorOnObj hX F₁ F₂ { as := y }

Map assigned to a path equipped with a proof that it is piecewise covered.

Equations

• DirectedVanKampen.PushoutFunctor.FunctorOnHomOfCoveredPartwise hX h_comm hγ = DirectedVanKampen.PushoutFunctor.FunctorOnHomOfCoveredPartwiseAux hX h_comm x y γ hγ

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_apply_0 {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y : ↑X} {γ : Dipath x y} (hγ : Dipath.coveredPartwise hX γ 0) : FunctorOnHomOfCoveredPartwise hX h_comm hγ = FunctorOnHomOfCovered hX h_comm hγ

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_apply_succ {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {n : ℕ} {x y : ↑X} {γ : Dipath x y} (hγ : Dipath.coveredPartwise hX γ n.succ) : FunctorOnHomOfCoveredPartwise hX h_comm hγ = CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCovered hX h_comm ⋯) (FunctorOnHomOfCoveredPartwise hX h_comm ⋯)

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_equal {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {n : ℕ} {γ₁ γ₂ : Dipath x y} (h : γ₁ = γ₂) (hγ₁ : Dipath.coveredPartwise hX γ₁ n) (hγ₂ : Dipath.coveredPartwise hX γ₂ n) : FunctorOnHomOfCoveredPartwise hX h_comm hγ₁ = FunctorOnHomOfCoveredPartwise hX h_comm hγ₂

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_equal' {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {n m : ℕ} {γ₁ γ₂ : Dipath x y} (h₁ : γ₁ = γ₂) (h₂ : n = m) (hγ₁ : Dipath.coveredPartwise hX γ₁ n) (hγ₂ : Dipath.coveredPartwise hX γ₂ m) : FunctorOnHomOfCoveredPartwise hX h_comm hγ₁ = FunctorOnHomOfCoveredPartwise hX h_comm hγ₂

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_heq_of_ext {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {n m : ℕ} {x y x' y' : ↑X} {γ : Dipath x y} {γ' : Dipath x' y'} (h : ∀ (t : ↑unitInterval), γ t = γ' t) (hn : n = m) (hγ : Dipath.coveredPartwise hX γ n) (hγ' : Dipath.coveredPartwise hX γ' m) : FunctorOnHomOfCoveredPartwise hX h_comm hγ ≍ FunctorOnHomOfCoveredPartwise hX h_comm hγ'

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_cast_params {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {n m : ℕ} {γ₁ γ₂ : Dipath x y} (h₁ : γ₁ = γ₂) (h₂ : n = m) (hγ₁ : Dipath.coveredPartwise hX γ₁ n) : FunctorOnHomOfCoveredPartwise hX h_comm hγ₁ = FunctorOnHomOfCoveredPartwise hX h_comm ⋯

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_cast {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y x' y' : ↑X} {n : ℕ} {γ : Dipath x y} (hγ : Dipath.coveredPartwise hX γ n) (hx : x' = x) (hy : y' = y) : FunctorOnHomOfCoveredPartwise hX h_comm ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCoveredPartwise hX h_comm hγ) (CategoryTheory.eqToHom ⋯))

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_cast_left {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y x' : ↑X} {n : ℕ} {γ : Dipath x y} (hγ : Dipath.coveredPartwise hX γ n) (hx : x' = x) : FunctorOnHomOfCoveredPartwise hX h_comm ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (FunctorOnHomOfCoveredPartwise hX h_comm hγ)

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_cast_right {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y y' : ↑X} {n : ℕ} {γ : Dipath x y} (hγ : Dipath.coveredPartwise hX γ n) (hy : y' = y) : FunctorOnHomOfCoveredPartwise hX h_comm ⋯ = CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCoveredPartwise hX h_comm hγ) (CategoryTheory.eqToHom ⋯)

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_refine_of_covered {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) (k : ℕ) {x y : ↑X} {γ : Dipath x y} (hγ : Dipath.covered hX γ) : FunctorOnHomOfCoveredPartwise hX h_comm ⋯ = FunctorOnHomOfCoveredPartwise hX h_comm ⋯

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_split {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {n d : ℕ} (hdn : n > d) {x y : ↑X} {γ : Dipath x y} (hγ : Dipath.coveredPartwise hX γ n) : FunctorOnHomOfCoveredPartwise hX h_comm hγ = CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCoveredPartwise hX h_comm ⋯) (FunctorOnHomOfCoveredPartwise hX h_comm ⋯)

When a path is partwise covered by n + 1 paths, applying Fₙ to the two restrictions and composing gives Fₙ γ.

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_refine_apply {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) (n k : ℕ) {x y : ↑X} {γ : Dipath x y} (hγ : Dipath.coveredPartwise hX γ n.succ) : FunctorOnHomOfCoveredPartwise hX h_comm ⋯ = CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCoveredPartwise hX h_comm ⋯) (FunctorOnHomOfCoveredPartwise hX h_comm ⋯)

If a path can be covered partwise by (n + 1) ≥ 2 parts, its refinement to k * (n + 1) parts is the composition of covering the first part in k parts and the second part in k * n parts.

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_refine {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {n : ℕ} (k : ℕ) {x y : ↑X} {γ : Dipath x y} (hγ_n : Dipath.coveredPartwise hX γ n) : FunctorOnHomOfCoveredPartwise hX h_comm hγ_n = FunctorOnHomOfCoveredPartwise hX h_comm ⋯

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_apply_right_side {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y : ↑X} {γ : Dipath x y} {n : ℕ} (hγ : Dipath.coveredPartwise hX γ n.succ) : FunctorOnHomOfCoveredPartwise hX h_comm hγ = CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCoveredPartwise hX h_comm ⋯) (FunctorOnHomOfCovered hX h_comm ⋯)

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_trans_case_0 {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y z : ↑X} {γ₁ : Dipath x y} {γ₂ : Dipath y z} (hγ₁ : Dipath.coveredPartwise hX γ₁ 0) (hγ₂ : Dipath.coveredPartwise hX γ₂ 0) : FunctorOnHomOfCoveredPartwise hX h_comm ⋯ = CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCoveredPartwise hX h_comm hγ₁) (FunctorOnHomOfCoveredPartwise hX h_comm hγ₂)

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_trans {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {n : ℕ} {x y z : ↑X} {γ₁ : Dipath x y} {γ₂ : Dipath y z} (hγ₁ : Dipath.coveredPartwise hX γ₁ n) (hγ₂ : Dipath.coveredPartwise hX γ₂ n) : FunctorOnHomOfCoveredPartwise hX h_comm ⋯ = CategoryTheory.CategoryStruct.comp (FunctorOnHomOfCoveredPartwise hX h_comm hγ₁) (FunctorOnHomOfCoveredPartwise hX h_comm hγ₂)

theorem DirectedVanKampen.PushoutFunctor.functorOnHomOfCoveredPartwise_unique {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {n m : ℕ} {γ : Dipath x y} (hγ_n : Dipath.coveredPartwise hX γ n) (hγ_m : Dipath.coveredPartwise hX γ m) : FunctorOnHomOfCoveredPartwise hX h_comm hγ_n = FunctorOnHomOfCoveredPartwise hX h_comm hγ_m

noncomputable def DirectedVanKampen.PushoutFunctor.FunctorOnHomAux {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) (γ : Dipath x y) : FunctorOnObj hX F₁ F₂ { as := x } ⟶ FunctorOnObj hX F₁ F₂ { as := y }

Map on arbitrary directed paths, choosing a covered subdivision.

Equations

• DirectedVanKampen.PushoutFunctor.FunctorOnHomAux hX X₁_open X₂_open h_comm γ = DirectedVanKampen.PushoutFunctor.FunctorOnHomOfCoveredPartwise hX h_comm ⋯

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_apply {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {n : ℕ} {γ : Dipath x y} (hγ : Dipath.coveredPartwise hX γ n) : FunctorOnHomAux hX X₁_open X₂_open h_comm γ = FunctorOnHomOfCoveredPartwise hX h_comm hγ

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_refl {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x : ↑X} : FunctorOnHomAux hX X₁_open X₂_open h_comm (Dipath.refl x) = CategoryTheory.CategoryStruct.id (FunctorOnObj hX F₁ F₂ { as := x })

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_cast {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y x' y' : ↑X} (γ : Dipath x y) (hx : x' = x) (hy : y' = y) : FunctorOnHomAux hX X₁_open X₂_open h_comm (γ.cast hx hy) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (FunctorOnHomAux hX X₁_open X₂_open h_comm γ) (CategoryTheory.eqToHom ⋯))

@[simp]

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_cast_heq {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y x' y' : ↑X} (γ : Dipath x y) (hx : x' = x) (hy : y' = y) : FunctorOnHomAux hX X₁_open X₂_open h_comm (γ.cast hx hy) ≍ FunctorOnHomAux hX X₁_open X₂_open h_comm γ

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_heq_of_ext {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y x' y' : ↑X} {γ : Dipath x y} {γ' : Dipath x' y'} (h : ∀ (t : ↑unitInterval), γ t = γ' t) : FunctorOnHomAux hX X₁_open X₂_open h_comm γ ≍ FunctorOnHomAux hX X₁_open X₂_open h_comm γ'

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_trans {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y z : ↑X} (γ₁ : Dipath x y) (γ₂ : Dipath y z) : FunctorOnHomAux hX X₁_open X₂_open h_comm (γ₁.trans γ₂) = CategoryTheory.CategoryStruct.comp (FunctorOnHomAux hX X₁_open X₂_open h_comm γ₁) (FunctorOnHomAux hX X₁_open X₂_open h_comm γ₂)

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_split_of_covered_partwise {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y : ↑X} {γ : Dipath x y} {n : ℕ} (hγ : Dipath.coveredPartwise hX γ n.succ) : FunctorOnHomAux hX X₁_open X₂_open h_comm γ = CategoryTheory.CategoryStruct.comp (FunctorOnHomAux hX X₁_open X₂_open h_comm (SplitDipath.FirstPart γ (Fraction ⋯ ⋯))) (FunctorOnHomAux hX X₁_open X₂_open h_comm (SplitDipath.SecondPart γ (Fraction ⋯ ⋯)))

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_of_covered_dihomotopic {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y : ↑X} {γ γ' : Dipath x y} {F : γ.Dihomotopy γ'} (hF : Dipath.Dihomotopy.covered hX F) : FunctorOnHomAux hX X₁_open X₂_open h_comm γ = FunctorOnHomAux hX X₁_open X₂_open h_comm γ'

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_of_homotopic_dimaps_0 {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {f g : D(↑unitInterval,↑X)} {H : f.Dihomotopy g} (hcov : DirectedMap.Dihomotopy.coveredPartwise hX H 0 0) : CategoryTheory.CategoryStruct.comp (FunctorOnHomAux hX X₁_open X₂_open h_comm (Dipath.ofDirectedMap f)) (FunctorOnHomAux hX X₁_open X₂_open h_comm (H.evalAtRight 1)) = CategoryTheory.CategoryStruct.comp (FunctorOnHomAux hX X₁_open X₂_open h_comm (H.evalAtRight 0)) (FunctorOnHomAux hX X₁_open X₂_open h_comm (Dipath.ofDirectedMap g))

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_of_homotopic_dimaps {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {m : ℕ} {f g : D(↑unitInterval,↑X)} {H : f.Dihomotopy g} : DirectedMap.Dihomotopy.coveredPartwise hX H 0 m → CategoryTheory.CategoryStruct.comp (FunctorOnHomAux hX X₁_open X₂_open h_comm (Dipath.ofDirectedMap f)) (FunctorOnHomAux hX X₁_open X₂_open h_comm (H.evalAtRight 1)) = CategoryTheory.CategoryStruct.comp (FunctorOnHomAux hX X₁_open X₂_open h_comm (H.evalAtRight 0)) (FunctorOnHomAux hX X₁_open X₂_open h_comm (Dipath.ofDirectedMap g))

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_of_covered_dihomotopic_zero_m {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {m : ℕ} {x y : ↑X} {γ γ' : Dipath x y} (h : Dipath.Dihomotopy.dihomotopicCovered hX γ γ' 0 m) : FunctorOnHomAux hX X₁_open X₂_open h_comm γ = FunctorOnHomAux hX X₁_open X₂_open h_comm γ'

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_of_partwise_covered_dihomotopic {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {n m : ℕ} {x y : ↑X} {γ γ' : Dipath x y} : Dipath.Dihomotopy.dihomotopicCovered hX γ γ' n m → FunctorOnHomAux hX X₁_open X₂_open h_comm γ = FunctorOnHomAux hX X₁_open X₂_open h_comm γ'

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_of_pre_dihomotopic {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {γ γ' : Dipath x y} (h : γ.PreDihomotopic γ') : FunctorOnHomAux hX X₁_open X₂_open h_comm γ = FunctorOnHomAux hX X₁_open X₂_open h_comm γ'

theorem DirectedVanKampen.PushoutFunctor.functorOnHomAux_of_dihomotopic {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) (γ γ' : Dipath x y) (h : γ.Dihomotopic γ') : FunctorOnHomAux hX X₁_open X₂_open h_comm γ = FunctorOnHomAux hX X₁_open X₂_open h_comm γ'

noncomputable def DirectedVanKampen.PushoutFunctor.FunctorOnHom {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y : ↑(FundamentalCategory.fundamentalCategoryFunctor.obj X)} (γ : x ⟶ y) : FunctorOnObj hX F₁ F₂ x ⟶ FunctorOnObj hX F₁ F₂ y

Map on morphisms of the directed fundamental category.

Equations

• DirectedVanKampen.PushoutFunctor.FunctorOnHom hX X₁_open X₂_open h_comm γ = Quotient.liftOn γ (DirectedVanKampen.PushoutFunctor.FunctorOnHomAux hX X₁_open X₂_open h_comm) ⋯

theorem DirectedVanKampen.PushoutFunctor.functorOnHom_apply {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {x y : ↑X} {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) (γ : Dipath x y) : FunctorOnHom hX X₁_open X₂_open h_comm ⟦γ⟧ = FunctorOnHomAux hX X₁_open X₂_open h_comm γ

theorem DirectedVanKampen.PushoutFunctor.functorOnHom_trans {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y z : ↑X} (γ₁ : Dipath x y) (γ₂ : Dipath y z) : FunctorOnHom hX X₁_open X₂_open h_comm ⟦γ₁.trans γ₂⟧ = CategoryTheory.CategoryStruct.comp (FunctorOnHom hX X₁_open X₂_open h_comm ⟦γ₁⟧) (FunctorOnHom hX X₁_open X₂_open h_comm ⟦γ₂⟧)

theorem DirectedVanKampen.PushoutFunctor.functorOnHom_id {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) (x : ↑(FundamentalCategory.fundamentalCategoryFunctor.obj X)) : FunctorOnHom hX X₁_open X₂_open h_comm (CategoryTheory.CategoryStruct.id x) = CategoryTheory.CategoryStruct.id (FunctorOnObj hX F₁ F₂ x)

theorem DirectedVanKampen.PushoutFunctor.functorOnHom_comp_path {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y z : ↑X} (γ₁ : Dipath x y) (γ₂ : Dipath y z) : FunctorOnHom hX X₁_open X₂_open h_comm (CategoryTheory.CategoryStruct.comp ⟦γ₁⟧ ⟦γ₂⟧) = CategoryTheory.CategoryStruct.comp (FunctorOnHom hX X₁_open X₂_open h_comm ⟦γ₁⟧) (FunctorOnHom hX X₁_open X₂_open h_comm ⟦γ₂⟧)

theorem DirectedVanKampen.PushoutFunctor.functorOnHom_comp {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y z : ↑(FundamentalCategory.fundamentalCategoryFunctor.obj X)} (γ₁ : x ⟶ y) (γ₂ : y ⟶ z) : FunctorOnHom hX X₁_open X₂_open h_comm (CategoryTheory.CategoryStruct.comp γ₁ γ₂) = CategoryTheory.CategoryStruct.comp (FunctorOnHom hX X₁_open X₂_open h_comm γ₁) (FunctorOnHom hX X₁_open X₂_open h_comm γ₂)

noncomputable def DirectedVanKampen.PushoutFunctor.Functor {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj X) ↑C

The pushout functor from the directed fundamental category of X to C.

Equations

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

theorem DirectedVanKampen.PushoutFunctor.functorObj_def {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x : ↑(FundamentalCategory.fundamentalCategoryFunctor.obj X)} : (Functor hX X₁_open X₂_open h_comm).obj x = FunctorOnObj hX F₁ F₂ x

theorem DirectedVanKampen.PushoutFunctor.functorHom_def {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y : ↑(FundamentalCategory.fundamentalCategoryFunctor.obj X)} (f : x ⟶ y) : (Functor hX X₁_open X₂_open h_comm).map f = FunctorOnHom hX X₁_open X₂_open h_comm f

theorem DirectedVanKampen.PushoutFunctor.functor_comp_left_object {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) (x : ↑X₁) : (Functor hX X₁_open X₂_open h_comm).obj ((FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₁)).obj { as := x }) = F₁.obj { as := x }

theorem DirectedVanKampen.PushoutFunctor.functor_comp_left_dipath {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y : ↑X₁} (γ : Dipath x y) : FunctorOnHom hX X₁_open X₂_open h_comm ((FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₁)).map ⟦γ⟧) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (F₁.map ⟦γ⟧) (CategoryTheory.eqToHom ⋯))

theorem DirectedVanKampen.PushoutFunctor.functor_comp_left {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₁)).comp (Functor hX X₁_open X₂_open h_comm) = F₁

theorem DirectedVanKampen.PushoutFunctor.functor_comp_right_object {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) (x : ↑X₂) : (Functor hX X₁_open X₂_open h_comm).obj ((FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₂)).obj { as := x }) = F₂.obj { as := x }

theorem DirectedVanKampen.PushoutFunctor.functor_comp_right_dipath {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) {x y : ↑X₂} (γ : Dipath x y) : FunctorOnHom hX X₁_open X₂_open h_comm ((FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₂)).map ⟦γ⟧) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (F₂.map ⟦γ⟧) (CategoryTheory.eqToHom ⋯))

theorem DirectedVanKampen.PushoutFunctor.functor_comp_right {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₂)).comp (Functor hX X₁_open X₂_open h_comm) = F₂

theorem DirectedVanKampen.PushoutFunctor.functor_uniq_aux_obj {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) (F' : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj X) ↑C) (h₁ : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₁)).comp F' = F₁) (h₂ : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₂)).comp F' = F₂) (x : ↑X) : F'.obj { as := x } = (Functor hX X₁_open X₂_open h_comm).obj { as := x }

theorem DirectedVanKampen.PushoutFunctor.functor_uniq_of_covered {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) (F' : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj X) ↑C) (h₁ : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₁)).comp F' = F₁) (h₂ : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₂)).comp F' = F₂) {x y : ↑X} {γ : Dipath x y} (hγ : Dipath.covered hX γ) : F'.map ⟦γ⟧ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((Functor hX X₁_open X₂_open h_comm).map ⟦γ⟧) (CategoryTheory.eqToHom ⋯))

theorem DirectedVanKampen.PushoutFunctor.functor_uniq_aux_map {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) (F' : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj X) ↑C) (h₁ : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₁)).comp F' = F₁) (h₂ : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₂)).comp F' = F₂) {n : ℕ} {x y : ↑X} {γ : Dipath x y} : Dipath.coveredPartwise hX γ n → F'.map ⟦γ⟧ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((Functor hX X₁_open X₂_open h_comm).map ⟦γ⟧) (CategoryTheory.eqToHom ⋯))

theorem DirectedVanKampen.PushoutFunctor.functor_uniq {X : dTopCat} {X₁ X₂ : Set ↑X} (hX : X₁ ∪ X₂ = Set.univ) (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) {C : CategoryTheory.Cat} {F₁ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₁)) ↑C} {F₂ : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj (dTopCat.of ↑X₂)) ↑C} (h_comm : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₁ = (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubsetHom ⋯)).comp F₂) (F' : CategoryTheory.Functor ↑(FundamentalCategory.fundamentalCategoryFunctor.obj X) ↑C) (h₁ : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₁)).comp F' = F₁) (h₂ : (FundamentalCategory.fundamentalCategoryMap (dTopCat.DirectedSubtypeHom X₂)).comp F' = F₂) : F' = Functor hX X₁_open X₂_open h_comm

theorem DirectedVanKampen.directed_van_kampen {X : dTopCat} {X₁ X₂ : Set ↑X} (X₁_open : IsOpen X₁) (X₂_open : IsOpen X₂) (hX : X₁ ∪ X₂ = Set.univ) : CategoryTheory.IsPushout (FundamentalCategory.fundamentalCategoryFunctor.map (dTopCat.DirectedSubsetHom ⋯)) (FundamentalCategory.fundamentalCategoryFunctor.map (dTopCat.DirectedSubsetHom ⋯)) (FundamentalCategory.fundamentalCategoryFunctor.map (dTopCat.DirectedSubtypeHom X₁)) (FundamentalCategory.fundamentalCategoryFunctor.map (dTopCat.DirectedSubtypeHom X₂))

The Van Kampen Theorem: the fundamental category functor dπ induces a pushout in the category of categories.