Loogle!
Result
Found 79 declarations mentioning CategoryTheory.Limits.pullback.map.
- CategoryTheory.Limits.pullback.map 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S) [CategoryTheory.Limits.HasPullback f₁ f₂] (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) [CategoryTheory.Limits.HasPullback g₁ g₂] (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T) (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂) : CategoryTheory.Limits.pullback f₁ f₂ ⟶ CategoryTheory.Limits.pullback g₁ g₂ - CategoryTheory.Limits.pullback.congrHom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X ⟶ Z} {g₁ g₂ : Y ⟶ Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [CategoryTheory.Limits.HasPullback f₁ g₁] [CategoryTheory.Limits.HasPullback f₂ g₂] : (CategoryTheory.Limits.pullback.congrHom h₁ h₂).hom = CategoryTheory.Limits.pullback.map f₁ g₁ f₂ g₂ (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯ - CategoryTheory.Limits.pullback.map_isIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S) [CategoryTheory.Limits.HasPullback f₁ f₂] (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) [CategoryTheory.Limits.HasPullback g₁ g₂] (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T) (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂) [CategoryTheory.IsIso i₁] [CategoryTheory.IsIso i₂] [CategoryTheory.IsIso i₃] : CategoryTheory.IsIso (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) - CategoryTheory.Limits.pullback.map.congr_simp 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S) [CategoryTheory.Limits.HasPullback f₁ f₂] (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) [CategoryTheory.Limits.HasPullback g₁ g₂] (i₁ i₁✝ : W ⟶ Y) (e_i₁ : i₁ = i₁✝) (i₂ i₂✝ : X ⟶ Z) (e_i₂ : i₂ = i₂✝) (i₃ i₃✝ : S ⟶ T) (e_i₃ : i₃ = i₃✝) (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂) : CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ = CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁✝ i₂✝ i₃✝ ⋯ ⋯ - CategoryTheory.Limits.pullback.map_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [CategoryTheory.Limits.HasPullback f g] : CategoryTheory.Limits.pullback.map f g f g (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f g) - CategoryTheory.Limits.pullback.congrHom_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X ⟶ Z} {g₁ g₂ : Y ⟶ Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [CategoryTheory.Limits.HasPullback f₁ g₁] [CategoryTheory.Limits.HasPullback f₂ g₂] : (CategoryTheory.Limits.pullback.congrHom h₁ h₂).inv = CategoryTheory.Limits.pullback.map f₂ g₂ f₁ g₁ (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯ - CategoryTheory.Limits.pullback.map_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' X'' Y'' Z'' : C} {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} {f'' : X'' ⟶ Z''} {g'' : Y'' ⟶ Z''} (i₁ : X ⟶ X') (j₁ : X' ⟶ X'') (i₂ : Y ⟶ Y') (j₂ : Y' ⟶ Y'') (i₃ : Z ⟶ Z') (j₃ : Z' ⟶ Z'') [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' g'] [CategoryTheory.Limits.HasPullback f'' g''] (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g') (e₃ : CategoryTheory.CategoryStruct.comp f' j₃ = CategoryTheory.CategoryStruct.comp j₁ f'') (e₄ : CategoryTheory.CategoryStruct.comp g' j₃ = CategoryTheory.CategoryStruct.comp j₂ g'') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (CategoryTheory.Limits.pullback.map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄) = CategoryTheory.Limits.pullback.map f g f'' g'' (CategoryTheory.CategoryStruct.comp i₁ j₁) (CategoryTheory.CategoryStruct.comp i₂ j₂) (CategoryTheory.CategoryStruct.comp i₃ j₃) ⋯ ⋯ - CategoryTheory.Limits.pullback.map_comp_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' X'' Y'' Z'' : C} {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} {f'' : X'' ⟶ Z''} {g'' : Y'' ⟶ Z''} (i₁ : X ⟶ X') (j₁ : X' ⟶ X'') (i₂ : Y ⟶ Y') (j₂ : Y' ⟶ Y'') (i₃ : Z ⟶ Z') (j₃ : Z' ⟶ Z'') [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' g'] [CategoryTheory.Limits.HasPullback f'' g''] (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g') (e₃ : CategoryTheory.CategoryStruct.comp f' j₃ = CategoryTheory.CategoryStruct.comp j₁ f'') (e₄ : CategoryTheory.CategoryStruct.comp g' j₃ = CategoryTheory.CategoryStruct.comp j₂ g'') {Z✝ : C} (h : CategoryTheory.Limits.pullback f'' g'' ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map f g f'' g'' (CategoryTheory.CategoryStruct.comp i₁ j₁) (CategoryTheory.CategoryStruct.comp i₂ j₂) (CategoryTheory.CategoryStruct.comp i₃ j₃) ⋯ ⋯) h - CategoryTheory.IsKernelPair.pullback 📋 Mathlib.CategoryTheory.Limits.Shapes.KernelPair
{C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z A : C} {g : Y ⟶ Z} {a₁ a₂ : A ⟶ Y} (h : CategoryTheory.IsKernelPair g a₁ a₂) (f : X ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp a₁ g)] : CategoryTheory.IsKernelPair (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp a₁ g) f g (CategoryTheory.CategoryStruct.id X) a₁ (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯) (CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp a₁ g) f g (CategoryTheory.CategoryStruct.id X) a₂ (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯) - CategoryTheory.Limits.pullbackDiagonalMapIdIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S 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.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 - CategoryTheory.Limits.pullbackDiagonalMapIdIso.congr_simp 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S 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.Limits.pullbackDiagonalMapIdIso f g i = CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i - CategoryTheory.Limits.pullback_map_diagonal_isPullback 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S 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 g) 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) ⋯ ⋯) - CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S 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 - CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S 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) - CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S 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.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 - CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S 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.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 - CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S 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 - CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S 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 - CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S 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)) - CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S 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)) - CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S 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) - CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S 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) - CategoryTheory.Limits.pullback_lift_diagonal_isPullback 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S : C} (g : Y ⟶ X) (f : X ⟶ S) : CategoryTheory.IsPullback g (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id Y) g ⋯) (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp g f) f f f g (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) - CategoryTheory.Limits.pullback.comp_diagonal 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y Z : C} [CategoryTheory.Limits.HasPullbacks C] (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.pullback.diagonal g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f g) g g f f (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯) - CategoryTheory.Limits.pullback_lift_map_isPullback 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks 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₁ : 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 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) ⋯) (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.comp_diagonal_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y Z : C} [CategoryTheory.Limits.HasPullbacks C] (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : CategoryTheory.Limits.pullback.diagonalObj g ⟶ Z✝) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.CategoryStruct.comp f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f g) g g f f (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯) h) - CategoryTheory.Limits.pullbackFstFstIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks 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₁ : 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) ⋯) ⋯ - CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks 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₁ : 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 (CategoryTheory.Limits.pullback.fst f' g') i₁) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂)) - CategoryTheory.Limits.pullback.diagonal_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y Z : C} [CategoryTheory.Limits.HasPullbacks C] (f : X ⟶ Y) (g : Y ⟶ Z) : 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) ⋯ ⋯))) - CategoryTheory.Limits.pullback_fst_map_snd_isPullback 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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 i₁ i₂) (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))) (CategoryTheory.Limits.pullback.map i₁ i₂ (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.id V₁) (CategoryTheory.CategoryStruct.id V₂) (CategoryTheory.Limits.pullback.snd f i) ⋯ ⋯) (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.pullbackDiagonalMapIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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₂ - CategoryTheory.Limits.pullbackDiagonalMapIso.hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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₂ - CategoryTheory.Limits.pullbackDiagonalMapIso.inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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 ⋯ ⋯) - CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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.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.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst i₁ i₂) (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) - CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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 (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 ⋯ ⋯)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst i₁ i₂) (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f i) h)) - CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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.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.fst (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))) = CategoryTheory.Limits.pullback.fst i₁ i₂ - CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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.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.snd (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))) = CategoryTheory.Limits.pullback.snd i₁ i₂ - CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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.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.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))) = CategoryTheory.Limits.pullback.fst (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_diagonal_map_snd_snd_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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.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.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i))) = CategoryTheory.Limits.pullback.fst (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.pullbackDiagonalMapIso.inv_snd_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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.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.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst i₁ i₂) h - CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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.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.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd i₁ i₂) h - CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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 i₁ i₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (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.fst (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) - CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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 i₁ i₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (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.snd (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) - CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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.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.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f i) h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (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 ⋯ ⋯)) h - CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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.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.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f i) h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (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 ⋯ ⋯)) h - CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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 i₁ i₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (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.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) h) - CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ 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 i₁ i₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (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.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) h) - CategoryTheory.MorphismProperty.pullback_map 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [CategoryTheory.Limits.HasPullbacks C] [P.IsStableUnderBaseChange] [P.IsStableUnderComposition] {S X X' Y Y' : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : X' ⟶ S} {g' : Y' ⟶ S} {i₁ : X ⟶ X'} {i₂ : Y ⟶ Y'} (h₁ : P i₁) (h₂ : P i₂) (e₁ : f = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : g = CategoryTheory.CategoryStruct.comp i₂ g') : P (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) - CategoryTheory.ShortComplex.SnakeInput.functorP_map 📋 Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {X✝ Y✝ : CategoryTheory.ShortComplex.SnakeInput C} (f : X✝ ⟶ Y✝) : CategoryTheory.ShortComplex.SnakeInput.functorP.map f = CategoryTheory.Limits.pullback.map X✝.L₁.g X✝.v₀₁.τ₃ Y✝.L₁.g Y✝.v₀₁.τ₃ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ ⋯ ⋯ - TopCat.pullback_map_isEmbedding 📋 Mathlib.Topology.Category.TopCat.Limits.Pullbacks
{W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z} (H₁ : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₁)) (H₂ : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₂)) (i₃ : S ⟶ T) (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) - TopCat.pullback_map_isOpenEmbedding 📋 Mathlib.Topology.Category.TopCat.Limits.Pullbacks
{W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z} (H₁ : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₁)) (H₂ : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₂)) (i₃ : S ⟶ T) [H₃ : CategoryTheory.Mono i₃] (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) - TopCat.range_pullback_map 📋 Mathlib.Topology.Category.TopCat.Limits.Pullbacks
{W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T) [H₃ : CategoryTheory.Mono i₃] (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) = ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst g₁ g₂)) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom i₁) ∩ ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd g₁ g₂)) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom i₂) - CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_map 📋 Mathlib.CategoryTheory.Extensive
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.FinitaryPreExtensive C] {ι : Type u_1} {ι' : Type u_2} [Finite ι] [Finite ι'] {S : C} {X : ι → C} {Y : ι' → C} (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S) : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc fun p => CategoryTheory.Limits.pullback.map (f p.1) (g p.2) (CategoryTheory.Limits.Sigma.desc f) (CategoryTheory.Limits.Sigma.desc g) (CategoryTheory.Limits.Sigma.ι X p.1) (CategoryTheory.Limits.Sigma.ι Y p.2) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) - CategoryTheory.PreOneHypercover.inter_p₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] (i j : (E.inter F.toPreZeroHypercover).I₀) (k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2) : (E.inter F).p₁ k = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (E.p₁ k.1) (E.f i.1)) (CategoryTheory.CategoryStruct.comp (F.p₁ k.2) (F.f i.2)) (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).fst) (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).snd) (E.p₁ k.1) (F.p₁ k.2) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯ - CategoryTheory.PreOneHypercover.inter_p₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] (i j : (E.inter F.toPreZeroHypercover).I₀) (k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2) : (E.inter F).p₂ k = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (E.p₁ k.1) (E.f i.1)) (CategoryTheory.CategoryStruct.comp (F.p₁ k.2) (F.f i.2)) (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).fst) (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).snd) (E.p₂ k.1) (F.p₂ k.2) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯ - AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso.eq_1 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀) : AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i = CategoryTheory.Limits.pullbackSymmetry f (𝒰.affineRefinement.openCover.f i) ≪≫ (CategoryTheory.Limits.pullbackRightPullbackFstIso (𝒰.f i.fst) f (((fun i => ((fun j => (𝒰.X j).affineCover) i).toPreZeroHypercover) i.fst).f i.snd)).symm ≪≫ CategoryTheory.Limits.pullbackSymmetry (((fun i => ((fun j => (𝒰.X j).affineCover) i).toPreZeroHypercover) i.fst).f i.snd) (CategoryTheory.Limits.pullback.fst (𝒰.f i.fst) f) ≪≫ CategoryTheory.asIso (CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.fst (𝒰.f i.fst) f) (((fun i => ((fun j => (𝒰.X j).affineCover) i).toPreZeroHypercover) i.fst).f i.snd) (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst) ((𝒰.X i.fst).affineCover.f i.snd) (CategoryTheory.Limits.pullbackSymmetry (𝒰.f i.fst) f).hom (CategoryTheory.CategoryStruct.id (𝒰.affineRefinement.openCover.X i)) (CategoryTheory.CategoryStruct.id (𝒰.X i.fst)) ⋯ ⋯) - CategoryTheory.Over.whiskerLeft_left 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {R S T : CategoryTheory.Over X} (f : S ⟶ T) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f).left = CategoryTheory.Limits.pullback.map R.hom S.hom R.hom T.hom (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj R.left)) f.left (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.fromPUnit X).obj R.right)) ⋯ ⋯ - CategoryTheory.Over.whiskerRight_left 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {R S T : CategoryTheory.Over X} (f : S ⟶ T) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R).left = CategoryTheory.Limits.pullback.map S.hom R.hom T.hom R.hom f.left (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj R.left)) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.fromPUnit X).obj S.right)) ⋯ ⋯ - CategoryTheory.Over.tensorHom_left 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Over
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {R S T U : CategoryTheory.Over X} (f : R ⟶ S) (g : T ⟶ U) : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).left = CategoryTheory.Limits.pullback.map R.hom T.hom S.hom U.hom f.left g.left (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.fromPUnit X).obj R.right)) ⋯ ⋯ - AlgebraicGeometry.Scheme.pullback_map_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y S X' Y' S' : AlgebraicGeometry.Scheme} (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') [AlgebraicGeometry.IsOpenImmersion i₁] [AlgebraicGeometry.IsOpenImmersion i₂] [CategoryTheory.Mono i₃] : AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) - AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_f 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft 𝒰 f g).f i = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g f g (𝒰.f i) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯ - AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_f 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfRight 𝒰 f g).f i = CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp (𝒰.f i) g) f g (CategoryTheory.CategoryStruct.id X) (𝒰.f i) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯ - AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_f 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f g).f i = CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.snd f (𝒰.f i)) (CategoryTheory.Limits.pullback.snd g (𝒰.f i)) f g (CategoryTheory.Limits.pullback.fst f (𝒰.f i)) (CategoryTheory.Limits.pullback.fst g (𝒰.f i)) (𝒰.f i) ⋯ ⋯ - AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_f 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (ij : 𝒰X.I₀ × 𝒰Y.I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight 𝒰X 𝒰Y f g).f ij = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (𝒰X.f ij.1) f) (CategoryTheory.CategoryStruct.comp (𝒰Y.f ij.2) g) f g (𝒰X.f ij.1) (𝒰Y.f ij.2) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯ - AlgebraicGeometry.Scheme.Pullback.gluedLift.eq_1 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) : AlgebraicGeometry.Scheme.Pullback.gluedLift 𝒰 f g s = AlgebraicGeometry.Scheme.Cover.glueMorphisms (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) (fun i => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.f i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (𝒰.f i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g (CategoryTheory.CategoryStruct.id (𝒰.X i)) s.snd f ⋯ ⋯) ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι i))) ⋯ - AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap.eq_1 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.I₀) : AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap 𝒰 f g s i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso s.fst (𝒰.f j) ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)).hom (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) s.fst) (𝒰.f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i)) (𝒰.f j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.f i)).hom (CategoryTheory.Limits.pullback.map (𝒰.f i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g (CategoryTheory.CategoryStruct.id (𝒰.X i)) s.snd f ⋯ ⋯)) (CategoryTheory.CategoryStruct.id (𝒰.X j)) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯) - AlgebraicGeometry.Scheme.Pullback.t.eq_1 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i j : 𝒰.I₀) : AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i)) (𝒰.f j)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc (𝒰.f j) (𝒰.f i) (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f j) (𝒰.f i)) (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) g (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (CategoryTheory.CategoryStruct.comp (𝒰.f j) f)) g (CategoryTheory.Limits.pullbackSymmetry (𝒰.f j) (𝒰.f i)).hom (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc (𝒰.f i) (𝒰.f j) (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g).hom (CategoryTheory.Limits.pullbackSymmetry (𝒰.f i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))).hom))) - AlgebraicGeometry.Scheme.Pullback.t'.eq_1 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i j k : 𝒰.I₀) : AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i)) (𝒰.f k) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))) (𝒰.f k) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))) (𝒰.f k) (AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j) (CategoryTheory.CategoryStruct.id (𝒰.X k)) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯) (CategoryTheory.Limits.pullbackRightPullbackFstIso (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j)) (𝒰.f k) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i)).inv) (CategoryTheory.Limits.pullbackSymmetry (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)).hom) - AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap 𝒰 f g s i j) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i)) (𝒰.f j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.f i)).hom (CategoryTheory.Limits.pullback.map (𝒰.f i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g (CategoryTheory.CategoryStruct.id (𝒰.X i)) s.snd f ⋯ ⋯)) - AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.I₀) {Z✝ : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap 𝒰 f g s i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i)) (𝒰.f j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.f i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (𝒰.f i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g (CategoryTheory.CategoryStruct.id (𝒰.X i)) s.snd f ⋯ ⋯) h)) - AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (ij : (i : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).I₀) × ((fun i => ((fun i => AlgebraicGeometry.Scheme.coverOfIsIso (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.f i)) (CategoryTheory.Limits.pullback.snd g (𝒰.f i))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (𝒰.f i)) (𝒰.f i)) g (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.f i))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)))) i).toPreZeroHypercover) i).I₀) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase' 𝒰 f g).f ij = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.f ij.fst)) (CategoryTheory.Limits.pullback.snd g (𝒰.f ij.fst))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (𝒰.f ij.fst)) (𝒰.f ij.fst)) g (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.f ij.fst)) f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.f ij.fst))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.f ij.fst)) f) g f g (CategoryTheory.Limits.pullback.fst f (𝒰.f ij.fst)) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯))) - AlgebraicGeometry.Scheme.Pullback.diagonalCover_map 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover) (I : (AlgebraicGeometry.Scheme.Pullback.diagonalCover f 𝒰 𝒱).I₀) : (AlgebraicGeometry.Scheme.Pullback.diagonalCover f 𝒰 𝒱).f I = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.1) (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f I.fst)) (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.2) (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f I.fst)) f f (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.1) (CategoryTheory.Limits.pullback.fst f (𝒰.f I.fst))) (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.2) (CategoryTheory.Limits.pullback.fst f (𝒰.f I.fst))) (𝒰.f I.fst) ⋯ ⋯ - AlgebraicGeometry.Scheme.Pullback.range_map 📋 Mathlib.AlgebraicGeometry.PullbackCarrier
{X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) {X' Y' S' : AlgebraicGeometry.Scheme} (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₃] : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂).base) = ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f' g').base) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom i₁.base) ∩ ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f' g').base) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom i₂.base) - CategoryTheory.PreOneHypercover.cylinder_Y 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) {p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)) : (CategoryTheory.PreOneHypercover.cylinder f g).Y k = CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g p.snd) (CategoryTheory.PreOneHypercover.cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) - CategoryTheory.PreOneHypercover.toPullback_cylinder 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) {i j : (CategoryTheory.PreOneHypercover.cylinder f g).I₀} (k : (CategoryTheory.PreOneHypercover.cylinder f g).I₁ i j) : (CategoryTheory.PreOneHypercover.cylinder f g).toPullback k = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g i.snd) (CategoryTheory.PreOneHypercover.cylinderf f g j.snd) (E.f i.fst) (E.f j.fst) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) - CategoryTheory.PreOneHypercover.cylinderHom_h₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) {p q : (CategoryTheory.PreOneHypercover.cylinder f g).I₀} (k : (CategoryTheory.PreOneHypercover.cylinder f g).I₁ p q) : (CategoryTheory.PreOneHypercover.cylinderHom f g).h₁ k = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g p.snd) (CategoryTheory.PreOneHypercover.cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) - CategoryTheory.PreOneHypercover.cylinder_p₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) {p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)) : (CategoryTheory.PreOneHypercover.cylinder f g).p₁ k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g p.snd) (CategoryTheory.PreOneHypercover.cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.PreOneHypercover.cylinderf f g p.snd) (CategoryTheory.PreOneHypercover.cylinderf f g q.snd)) - CategoryTheory.PreOneHypercover.cylinder_p₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) {p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)) : (CategoryTheory.PreOneHypercover.cylinder f g).p₂ k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g p.snd) (CategoryTheory.PreOneHypercover.cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.PreOneHypercover.cylinderf f g p.snd) (CategoryTheory.PreOneHypercover.cylinderf f g q.snd)) - CategoryTheory.PreOneHypercover.sieve₁'_cylinder 📋 Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
{C : Type u} [CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S} {F : CategoryTheory.PreOneHypercover S} [CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F) (i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) : (CategoryTheory.PreOneHypercover.cylinder f g).sieve₁' i j = CategoryTheory.Sieve.pullback (CategoryTheory.Limits.pullback.map ((CategoryTheory.PreOneHypercover.cylinder f g).f i) ((CategoryTheory.PreOneHypercover.cylinder f g).f j) (E.f i.fst) (E.f j.fst) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (E.sieve₁' i.fst j.fst)
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try the
#loogle command from LeanSearchClient,
the CLI version, the Loogle
VS Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?aIf the pattern has parameters, they are matched in any order. Both of these will find
List.map:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?bBy main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→and∀) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin
and tsum, have "two" as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _ (if
there were any such lemmas). Metavariables (?a) are
assigned independently in each filter.
The #lucky button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.
This is Loogle revision ee8c038 serving mathlib revision 7a9e177