def
CategoryTheory.UvPoly.compDomEquiv
{𝒞 : Type u_1}
[Category.{u_2, u_1} 𝒞]
[Limits.HasTerminal 𝒞]
[Limits.HasPullbacks 𝒞]
{Γ E B D A : 𝒞}
{P : UvPoly E B}
{Q : UvPoly D A}
:
(Γ ⟶ P.compDom Q) ≃ (AB : Γ ⟶ P.functor.obj A) ×
(α : Γ ⟶ E) ×
(β : Γ ⟶ D) ×'
(w : CategoryStruct.comp AB (P.fstProj A) = CategoryStruct.comp α P.p) ×'
CategoryStruct.comp β Q.p = CategoryStruct.comp (Limits.pullback.lift AB α w) (PartialProduct.fan P A).snd
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.UvPoly.compDomEquiv_symm_comp_p
{𝒞 : Type u_1}
[Category.{u_2, u_1} 𝒞]
[Limits.HasTerminal 𝒞]
[Limits.HasPullbacks 𝒞]
{Γ E B D A : 𝒞}
{P : UvPoly E B}
{Q : UvPoly D A}
(AB : Γ ⟶ P.functor.obj A)
(α : Γ ⟶ E)
(β : Γ ⟶ D)
(w : CategoryStruct.comp AB (P.fstProj A) = CategoryStruct.comp α P.p)
(h : CategoryStruct.comp β Q.p = CategoryStruct.comp (Limits.pullback.lift AB α w) (PartialProduct.fan P A).snd)
: