Loogle!
Result
Found 70 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_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.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_embedding_of_embeddings 📋 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_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.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.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_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 📋 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.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.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.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.MorphismProperty.IsStableUnderBaseChange.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) ⋯ ⋯) - AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso.eq_1 📋 Mathlib.AlgebraicGeometry.Cover.Open
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (i : (AlgebraicGeometry.Scheme.Cover.pullbackCover 𝒰.affineRefinement.openCover f).J) : AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i = CategoryTheory.Limits.pullbackSymmetry f (𝒰.affineRefinement.openCover.map i) ≪≫ (CategoryTheory.Limits.pullbackRightPullbackFstIso (𝒰.map i.fst) f (((fun j => (𝒰.obj j).affineCover) i.fst).map i.snd)).symm ≪≫ CategoryTheory.Limits.pullbackSymmetry (((fun j => (𝒰.obj j).affineCover) i.fst).map i.snd) (CategoryTheory.Limits.pullback.fst (𝒰.map i.fst) f) ≪≫ CategoryTheory.asIso (CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.fst (𝒰.map i.fst) f) (((fun j => (𝒰.obj j).affineCover) i.fst).map i.snd) (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst) ((𝒰.obj i.fst).affineCover.map i.snd) (CategoryTheory.Limits.pullbackSymmetry (𝒰.map i.fst) f).hom (CategoryTheory.CategoryStruct.id (𝒰.affineRefinement.openCover.obj i)) (CategoryTheory.CategoryStruct.id (𝒰.obj i.fst)) ⋯ ⋯) - CategoryTheory.Over.whiskerLeft_left 📋 Mathlib.CategoryTheory.ChosenFiniteProducts.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.ChosenFiniteProducts.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.ChosenFiniteProducts.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.openCoverOfLeft_map 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.J) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft 𝒰 f g).map i = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g f g (𝒰.map i) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯ - AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_map 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.J) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfRight 𝒰 f g).map i = CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp (𝒰.map i) g) f g (CategoryTheory.CategoryStruct.id X) (𝒰.map i) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯ - 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.openCoverOfBase_map 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.J) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f g).map i = CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) f g (CategoryTheory.Limits.pullback.fst f (𝒰.map i)) (CategoryTheory.Limits.pullback.fst g (𝒰.map i)) (𝒰.map i) ⋯ ⋯ - AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_map 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (ij : 𝒰X.J × 𝒰Y.J) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight 𝒰X 𝒰Y f g).map ij = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (𝒰X.map ij.1) f) (CategoryTheory.CategoryStruct.comp (𝒰Y.map ij.2) g) f g (𝒰X.map ij.1) (𝒰Y.map 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 : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) : AlgebraicGeometry.Scheme.Pullback.gluedLift 𝒰 f g s = (AlgebraicGeometry.Scheme.Cover.pullbackCover 𝒰 s.fst).glueMorphisms (fun i => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.map i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (𝒰.map i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g (CategoryTheory.CategoryStruct.id (𝒰.obj 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 : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.J) : AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap 𝒰 f g s i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso s.fst (𝒰.map j) ((AlgebraicGeometry.Scheme.Cover.pullbackCover 𝒰 s.fst).map i)).hom (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Cover.pullbackCover 𝒰 s.fst).map i) s.fst) (𝒰.map j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.map i)).hom (CategoryTheory.Limits.pullback.map (𝒰.map i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g (CategoryTheory.CategoryStruct.id (𝒰.obj i)) s.snd f ⋯ ⋯)) (CategoryTheory.CategoryStruct.id (𝒰.obj 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 : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) : AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc (𝒰.map j) (𝒰.map i) (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.map j) (𝒰.map i)) (CategoryTheory.CategoryStruct.comp (𝒰.map i) f)) g (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.map i) (𝒰.map j)) (CategoryTheory.CategoryStruct.comp (𝒰.map j) f)) g (CategoryTheory.Limits.pullbackSymmetry (𝒰.map j) (𝒰.map i)).hom (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc (𝒰.map i) (𝒰.map j) (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g).hom (CategoryTheory.Limits.pullbackSymmetry (𝒰.map i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map 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 : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : 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 (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map 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 (𝒰.map i) f) g) (𝒰.map i))) (𝒰.map k) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j))) (𝒰.map k) (AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j) (CategoryTheory.CategoryStruct.id (𝒰.obj k)) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯) (CategoryTheory.Limits.pullbackRightPullbackFstIso (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map 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 : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.J) : 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 (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst ((AlgebraicGeometry.Scheme.Cover.pullbackCover 𝒰 s.fst).map i) ((AlgebraicGeometry.Scheme.Cover.pullbackCover 𝒰 s.fst).map j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.map i)).hom (CategoryTheory.Limits.pullback.map (𝒰.map i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g (CategoryTheory.CategoryStruct.id (𝒰.obj 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 : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.J) {Z✝ : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.map 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 (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst ((AlgebraicGeometry.Scheme.Cover.pullbackCover 𝒰 s.fst).map i) ((AlgebraicGeometry.Scheme.Cover.pullbackCover 𝒰 s.fst).map j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.map i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (𝒰.map i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g (CategoryTheory.CategoryStruct.id (𝒰.obj i)) s.snd f ⋯ ⋯) h)) - AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_map 📋 Mathlib.AlgebraicGeometry.Pullbacks
{X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (x : (i : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft (AlgebraicGeometry.Scheme.Cover.pullbackCover 𝒰 f) f g).J) × ((fun i => AlgebraicGeometry.Scheme.coverOfIsIso (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (CategoryTheory.Limits.pullback.snd g (𝒰.map 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 (𝒰.map i)) (𝒰.map i)) g (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Cover.pullbackCover 𝒰 f).map i) f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.map i))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)))) i).J) : (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase' 𝒰 f g).map x = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd g (𝒰.map x.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 (𝒰.map x.fst)) (𝒰.map x.fst)) g (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.map x.fst)) f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.map x.fst))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.map x.fst)) f) g f g (CategoryTheory.Limits.pullback.fst f (𝒰.map x.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 : (AlgebraicGeometry.Scheme.Cover.pullbackCover 𝒰 f).J) → ((AlgebraicGeometry.Scheme.Cover.pullbackCover 𝒰 f).obj i).OpenCover) (I : (AlgebraicGeometry.Scheme.Pullback.diagonalCover f 𝒰 𝒱).J) : (AlgebraicGeometry.Scheme.Pullback.diagonalCover f 𝒰 𝒱).map I = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).map I.snd.1) (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f I.fst)) (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).map I.snd.2) (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f I.fst)) f f (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).map I.snd.1) (CategoryTheory.Limits.pullback.fst f (𝒰.map I.fst))) (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).map I.snd.2) (CategoryTheory.Limits.pullback.fst f (𝒰.map I.fst))) (𝒰.map 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)
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 19971e9 serving mathlib revision 40fea08