Loogle!
Result
Found 68 declarations mentioning CategoryTheory.Limits.pullback.diagonal.
- CategoryTheory.Limits.pullback.diagonal 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] : X ⟶ CategoryTheory.Limits.pullback.diagonalObj f - CategoryTheory.Limits.pullback.instIsSplitMonoDiagonal 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] : CategoryTheory.IsSplitMono (CategoryTheory.Limits.pullback.diagonal f) - CategoryTheory.Limits.pullback.instIsIsoDiagonalOfMono 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] [CategoryTheory.Mono f] : CategoryTheory.IsIso (CategoryTheory.Limits.pullback.diagonal f) - CategoryTheory.Limits.pullback.isIso_diagonal_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] : CategoryTheory.IsIso (CategoryTheory.Limits.pullback.diagonal f) ↔ CategoryTheory.Mono f - CategoryTheory.Limits.pullback.diagonal_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.fst f f) = CategoryTheory.CategoryStruct.id X - CategoryTheory.Limits.pullback.diagonal_snd 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.snd f f) = CategoryTheory.CategoryStruct.id X - CategoryTheory.Limits.pullback.diagonal_fst_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f f) h) = h - CategoryTheory.Limits.pullback.diagonal_snd_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f f) h) = h - CategoryTheory.Limits.pullbackDiagonalMapIdIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, 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_lift_diagonal_isPullback 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, 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.pushout.op_codiagonal 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPushout f f] : (CategoryTheory.Limits.pushout.codiagonal f).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f.op) (CategoryTheory.Limits.pullbackIsoOpPushout f.op f.op).hom - CategoryTheory.Limits.pullback_map_diagonal_isPullback 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.pullback.comp_diagonal 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, 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.pullbackDiagonalMapIdIso_hom_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.comp_diagonal_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, 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.diagonal_pullback_fst 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.pullback.fst f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f (CategoryTheory.Over.mk g).hom).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback f).map (CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.diagonal g) ⋯))) (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv) - CategoryTheory.Limits.pullback_fst_map_snd_isPullback 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, 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.pullback.diagonal_comp 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, 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.pullbackDiagonalMapIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Diagonal
{C : Type u_1} [CategoryTheory.Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.diagonal_iff 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y} : P.diagonal f ↔ P (CategoryTheory.Limits.pullback.diagonal f) - AlgebraicGeometry.diagonal_SpecMap 📋 Mathlib.AlgebraicGeometry.Pullbacks
(R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : CategoryTheory.Limits.pullback.diagonal (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)) (AlgebraicGeometry.pullbackSpecIso R S S).inv - AlgebraicGeometry.Scheme.Pullback.diagonalRestrictIsoDiagonal 📋 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.openCoverOfBase 𝒰 f f).I₀) (j : (𝒱 i).I₀) : CategoryTheory.Arrow.mk (CategoryTheory.Limits.pullback.diagonal f ∣_ AlgebraicGeometry.Scheme.Hom.opensRange ((AlgebraicGeometry.Scheme.Pullback.diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩)) ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.CategoryStruct.comp ((𝒱 i).f j) (CategoryTheory.Limits.pullback.snd f (𝒰.f i)))) - AlgebraicGeometry.QuasiSeparated.quasiCompact_diagonal 📋 Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
{X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.QuasiSeparated f] : AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.pullback.diagonal f) - AlgebraicGeometry.QuasiSeparated.mk 📋 Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
{X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (quasiCompact_diagonal : AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.pullback.diagonal f) := by infer_instance) : AlgebraicGeometry.QuasiSeparated f - AlgebraicGeometry.quasiSeparated_iff 📋 Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.QuasiSeparated f ↔ autoParam (AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.pullback.diagonal f)) AlgebraicGeometry.QuasiSeparated.quasiCompact_diagonal._autoParam - AlgebraicGeometry.IsAffineOpen.inf 📋 Mathlib.AlgebraicGeometry.Morphisms.Affine
{X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))] {U V : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (hV : AlgebraicGeometry.IsAffineOpen V) : AlgebraicGeometry.IsAffineOpen (U ⊓ V) - AlgebraicGeometry.IsAffineOpen.iInf 📋 Mathlib.AlgebraicGeometry.Morphisms.Affine
{X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))] {ι : Sort u_1} [Finite ι] [Nonempty ι] {U : ι → X.Opens} (hU : ∀ (i : ι), AlgebraicGeometry.IsAffineOpen (U i)) : AlgebraicGeometry.IsAffineOpen (⨅ i, U i) - AlgebraicGeometry.IsAffineOpen.biInf 📋 Mathlib.AlgebraicGeometry.Morphisms.Affine
{X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X))] {ι : Type u_1} (s : Set ι) (hs : s.Finite) (hs' : s.Nonempty) {U : ι → X.Opens} (hU : ∀ i ∈ s, AlgebraicGeometry.IsAffineOpen (U i)) : AlgebraicGeometry.IsAffineOpen (⨅ i ∈ s, U i) - AlgebraicGeometry.isAffineHom_diagonal_iff 📋 Mathlib.AlgebraicGeometry.Morphisms.Affine
{X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} : AlgebraicGeometry.IsAffineHom (CategoryTheory.Limits.pullback.diagonal f) ↔ ∀ (U : Y.Opens), AlgebraicGeometry.IsAffineOpen U → ∀ V₁ ≤ (TopologicalSpace.Opens.map f.base).obj U, ∀ V₂ ≤ (TopologicalSpace.Opens.map f.base).obj U, AlgebraicGeometry.IsAffineOpen V₁ → AlgebraicGeometry.IsAffineOpen V₂ → AlgebraicGeometry.IsAffineOpen (V₁ ⊓ V₂) - AlgebraicGeometry.IsSeparated.isClosedImmersion_diagonal 📋 Mathlib.AlgebraicGeometry.Morphisms.Separated
{X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsSeparated f] : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f) - AlgebraicGeometry.IsSeparated.mk 📋 Mathlib.AlgebraicGeometry.Morphisms.Separated
{X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (isClosedImmersion_diagonal : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f) := by infer_instance) : AlgebraicGeometry.IsSeparated f - AlgebraicGeometry.isSeparated_iff 📋 Mathlib.AlgebraicGeometry.Morphisms.Separated
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.IsSeparated f ↔ autoParam (AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)) AlgebraicGeometry.IsSeparated.isClosedImmersion_diagonal._autoParam - AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange 📋 Mathlib.AlgebraicGeometry.Morphisms.Separated
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : 𝒰.I₀) → (CategoryTheory.Limits.pullback f (𝒰.f i)).OpenCover) : Set.range ⇑(CategoryTheory.Limits.pullback.diagonal f) ⊆ ↑(AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f 𝒰 𝒱) - AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange 📋 Mathlib.AlgebraicGeometry.Morphisms.Separated
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : 𝒰.I₀) → (CategoryTheory.Limits.pullback f (𝒰.f i)).OpenCover) [∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)] [∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), AlgebraicGeometry.IsAffine ((𝒱 i).X j)] : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f ∣_ AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f 𝒰 𝒱) - AlgebraicGeometry.IsImmersion.instDiagonalScheme 📋 Mathlib.AlgebraicGeometry.Morphisms.Immersion
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.IsImmersion (CategoryTheory.Limits.pullback.diagonal f) - AlgebraicGeometry.UniversallyInjective.iff_diagonal 📋 Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.UniversallyInjective f ↔ AlgebraicGeometry.Surjective (CategoryTheory.Limits.pullback.diagonal f) - AlgebraicGeometry.tfae_universallyInjective 📋 Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : [AlgebraicGeometry.UniversallyInjective f, ∀ (K : Type u) [inst : Field K], Function.Injective fun g => CategoryTheory.CategoryStruct.comp g f, Function.Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable, AlgebraicGeometry.Surjective (CategoryTheory.Limits.pullback.diagonal f)].TFAE - AlgebraicGeometry.FormallyUnramified.instOfIsOpenImmersionDiagonalScheme 📋 Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.pullback.diagonal f)] : AlgebraicGeometry.FormallyUnramified f - AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal 📋 Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.FormallyUnramified f] [AlgebraicGeometry.LocallyOfFiniteType f] : AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.pullback.diagonal f) - AlgebraicGeometry.WeaklyEtale.flat_diagonal 📋 Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
{X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.WeaklyEtale f] : AlgebraicGeometry.Flat (CategoryTheory.Limits.pullback.diagonal f) - AlgebraicGeometry.WeaklyEtale.instDiagonalScheme 📋 Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.WeaklyEtale f] : AlgebraicGeometry.WeaklyEtale (CategoryTheory.Limits.pullback.diagonal f) - AlgebraicGeometry.WeaklyEtale.mk 📋 Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
{X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (flat : AlgebraicGeometry.Flat f := by infer_instance) (flat_diagonal : AlgebraicGeometry.Flat (CategoryTheory.Limits.pullback.diagonal f) := by infer_instance) : AlgebraicGeometry.WeaklyEtale f - AlgebraicGeometry.weaklyEtale_iff 📋 Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
{X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.WeaklyEtale f ↔ autoParam (AlgebraicGeometry.Flat f) AlgebraicGeometry.WeaklyEtale.flat._autoParam ∧ autoParam (AlgebraicGeometry.Flat (CategoryTheory.Limits.pullback.diagonal f)) AlgebraicGeometry.WeaklyEtale.flat_diagonal._autoParam
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from within the Lean4 VSCode language extension
using the Loogle command from the command palette. 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.You can filter for definitions vs theorems: Using
⊢ (_ : Type _)finds all definitions which provide data while⊢ (_ : Prop)finds all theorems (and definitions of proofs).
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. Please review the Lean FRO Terms of Use and Privacy Policy.
This is Loogle revision 9f11169 serving mathlib revision 69fae59