Loogle!

Result

Found 75 declarations mentioning CategoryTheory.MorphismProperty.Under.

CategoryTheory.MorphismProperty.Under 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) (X : T) : Type (max v_1 u_1)
CategoryTheory.MorphismProperty.Under.mk 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) {X A : T} (f : X ⟶ A) (hf : P f) : P.Under Q X
CategoryTheory.MorphismProperty.Under.forget 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) (X : T) [Q.IsMultiplicative] : CategoryTheory.Functor (P.Under Q X) (CategoryTheory.Under X)
CategoryTheory.MorphismProperty.instFaithfulUnderUnderForget 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) (X : T) [Q.IsMultiplicative] : (CategoryTheory.MorphismProperty.Under.forget P Q X).Faithful
CategoryTheory.MorphismProperty.instFullUnderTopUnderForget 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) : (CategoryTheory.MorphismProperty.Under.forget P ⊤ X).Full
CategoryTheory.MorphismProperty.Under.Hom.mk 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : (CategoryTheory.MorphismProperty.Under.forget P Q X).obj A ⟶ (CategoryTheory.MorphismProperty.Under.forget P Q X).obj B) (hf : Q (CategoryTheory.Under.Hom.right f)) : A ⟶ B
CategoryTheory.MorphismProperty.Under.forget_comp_forget_map 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) (X : T) [Q.IsMultiplicative] {A B : P.Under Q X} (f : A ⟶ B) : ((CategoryTheory.MorphismProperty.Under.forget P Q X).comp (CategoryTheory.Under.forget X)).map f = f.right
CategoryTheory.MorphismProperty.Under.Hom.ext 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} {f g : A ⟶ B} (h : f.right = g.right) : f = g
CategoryTheory.MorphismProperty.Under.Hom.ext_iff 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} {f g : A ⟶ B} : f = g ↔ f.right = g.right
CategoryTheory.MorphismProperty.Under.Hom.mk_hom 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : (CategoryTheory.MorphismProperty.Under.forget P Q X).obj A ⟶ (CategoryTheory.MorphismProperty.Under.forget P Q X).obj B) (hf : Q (CategoryTheory.Under.Hom.right f)) : CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Under.Hom.mk f hf) = f
CategoryTheory.MorphismProperty.Under.w 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp A.hom f.right = B.hom
CategoryTheory.MorphismProperty.Under.isoMk 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] [Q.RespectsIso] {A B : P.Under Q X} (f : A.right ≅ B.right) (w : CategoryTheory.CategoryStruct.comp A.hom f.hom = B.hom := by cat_disch) : A ≅ B
CategoryTheory.MorphismProperty.Under.homMk 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : A.right ⟶ B.right) (w : CategoryTheory.CategoryStruct.comp A.hom f = B.hom := by cat_disch) (hf : Q f := by trivial) : A ⟶ B
CategoryTheory.MorphismProperty.Under.w_assoc 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : A ⟶ B) {Z : T} (h : B.right ⟶ Z) : CategoryTheory.CategoryStruct.comp A.hom (CategoryTheory.CategoryStruct.comp f.right h) = CategoryTheory.CategoryStruct.comp B.hom h
CategoryTheory.MorphismProperty.Under.homMk_hom 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] {A B : P.Under Q X} (f : A.right ⟶ B.right) (w : CategoryTheory.CategoryStruct.comp A.hom f = B.hom := by cat_disch) (hf : Q f := by trivial) : CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Under.homMk f w hf) = CategoryTheory.Under.homMk f w
CategoryTheory.MorphismProperty.Under.isoMk_hom_right 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] [Q.RespectsIso] {A B : P.Under Q X} (f : A.right ≅ B.right) (w : CategoryTheory.CategoryStruct.comp A.hom f.hom = B.hom := by cat_disch) : (CategoryTheory.MorphismProperty.Under.isoMk f w).hom.right = f.hom
CategoryTheory.MorphismProperty.Under.isoMk_inv_right 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T} [Q.IsMultiplicative] [Q.RespectsIso] {A B : P.Under Q X} (f : A.right ≅ B.right) (w : CategoryTheory.CategoryStruct.comp A.hom f.hom = B.hom := by cat_disch) : (CategoryTheory.MorphismProperty.Under.isoMk f w).inv.right = f.inv
essentiallySmall_of_le 📋 Mathlib.Algebra.Category.CommAlgCat.FiniteType
{Q : CategoryTheory.MorphismProperty CommRingCat} (hQ : Q ≤ RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => RingHom.FiniteType) (R : CommRingCat) : CategoryTheory.EssentiallySmall.{u, u, u + 1} (Q.Under ⊤ R)
FGAlgCat.equivUnder 📋 Mathlib.Algebra.Category.CommAlgCat.FiniteType
(R : CommRingCat) : FGAlgCat ↑R ≌ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => RingHom.FiniteType).Under ⊤ R
CategoryTheory.MorphismProperty.Under.map 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hPf : P f) : CategoryTheory.Functor (P.Under Q Y) (P.Under Q X)
CategoryTheory.MorphismProperty.Under.pushout 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] : CategoryTheory.Functor (P.Under Q X) (P.Under Q Y)
CategoryTheory.MorphismProperty.Under.mapPushoutAdj 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] [Q.IsStableUnderCobaseChange] (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.HasOfPrecompProperty Q] (hPf : P f) (hQf : Q f) : CategoryTheory.MorphismProperty.Under.pushout P Q f ⊣ CategoryTheory.MorphismProperty.Under.map Q hPf
CategoryTheory.MorphismProperty.instHasPushoutHomDiscretePUnitOfHasPushoutsAlong 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) {X Y : T} (f : X ⟶ Y) [P.HasPushoutsAlong f] (A : P.Under Q X) : CategoryTheory.Limits.HasPushout A.hom f
CategoryTheory.MorphismProperty.instIsRightAdjointUnderTopMapOfHasPushoutsAlongOfIsStableUnderCobaseChangeAlong 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {X Y : T} [P.IsStableUnderComposition] (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] (hPf : P f) : (CategoryTheory.MorphismProperty.Under.map ⊤ hPf).IsRightAdjoint
CategoryTheory.MorphismProperty.isLeftAdjoint_pushout 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {X Y : T} [P.IsStableUnderComposition] (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] (hPf : P f) : (CategoryTheory.MorphismProperty.Under.pushout P ⊤ f).IsLeftAdjoint
CategoryTheory.MorphismProperty.Under.mapCongr 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf : P f) : CategoryTheory.MorphismProperty.Under.map Q hf ≅ CategoryTheory.MorphismProperty.Under.map Q ⋯
CategoryTheory.MorphismProperty.Under.map_obj_right 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hPf : P f) (X✝ : CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.fromPUnit Y) (CategoryTheory.Functor.id T) P ⊤ Q) : ((CategoryTheory.MorphismProperty.Under.map Q hPf).obj X✝).right = X✝.right
CategoryTheory.MorphismProperty.Under.pushoutCongr 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] {g : X ⟶ Y} (h : f = g) : CategoryTheory.MorphismProperty.Under.pushout P Q f ≅ CategoryTheory.MorphismProperty.Under.pushout P Q g
CategoryTheory.MorphismProperty.Under.mapId 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := CategoryTheory.CategoryStruct.id X) (hf : f = CategoryTheory.CategoryStruct.id X := by cat_disch) : CategoryTheory.MorphismProperty.Under.map Q ⋯ ≅ CategoryTheory.Functor.id (P.Under Q X)
CategoryTheory.MorphismProperty.Under.pushout_obj_right 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] (A : P.Under Q X) : ((CategoryTheory.MorphismProperty.Under.pushout P Q f).obj A).right = CategoryTheory.Limits.pushout A.hom f
CategoryTheory.MorphismProperty.Under.map_comp 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y Z : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) : CategoryTheory.MorphismProperty.Under.map Q ⋯ = (CategoryTheory.MorphismProperty.Under.map Q hg).comp (CategoryTheory.MorphismProperty.Under.map Q hf)
CategoryTheory.MorphismProperty.Under.pushoutCompForgetIso 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [CategoryTheory.Limits.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] : (CategoryTheory.MorphismProperty.Under.pushout P Q f).comp (CategoryTheory.MorphismProperty.Under.forget P Q Y) ≅ (CategoryTheory.MorphismProperty.Under.forget P Q X).comp (CategoryTheory.Under.pushout f)
CategoryTheory.MorphismProperty.instHasPushoutInrHomDiscretePUnitOfHasPushoutsAlongOfIsStableUnderCobaseChangeAlong 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) {X Y Z : T} (f : Y ⟶ X) (g : Z ⟶ Y) [P.HasPushoutsAlong f] [P.HasPushoutsAlong g] [P.IsStableUnderCobaseChangeAlong g] (A : P.Under Q Z) : CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr A.hom g) f
CategoryTheory.MorphismProperty.Under.mapComp 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y Z : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] (fg : X ⟶ Z := CategoryTheory.CategoryStruct.comp f g) (hfg : fg = CategoryTheory.CategoryStruct.comp f g := by cat_disch) : CategoryTheory.MorphismProperty.Under.map Q ⋯ ≅ (CategoryTheory.MorphismProperty.Under.map Q hg).comp (CategoryTheory.MorphismProperty.Under.map Q hf)
CategoryTheory.MorphismProperty.Under.pushoutComp 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [P.IsStableUnderCobaseChangeAlong f] [P.IsStableUnderCobaseChangeAlong g] [P.HasPushoutsAlong f] [P.HasPushoutsAlong g] [Q.RespectsIso] [Q.IsStableUnderCobaseChange] (fg : X ⟶ Z := CategoryTheory.CategoryStruct.comp f g) (hfg : fg = CategoryTheory.CategoryStruct.comp f g := by cat_disch) : CategoryTheory.MorphismProperty.Under.pushout P Q fg ≅ (CategoryTheory.MorphismProperty.Under.pushout P Q f).comp (CategoryTheory.MorphismProperty.Under.pushout P Q g)
CategoryTheory.MorphismProperty.Under.pushout_obj_hom 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] (A : P.Under Q X) : ((CategoryTheory.MorphismProperty.Under.pushout P Q f).obj A).hom = CategoryTheory.Limits.pushout.inr A.hom f
CategoryTheory.MorphismProperty.Under.map_obj_hom 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hPf : P f) (X✝ : CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.fromPUnit Y) (CategoryTheory.Functor.id T) P ⊤ Q) : ((CategoryTheory.MorphismProperty.Under.map Q hPf).obj X✝).hom = CategoryTheory.CategoryStruct.comp f X✝.hom
CategoryTheory.MorphismProperty.Under.mapPushoutAdj_unit_app 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] [Q.IsStableUnderCobaseChange] (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.HasOfPrecompProperty Q] (hPf : P f) (hQf : Q f) (A : P.Under Q X) : (CategoryTheory.MorphismProperty.Under.mapPushoutAdj P Q f hPf hQf).unit.app A = CategoryTheory.MorphismProperty.Under.homMk (CategoryTheory.Limits.pushout.inl A.hom f) ⋯ ⋯
CategoryTheory.MorphismProperty.Under.mapCongr_hom_app_right 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf : P f) (X✝ : P.Under Q Y) : ((CategoryTheory.MorphismProperty.Under.mapCongr Q hfg hf).hom.app X✝).right = CategoryTheory.CategoryStruct.id X✝.right
CategoryTheory.MorphismProperty.Under.mapCongr_inv_app_right 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf : P f) (X✝ : P.Under Q Y) : ((CategoryTheory.MorphismProperty.Under.mapCongr Q hfg hf).inv.app X✝).right = CategoryTheory.CategoryStruct.id X✝.right
CategoryTheory.MorphismProperty.Under.pushoutCompForgetIso_hom_app_right 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [CategoryTheory.Limits.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] (X✝ : P.Under Q X) : ((CategoryTheory.MorphismProperty.Under.pushoutCompForgetIso f).hom.app X✝).right = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pushout X✝.hom f)
CategoryTheory.MorphismProperty.Under.pushoutCompForgetIso_inv_app_right 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [CategoryTheory.Limits.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] (X✝ : P.Under Q X) : ((CategoryTheory.MorphismProperty.Under.pushoutCompForgetIso f).inv.app X✝).right = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pushout X✝.hom f)
CategoryTheory.MorphismProperty.Under.mapPushoutAdj_counit_app 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] [Q.IsStableUnderCobaseChange] (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.HasOfPrecompProperty Q] (hPf : P f) (hQf : Q f) (A : P.Under Q Y) : (CategoryTheory.MorphismProperty.Under.mapPushoutAdj P Q f hPf hQf).counit.app A = CategoryTheory.MorphismProperty.Under.homMk (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.id A.right) A.hom ⋯) ⋯ ⋯
CategoryTheory.MorphismProperty.Under.mapId_hom_app_right 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := CategoryTheory.CategoryStruct.id X) (hf : f = CategoryTheory.CategoryStruct.id X := by cat_disch) (X✝ : P.Under Q X) : ((CategoryTheory.MorphismProperty.Under.mapId Q X f hf).hom.app X✝).right = CategoryTheory.CategoryStruct.id X✝.right
CategoryTheory.MorphismProperty.Under.mapId_inv_app_right 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] [P.IsStableUnderComposition] [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := CategoryTheory.CategoryStruct.id X) (hf : f = CategoryTheory.CategoryStruct.id X := by cat_disch) (X✝ : P.Under Q X) : ((CategoryTheory.MorphismProperty.Under.mapId Q X f hf).inv.app X✝).right = CategoryTheory.CategoryStruct.id X✝.right
CategoryTheory.MorphismProperty.Under.pushoutCongr_hom_app_left_fst 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.HasPushoutsAlong f] {g : X ⟶ Y} [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] (h : f = g) (A : P.Under Q X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl A.hom f) ((CategoryTheory.MorphismProperty.Under.pushoutCongr h).hom.app A).right = CategoryTheory.Limits.pushout.inl A.hom g
CategoryTheory.MorphismProperty.Under.mapComp_hom_app_left 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y Z : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) [Q.RespectsIso] (fg : X ⟶ Z := CategoryTheory.CategoryStruct.comp f g) (hfg : fg = CategoryTheory.CategoryStruct.comp f g := by cat_disch) (X✝ : P.Under Q Z) : ((CategoryTheory.MorphismProperty.Under.mapComp Q hf hg fg hfg).hom.app X✝).left = CategoryTheory.CategoryStruct.id ((CategoryTheory.MorphismProperty.Under.map Q ⋯).obj X✝).toComma.1
CategoryTheory.MorphismProperty.Under.map_map_right 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T} (Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} [P.IsStableUnderComposition] {f : X ⟶ Y} (hPf : P f) {X✝ Y✝ : CategoryTheory.MorphismProperty.Comma (CategoryTheory.Functor.fromPUnit Y) (CategoryTheory.Functor.id T) P ⊤ Q} (f✝ : X✝ ⟶ Y✝) : ((CategoryTheory.MorphismProperty.Under.map Q hPf).map f✝).right = (CategoryTheory.MorphismProperty.Comma.Hom.hom f✝).right
CategoryTheory.MorphismProperty.Under.pushoutCongr_hom_app_left_fst_assoc 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] {X Y : T} {f : X ⟶ Y} [P.HasPushoutsAlong f] {g : X ⟶ Y} [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] (h : f = g) (A : P.Under Q X) {Z : T} (h✝ : ((CategoryTheory.MorphismProperty.Under.pushout P Q g).obj A).right ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl A.hom f) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.Under.pushoutCongr h).hom.app A).right h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl A.hom g) h✝
CategoryTheory.MorphismProperty.Under.pushout_map_right 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) [Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [P.HasPushoutsAlong f] [P.IsStableUnderCobaseChangeAlong f] [Q.IsStableUnderCobaseChange] {A B : P.Under Q X} (g : A ⟶ B) : ((CategoryTheory.MorphismProperty.Under.pushout P Q f).map g).right = CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.comp g.right (CategoryTheory.Limits.pushout.inl B.hom f)) (CategoryTheory.Limits.pushout.inr B.hom f) ⋯
CategoryTheory.MorphismProperty.Under.pushoutComp_hom_app_right 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [P.IsStableUnderCobaseChangeAlong f] [P.IsStableUnderCobaseChangeAlong g] [P.HasPushoutsAlong f] [P.HasPushoutsAlong g] [Q.RespectsIso] [Q.IsStableUnderCobaseChange] (fg : X ⟶ Z := CategoryTheory.CategoryStruct.comp f g) (hfg : fg = CategoryTheory.CategoryStruct.comp f g := by cat_disch) (X✝ : P.Under Q X) : ((CategoryTheory.MorphismProperty.Under.pushoutComp f g fg hfg).hom.app X✝).right = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.map X✝.hom fg X✝.hom (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X✝.right) (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯) (CategoryTheory.Limits.pushoutLeftPushoutInrIso X✝.hom f g).inv
CategoryTheory.MorphismProperty.Under.pushoutComp_inv_app_right 📋 Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} [Q.IsMultiplicative] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) [P.IsStableUnderCobaseChangeAlong f] [P.IsStableUnderCobaseChangeAlong g] [P.HasPushoutsAlong f] [P.HasPushoutsAlong g] [Q.RespectsIso] [Q.IsStableUnderCobaseChange] (fg : X ⟶ Z := CategoryTheory.CategoryStruct.comp f g) (hfg : fg = CategoryTheory.CategoryStruct.comp f g := by cat_disch) (X✝ : P.Under Q X) : ((CategoryTheory.MorphismProperty.Under.pushoutComp f g fg hfg).inv.app X✝).right = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso X✝.hom f g).hom (CategoryTheory.Limits.pushout.map X✝.hom (CategoryTheory.CategoryStruct.comp f g) X✝.hom fg (CategoryTheory.CategoryStruct.id X✝.right) (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯)
CategoryTheory.MorphismProperty.Under.instHasInitialTopOfContainsIdentities 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [P.ContainsIdentities] : CategoryTheory.Limits.HasInitial (P.Under ⊤ X)
CategoryTheory.MorphismProperty.Under.instHasPushoutsTopOfIsStableUnderCompositionOfIsStableUnderCobaseChangeOfHasOfPrecompProperty 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [CategoryTheory.Limits.HasPushouts T] [P.IsStableUnderComposition] [P.IsStableUnderCobaseChange] [P.HasOfPrecompProperty P] : CategoryTheory.Limits.HasPushouts (P.Under ⊤ X)
CategoryTheory.MorphismProperty.Under.instHasFiniteColimitsTopOfHasFiniteWidePushouts 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [CategoryTheory.Limits.HasPushouts T] [P.IsStableUnderComposition] [P.ContainsIdentities] [P.IsStableUnderCobaseChange] [P.HasOfPrecompProperty P] [CategoryTheory.Limits.HasFiniteWidePushouts T] : CategoryTheory.Limits.HasFiniteColimits (P.Under ⊤ X)
CategoryTheory.MorphismProperty.Under.mkIdInitial 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [P.ContainsIdentities] : CategoryTheory.Limits.IsInitial (CategoryTheory.MorphismProperty.Under.mk ⊤ (CategoryTheory.CategoryStruct.id X) ⋯)
CategoryTheory.MorphismProperty.Under.instCreatesColimitsOfShapeTopUnderDiscretePEmptyForgetOfContainsIdentitiesOfRespectsIso 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [P.ContainsIdentities] [P.RespectsIso] : CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (CategoryTheory.MorphismProperty.Under.forget P ⊤ X)
CategoryTheory.MorphismProperty.Under.instCreatesColimitsOfShapeTopUnderWalkingSpanForgetOfHasPushoutsOfIsStableUnderCompositionOfIsStableUnderCobaseChangeOfHasOfPrecompProperty 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [CategoryTheory.Limits.HasPushouts T] [P.IsStableUnderComposition] [P.IsStableUnderCobaseChange] [P.HasOfPrecompProperty P] : CategoryTheory.CreatesColimitsOfShape CategoryTheory.Limits.WalkingSpan (CategoryTheory.MorphismProperty.Under.forget P ⊤ X)
CategoryTheory.MorphismProperty.Under.instCreatesFiniteColimitsTopUnderForget 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [CategoryTheory.Limits.HasPushouts T] [P.IsStableUnderComposition] [P.ContainsIdentities] [P.IsStableUnderCobaseChange] [P.HasOfPrecompProperty P] : CategoryTheory.Limits.CreatesFiniteColimits (CategoryTheory.MorphismProperty.Under.forget P ⊤ X)
CategoryTheory.MorphismProperty.Under.instPreservesFiniteColimitsTopUnderForget 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [CategoryTheory.Limits.HasPushouts T] [P.IsStableUnderComposition] [P.ContainsIdentities] [P.IsStableUnderCobaseChange] [P.HasOfPrecompProperty P] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MorphismProperty.Under.forget P ⊤ X)
CategoryTheory.MorphismProperty.Under.instUniqueHomTopMkId 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
{T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {X : T} [P.ContainsIdentities] (Y : P.Under ⊤ X) : Unique (CategoryTheory.MorphismProperty.Under.mk ⊤ (CategoryTheory.CategoryStruct.id X) ⋯ ⟶ Y)
RingHom.HasEqualizers.hasEqualizers 📋 Mathlib.Algebra.Category.Ring.Under.Property
{Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) (hQe : RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.Limits.HasEqualizers ((RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q).Under ⊤ R)
RingHom.HasFiniteProducts.hasFiniteProducts 📋 Mathlib.Algebra.Category.Ring.Under.Property
{Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) (hQp : RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.Limits.HasFiniteProducts ((RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q).Under ⊤ R)
CommRingCat.Under.hasFiniteLimits 📋 Mathlib.Algebra.Category.Ring.Under.Property
{Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) (hQp : RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => Q) (hQe : RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.Limits.HasFiniteLimits ((RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q).Under ⊤ R)
RingHom.HasFiniteProducts.createsFiniteProductsForget 📋 Mathlib.Algebra.Category.Ring.Under.Property
{Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) (hQp : RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.Limits.CreatesFiniteProducts (CategoryTheory.MorphismProperty.Under.forget (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q) ⊤ R)
RingHom.HasEqualizers.createsLimitsWalkingParallelPair 📋 Mathlib.Algebra.Category.Ring.Under.Property
{Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) (hQe : RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MorphismProperty.Under.forget (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q) ⊤ R)
CommRingCat.Under.createsFiniteLimitsForget 📋 Mathlib.Algebra.Category.Ring.Under.Property
{Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) (hQp : RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => Q) (hQe : RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => Q) (R : CommRingCat) : CategoryTheory.Limits.CreatesFiniteLimits (CategoryTheory.MorphismProperty.Under.forget (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q) ⊤ R)
RingHom.HasFiniteProducts.preservesFiniteProducts_pushout 📋 Mathlib.Algebra.Category.Ring.Under.Property
{Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) (hQp : RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => Q) [(RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q).IsStableUnderCobaseChange] {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.MorphismProperty.Under.pushout (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q) ⊤ f)
RingHom.HasStableEqualizers.preservesEqualizers_pushout 📋 Mathlib.Algebra.Category.Ring.Under.Property
{P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) (hPe : RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => P) (hPse : RingHom.HasStableEqualizers fun {R S} [CommRing R] [CommRing S] => P) [(RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).IsStableUnderCobaseChange] {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MorphismProperty.Under.pushout (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P) ⊤ f)
RingHom.HasStableEqualizers.preservesFiniteLimits_pushout 📋 Mathlib.Algebra.Category.Ring.Under.Property
{P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) (hPp : RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => P) (hPe : RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => P) (hPse : RingHom.HasStableEqualizers fun {R S} [CommRing R] [CommRing S] => P) [(RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).IsStableUnderCobaseChange] {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MorphismProperty.Under.pushout (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P) ⊤ f)
CategoryTheory.MorphismProperty.underEquivOfIsTerminal 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : P.Under Q X ≌ CategoryTheory.Discrete PUnit.{w + 1}
CategoryTheory.MorphismProperty.underEquivOfIsTerminal_functor 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.MorphismProperty.underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).functor = CategoryTheory.Functor.star (P.Under Q X)
CategoryTheory.MorphismProperty.underEquivOfIsTerminal_inverse 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.MorphismProperty.underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).inverse = CategoryTheory.Functor.fromPUnit (CategoryTheory.MorphismProperty.Under.mk Q (CategoryTheory.CategoryStruct.id X) ⋯)
CategoryTheory.MorphismProperty.underEquivOfIsTerminal_counitIso 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.MorphismProperty.underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.Functor.fromPUnit (CategoryTheory.MorphismProperty.Under.mk Q (CategoryTheory.CategoryStruct.id X) ⋯)).comp (CategoryTheory.Functor.star (P.Under Q X)))
CategoryTheory.MorphismProperty.underEquivOfIsTerminal_unitIso 📋 Mathlib.CategoryTheory.Comma.Over.StrictInitial
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C) [P.ContainsIdentities] [Q.IsMultiplicative] [Q.RespectsIso] [CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X) : (CategoryTheory.MorphismProperty.underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).unitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.MorphismProperty.Under.isoMk (CategoryTheory.asIso A.hom).symm ⋯) ⋯

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 ?a

If 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 ?b
By 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 find tsum_lt_tsum even though the hypothesis f i < g i is 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 ce5dd8c