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.

source

@[reducible, inline]

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] :

The diagonal object of a morphism f : X ⟶ Y is Δ_{X/Y} := pullback f f.

Equations

CategoryTheory.Limits.pullback.diagonalObj f = CategoryTheory.Limits.pullback f f

Instances For

source

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] :

X ⟶ CategoryTheory.Limits.pullback.diagonalObj f

The diagonal morphism X ⟶ Δ_{X/Y} for a morphism f : X ⟶ Y.

Equations

CategoryTheory.Limits.pullback.diagonal f = CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X) ⋯

Instances For

source

@[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 f f) = CategoryTheory.CategoryStruct.id X

source

@[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 f f) h) = h

source

@[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 f f) = CategoryTheory.CategoryStruct.id X

source

@[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 f f) h) = h

source

instance CategoryTheory.Limits.pullback.instIsSplitMonoDiagonal {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] :

CategoryTheory.IsSplitMono (CategoryTheory.Limits.pullback.diagonal f)

Equations

⋯ = ⋯

source

instance CategoryTheory.Limits.pullback.instIsSplitEpiFst {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 f f)

Equations

⋯ = ⋯

source

instance CategoryTheory.Limits.pullback.instIsSplitEpiSnd {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 f f)

Equations

⋯ = ⋯

source

instance CategoryTheory.Limits.pullback.instIsIsoDiagonalOfMono {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] :

CategoryTheory.IsIso (CategoryTheory.Limits.pullback.diagonal f)

Equations

⋯ = ⋯

source

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 f f) (CategoryTheory.Limits.pullback.snd f f)

The two projections Δ_{X/Y} ⟶ X form a kernel pair for f : X ⟶ Y.

source

@[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) :

source

@[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) :

source

@[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) :

source

@[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) :

source

@[reducible, inline]

abbrev CategoryTheory.Limits.pullbackDiagonalMapIso.hom {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 f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯) ⟶ CategoryTheory.Limits.pullback i₁ i₂

The underlying map of pullbackDiagonalIso

Equations

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

Instances For

source

@[reducible, inline]

abbrev CategoryTheory.Limits.pullbackDiagonalMapIso.inv {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 i₁ i₂ ⟶ CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)

The underlying inverse of pullbackDiagonalIso

Equations

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

Instances For

source

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₂] :

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

source

@[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₂] :

source

@[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) :

source

@[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₂] :

source

@[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) :

source

@[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₂] :

source

@[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) :

source

@[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₂] :

source

@[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) :

source

@[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₂] :

source

@[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) :

source

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₂] :

source

CategoryTheory.Limits.pullback (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.Limits.pullback f g

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

source

@[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 f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (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.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i))

source

@[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 f g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (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.pullback.fst (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)) h)

source

@[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 f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (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.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i))

source

@[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 f g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (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.pullback.snd (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)) h)

source

@[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.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.pullback.fst f g) f

source

@[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 (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) ⋯ ⋯)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.CategoryStruct.comp f h)

source

@[simp]

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (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.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i))) = CategoryTheory.Limits.pullback.fst f g

source

@[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.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.pullback.fst (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h

source

@[simp]

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (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.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i))) = CategoryTheory.Limits.pullback.snd f g

source

@[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.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.pullback.snd (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h

source

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 (CategoryTheory.Limits.pullback.diagonal g) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f g) g g f f (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)))

source

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) ⋯ ⋯)] :

source

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 f g) ≅ CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) 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

source

@[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.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) (CategoryTheory.Limits.pullback.fst g g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.snd f g)

source

@[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) :

source

@[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.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) (CategoryTheory.Limits.pullback.snd g g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.snd f g)

source

@[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) :

source

@[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.snd g g) g) f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.fst f g)

source

@[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 (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h)

source

@[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 f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.fst f g)) = CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f

source

@[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.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) h

source

@[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.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.snd f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) (CategoryTheory.Limits.pullback.fst g g)

source

@[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) :

source

@[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 f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.fst f g)) = CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f

source

@[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.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) h

source

@[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.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.snd f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) (CategoryTheory.Limits.pullback.snd g g)

source

@[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) :

source

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 f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f (CategoryTheory.Over.mk g).hom).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback f).map (CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.diagonal g) ⋯)).left (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv)

source

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 f' g') i₁) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂) ≅ 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

source

@[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₃] :

source

@[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 f g) ⋯) (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (CategoryTheory.Limits.pullback.snd f g) ⋯) ⋯

source

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₃] :

source

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₃] :

Documentation

Mathlib.CategoryTheory.Limits.Shapes.Diagonal

The diagonal object of a morphism. #