mathlib documentation

category_theory.limits.shapes.diagonal

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.

@[reducible]
noncomputable def category_theory.limits.pullback.diagonal_obj {C : Type u_1} [category_theory.category C] {X Y : C} (f : X Y) [category_theory.limits.has_pullback f f] :
C

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

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_is_pullback.

Equations

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_is_pullback.

Equations
@[simp]
theorem category_theory.limits.pullback_fst_fst_iso_inv {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y S X' Y' S' : C} (f : X S) (g : Y S) (f' : X' S') (g' : Y' S') (i₁ : X X') (i₂ : Y Y') (i₃ : S S') (e₁ : f i₃ = i₁ f') (e₂ : g i₃ = i₂ g') [category_theory.mono i₃] :
noncomputable def category_theory.limits.pullback_fst_fst_iso {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y S X' Y' S' : C} (f : X S) (g : Y S) (f' : X' S') (g' : Y' S') (i₁ : X X') (i₂ : Y Y') (i₃ : S S') (e₁ : f i₃ = i₁ f') (e₂ : g i₃ = i₂ g') [category_theory.mono i₃] :

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
@[simp]
theorem category_theory.limits.pullback_fst_fst_iso_hom {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y S X' Y' S' : C} (f : X S) (g : Y S) (f' : X' S') (g' : Y' S') (i₁ : X X') (i₂ : Y Y') (i₃ : S S') (e₁ : f i₃ = i₁ f') (e₂ : g i₃ = i₂ g') [category_theory.mono i₃] :
theorem category_theory.limits.pullback_map_eq_pullback_fst_fst_iso_inv {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y S X' Y' S' : C} (f : X S) (g : Y S) (f' : X' S') (g' : Y' S') (i₁ : X X') (i₂ : Y Y') (i₃ : S S') (e₁ : f i₃ = i₁ f') (e₂ : g i₃ = i₂ g') [category_theory.mono i₃] :