The diagonal object of a morphism. #
We provide various API and isomorphisms considering the diagonal object Δ_{Y/X} := pullback f f
of a morphism f : X ⟶ Y.
@[inline, reducible]
abbrev
CategoryTheory.Limits.pullback.diagonalObj
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasPullback f f]
:
C
The diagonal object of a morphism f : X ⟶ Y is Δ_{X/Y} := pullback f f.
Instances For
def
CategoryTheory.Limits.pullback.diagonal
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasPullback f f]
:
The diagonal morphism X ⟶ Δ_{X/Y} for a morphism f : X ⟶ Y.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.pullback.diagonal_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasPullback f f]
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = h
@[simp]
theorem
CategoryTheory.Limits.pullback.diagonal_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasPullback f f]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f) CategoryTheory.Limits.pullback.fst = CategoryTheory.CategoryStruct.id X
@[simp]
theorem
CategoryTheory.Limits.pullback.diagonal_snd_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasPullback f f]
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = h
@[simp]
theorem
CategoryTheory.Limits.pullback.diagonal_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasPullback f f]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f) CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.id X
instance
CategoryTheory.Limits.pullback.instIsSplitMonoDiagonalObjDiagonal
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasPullback f f]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.pullback.instIsSplitEpiPullbackFst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasPullback f f]
:
CategoryTheory.IsSplitEpi CategoryTheory.Limits.pullback.fst
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.pullback.instIsSplitEpiPullbackSnd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasPullback f f]
:
CategoryTheory.IsSplitEpi CategoryTheory.Limits.pullback.snd
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.pullback.instIsIsoDiagonalObjDiagonal
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasPullback f f]
[CategoryTheory.Mono f]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.pullback.diagonal_isKernelPair
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasPullback f f]
:
CategoryTheory.IsKernelPair f CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd
The two projections Δ_{X/Y} ⟶ X form a kernel pair for f : X ⟶ Y.
@[simp]
theorem
CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp i₁
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h))) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h
@[simp]
theorem
CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp i₁ CategoryTheory.Limits.pullback.fst)) = CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp i₂
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h))) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h
@[simp]
theorem
CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp i₂ CategoryTheory.Limits.pullback.fst)) = CategoryTheory.Limits.pullback.fst
def
CategoryTheory.Limits.pullbackDiagonalMapIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
[CategoryTheory.Limits.HasPullback i₁ i₂]
:
CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.diagonal f)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ CategoryTheory.Limits.pullback.snd)
(CategoryTheory.CategoryStruct.comp i₂ CategoryTheory.Limits.pullback.snd) f f
(CategoryTheory.CategoryStruct.comp i₁ CategoryTheory.Limits.pullback.fst)
(CategoryTheory.CategoryStruct.comp i₂ CategoryTheory.Limits.pullback.fst) i ⋯ ⋯) ≅ CategoryTheory.Limits.pullback i₁ i₂
This iso witnesses the fact that
given f : X ⟶ Y, i : U ⟶ Y, and i₁ : V₁ ⟶ X ×[Y] U, i₂ : V₂ ⟶ X ×[Y] U, the diagram
V₁ ×[X ×[Y] U] V₂ ⟶ V₁ ×[U] V₂ | | | | ↓ ↓ X ⟶ X ×[Y] X
is a pullback square.
Also see pullback_fst_map_snd_isPullback.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIso_hom_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
[CategoryTheory.Limits.HasPullback i₁ i₂]
{Z : C}
(h : V₁ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIso_hom_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
[CategoryTheory.Limits.HasPullback i₁ i₂]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom
CategoryTheory.Limits.pullback.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIso_hom_snd_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
[CategoryTheory.Limits.HasPullback i₁ i₂]
{Z : C}
(h : V₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIso_hom_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
[CategoryTheory.Limits.HasPullback i₁ i₂]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom
CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIso_inv_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
[CategoryTheory.Limits.HasPullback i₁ i₂]
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h))
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIso_inv_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
[CategoryTheory.Limits.HasPullback i₁ i₂]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv
CategoryTheory.Limits.pullback.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp i₁ CategoryTheory.Limits.pullback.fst)
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIso_inv_snd_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
[CategoryTheory.Limits.HasPullback i₁ i₂]
{Z : C}
(h : V₁ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIso_inv_snd_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
[CategoryTheory.Limits.HasPullback i₁ i₂]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) = CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIso_inv_snd_snd_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
[CategoryTheory.Limits.HasPullback i₁ i₂]
{Z : C}
(h : V₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIso_inv_snd_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
[CategoryTheory.Limits.HasPullback i₁ i₂]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) = CategoryTheory.Limits.pullback.snd
theorem
CategoryTheory.Limits.pullback_fst_map_snd_isPullback
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{U : C}
{V₁ : C}
{V₂ : C}
(f : X ⟶ Y)
(i : U ⟶ Y)
(i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i)
(i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i)
[CategoryTheory.Limits.HasPullback i₁ i₂]
:
CategoryTheory.IsPullback
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp i₁ CategoryTheory.Limits.pullback.fst))
(CategoryTheory.Limits.pullback.map i₁ i₂ (CategoryTheory.CategoryStruct.comp i₁ CategoryTheory.Limits.pullback.snd)
(CategoryTheory.CategoryStruct.comp i₂ CategoryTheory.Limits.pullback.snd) (CategoryTheory.CategoryStruct.id V₁)
(CategoryTheory.CategoryStruct.id V₂) CategoryTheory.Limits.pullback.snd ⋯ ⋯)
(CategoryTheory.Limits.pullback.diagonal f)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ CategoryTheory.Limits.pullback.snd)
(CategoryTheory.CategoryStruct.comp i₂ CategoryTheory.Limits.pullback.snd) f f
(CategoryTheory.CategoryStruct.comp i₁ CategoryTheory.Limits.pullback.fst)
(CategoryTheory.CategoryStruct.comp i₂ CategoryTheory.Limits.pullback.fst) i ⋯ ⋯)
def
CategoryTheory.Limits.pullbackDiagonalMapIdIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{S : C}
{T : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
[CategoryTheory.Limits.HasPullback i i]
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
:
This iso witnesses the fact that
given f : X ⟶ T, g : Y ⟶ T, and i : T ⟶ S, the diagram
X ×ₜ Y ⟶ X ×ₛ Y | | | | ↓ ↓ T ⟶ T ×ₛ T
is a pullback square.
Also see pullback_map_diagonal_isPullback.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{S : C}
{T : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
[CategoryTheory.Limits.HasPullback i i]
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{S : C}
{T : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
[CategoryTheory.Limits.HasPullback i i]
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom
CategoryTheory.Limits.pullback.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{S : C}
{T : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
[CategoryTheory.Limits.HasPullback i i]
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{S : C}
{T : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
[CategoryTheory.Limits.HasPullback i i]
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom
CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{S : C}
{T : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
[CategoryTheory.Limits.HasPullback i i]
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
{Z : C}
(h : T ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f h)
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{S : C}
{T : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
[CategoryTheory.Limits.HasPullback i i]
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv
CategoryTheory.Limits.pullback.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{S : C}
{T : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
[CategoryTheory.Limits.HasPullback i i]
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{S : C}
{T : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
[CategoryTheory.Limits.HasPullback i i]
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) = CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{S : C}
{T : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
[CategoryTheory.Limits.HasPullback i i]
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h
@[simp]
theorem
CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{S : C}
{T : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
[CategoryTheory.Limits.HasPullback i i]
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) = CategoryTheory.Limits.pullback.snd
theorem
CategoryTheory.Limits.pullback.diagonal_comp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
{Z : C}
[CategoryTheory.Limits.HasPullbacks C]
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f f]
[CategoryTheory.Limits.HasPullback g g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f g)]
:
CategoryTheory.Limits.pullback.diagonal (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f f g).inv
CategoryTheory.Limits.pullback.snd)
theorem
CategoryTheory.Limits.pullback_map_diagonal_isPullback
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
[CategoryTheory.Limits.HasPullbacks C]
{S : C}
{T : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
[CategoryTheory.Limits.HasPullback i i]
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)]
:
CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f)
(CategoryTheory.Limits.pullback.map f g (CategoryTheory.CategoryStruct.comp f i)
(CategoryTheory.CategoryStruct.comp g i) (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) i
⋯ ⋯)
(CategoryTheory.Limits.pullback.diagonal i)
(CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
def
CategoryTheory.Limits.diagonalObjPullbackFstIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
CategoryTheory.Limits.pullback.diagonalObj CategoryTheory.Limits.pullback.fst ≅ CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd g) f
The diagonal object of X ×[Z] Y ⟶ X is isomorphic to Δ_{Y/Z} ×[Z] X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom
CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) = CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) = CategoryTheory.Limits.pullback.snd
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
@[simp]
theorem
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd
theorem
CategoryTheory.Limits.diagonal_pullback_fst
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
CategoryTheory.Limits.pullback.diagonal CategoryTheory.Limits.pullback.fst = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f (CategoryTheory.Over.mk g).hom).hom
(CategoryTheory.CategoryStruct.comp
((CategoryTheory.Limits.baseChange f).map
(CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.diagonal g) ⋯)).left
(CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv)
@[simp]
theorem
CategoryTheory.Limits.pullbackFstFstIso_hom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{S : C}
{X' : C}
{Y' : C}
{S' : C}
(f : X ⟶ S)
(g : Y ⟶ S)
(f' : X' ⟶ S')
(g' : Y' ⟶ S')
(i₁ : X ⟶ X')
(i₂ : Y ⟶ Y')
(i₃ : S ⟶ S')
(e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
(e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
[CategoryTheory.Mono i₃]
:
(CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).hom = CategoryTheory.Limits.pullback.lift
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) ⋯
@[simp]
theorem
CategoryTheory.Limits.pullbackFstFstIso_inv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{S : C}
{X' : C}
{Y' : C}
{S' : C}
(f : X ⟶ S)
(g : Y ⟶ S)
(f' : X' ⟶ S')
(g' : Y' ⟶ S')
(i₁ : X ⟶ X')
(i₂ : Y ⟶ Y')
(i₃ : S ⟶ S')
(e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
(e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
[CategoryTheory.Mono i₃]
:
(CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv = CategoryTheory.Limits.pullback.lift
(CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
CategoryTheory.Limits.pullback.fst ⋯)
(CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
CategoryTheory.Limits.pullback.snd ⋯)
⋯
def
CategoryTheory.Limits.pullbackFstFstIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{S : C}
{X' : C}
{Y' : C}
{S' : C}
(f : X ⟶ S)
(g : Y ⟶ S)
(f' : X' ⟶ S')
(g' : Y' ⟶ S')
(i₁ : X ⟶ X')
(i₂ : Y ⟶ Y')
(i₃ : S ⟶ S')
(e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
(e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
[CategoryTheory.Mono i₃]
:
CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst ≅ CategoryTheory.Limits.pullback f g
Given the following diagram with S ⟶ S' a monomorphism,
X ⟶ X'
↘ ↘
S ⟶ S'
↗ ↗
Y ⟶ Y'
This iso witnesses the fact that
X ×[S] Y ⟶ (X' ×[S'] Y') ×[Y'] Y
| |
| |
↓ ↓
(X' ×[S'] Y') ×[X'] X ⟶ X' ×[S'] Y'
is a pullback square. The diagonal map of this square is pullback.map.
Also see pullback_lift_map_is_pullback.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{S : C}
{X' : C}
{Y' : C}
{S' : C}
(f : X ⟶ S)
(g : Y ⟶ S)
(f' : X' ⟶ S')
(g' : Y' ⟶ S')
(i₁ : X ⟶ X')
(i₂ : Y ⟶ Y')
(i₃ : S ⟶ S')
(e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
(e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
[CategoryTheory.Mono i₃]
:
CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst)
theorem
CategoryTheory.Limits.pullback_lift_map_isPullback
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasPullbacks C]
{X : C}
{Y : C}
{S : C}
{X' : C}
{Y' : C}
{S' : C}
(f : X ⟶ S)
(g : Y ⟶ S)
(f' : X' ⟶ S')
(g' : Y' ⟶ S')
(i₁ : X ⟶ X')
(i₂ : Y ⟶ Y')
(i₃ : S ⟶ S')
(e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
(e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
[CategoryTheory.Mono i₃]
:
CategoryTheory.IsPullback
(CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
CategoryTheory.Limits.pullback.fst ⋯)
(CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
CategoryTheory.Limits.pullback.snd ⋯)
CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst