Loogle!

Result

Found 30 declarations mentioning CategoryTheory.CostructuredArrow.map.

• CategoryTheory.CostructuredArrow.map 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T') : CategoryTheory.Functor (CategoryTheory.CostructuredArrow S T) (CategoryTheory.CostructuredArrow S T')
• CategoryTheory.CostructuredArrow.map_id 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} : (CategoryTheory.CostructuredArrow.map (CategoryTheory.CategoryStruct.id T)).obj f = f
• CategoryTheory.CostructuredArrow.map_obj_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T') (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)) : ((CategoryTheory.CostructuredArrow.map f).obj X).left = X.left
• CategoryTheory.CostructuredArrow.map_obj_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T') (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)) : ((CategoryTheory.CostructuredArrow.map f).obj X).right = X.right
• CategoryTheory.CostructuredArrow.map_mk 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {Y : C} {S : CategoryTheory.Functor C D} {f : S.obj Y ⟶ T} (g : T ⟶ T') : (CategoryTheory.CostructuredArrow.map g).obj (CategoryTheory.CostructuredArrow.mk f) = CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp f g)
• CategoryTheory.CostructuredArrow.map_obj_hom 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T') (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)) : ((CategoryTheory.CostructuredArrow.map f).obj X).hom = CategoryTheory.CategoryStruct.comp X.hom f
• CategoryTheory.CostructuredArrow.map_comp 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' T'' : D} {S : CategoryTheory.Functor C D} {f : T ⟶ T'} {f' : T' ⟶ T''} {h : CategoryTheory.CostructuredArrow S T} : (CategoryTheory.CostructuredArrow.map (CategoryTheory.CategoryStruct.comp f f')).obj h = (CategoryTheory.CostructuredArrow.map f').obj ((CategoryTheory.CostructuredArrow.map f).obj h)
• CategoryTheory.CostructuredArrow.map_map_left 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T') {X✝ Y✝ : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f✝ : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.map f).map f✝).left = f✝.left
• CategoryTheory.CostructuredArrow.map_map_right 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T') {X✝ Y✝ : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (f✝ : X✝ ⟶ Y✝) : ((CategoryTheory.CostructuredArrow.map f).map f✝).right = CategoryTheory.CategoryStruct.id X✝.right
• CategoryTheory.CategoryOfElements.costructuredArrow_yoneda_equivalence_naturality 📋 Mathlib.CategoryTheory.Elements
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ (Type v)} (α : F₁ ⟶ F₂) : (CategoryTheory.CategoryOfElements.map α).op.comp (CategoryTheory.CategoryOfElements.toCostructuredArrow F₂) = (CategoryTheory.CategoryOfElements.toCostructuredArrow F₁).comp (CategoryTheory.CostructuredArrow.map α)
• CategoryTheory.Functor.pointwiseLeftKanExtension_map 📋 Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
  {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂) : (L.pointwiseLeftKanExtension F).map f = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj L Y₁).comp F) { pt := CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L Y₂).comp F), ι := { app := fun g => CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L Y₂).comp F) ((CategoryTheory.CostructuredArrow.map f).obj g), naturality := ⋯ } }
• CategoryTheory.CostructuredArrow.functor_map 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (T : CategoryTheory.Functor C D) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (CategoryTheory.CostructuredArrow.functor T).map f = CategoryTheory.CostructuredArrow.map f
• CategoryTheory.CostructuredArrow.map.eq_1 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T T' : D} {S : CategoryTheory.Functor C D} (f : T ⟶ T') : CategoryTheory.CostructuredArrow.map f = CategoryTheory.Comma.mapRight S ((CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{1})).map f)
• CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) : (CategoryTheory.CostructuredArrow.map f).comp ((CategoryTheory.Grothendieck.ι (CategoryTheory.CostructuredArrow.functor L) Y).comp (CategoryTheory.CostructuredArrow.grothendieckProj L)) ≅ CategoryTheory.CostructuredArrow.proj L X
• CategoryTheory.CostructuredArrow.grothendieckProj_map 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Grothendieck (CategoryTheory.CostructuredArrow.functor L)} (f : X✝ ⟶ Y✝) : (CategoryTheory.CostructuredArrow.grothendieckProj L).map f = f.fiber.left
• CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_hom_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) (X✝ : CategoryTheory.CostructuredArrow L X) : (CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj L f).hom.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
• CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj_inv_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) {X Y : D} (f : X ⟶ Y) (X✝ : CategoryTheory.CostructuredArrow L X) : (CategoryTheory.CostructuredArrow.mapCompιCompGrothendieckProj L f).inv.app X✝ = CategoryTheory.CategoryStruct.id X✝.left
• CategoryTheory.Limits.Cocone.toCostructuredArrowCocone 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone K) (F : CategoryTheory.Functor C D) {X : D} (f : F.obj c.pt ⟶ X) : CategoryTheory.Limits.Cocone ((F.mapCocone c).toCostructuredArrow.comp ((CategoryTheory.CostructuredArrow.map f).comp (CategoryTheory.CostructuredArrow.pre K F X)))
• CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_pt 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone K) (F : CategoryTheory.Functor C D) {X : D} (f : F.obj c.pt ⟶ X) : (c.toCostructuredArrowCocone F f).pt = CategoryTheory.CostructuredArrow.mk f
• CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone K) (F : CategoryTheory.Functor C D) {X : D} (f : F.obj c.pt ⟶ X) (j : J) : (c.toCostructuredArrowCocone F f).ι.app j = CategoryTheory.CostructuredArrow.homMk (c.ι.app j) ⋯
• CategoryTheory.NonemptyParallelPairPresentationAux.F₁ 📋 Mathlib.CategoryTheory.Limits.Indization.ParallelPair
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : CategoryTheory.Limits.IndObjectPresentation A) (P₂ : CategoryTheory.Limits.IndObjectPresentation B) : CategoryTheory.Functor (CategoryTheory.NonemptyParallelPairPresentationAux.K f g P₁ P₂) C
• CategoryTheory.NonemptyParallelPairPresentationAux.F₂ 📋 Mathlib.CategoryTheory.Limits.Indization.ParallelPair
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : CategoryTheory.Limits.IndObjectPresentation A) (P₂ : CategoryTheory.Limits.IndObjectPresentation B) : CategoryTheory.Functor (CategoryTheory.NonemptyParallelPairPresentationAux.K f g P₁ P₂) C
• CategoryTheory.NonemptyParallelPairPresentationAux.ψ 📋 Mathlib.CategoryTheory.Limits.Indization.ParallelPair
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : CategoryTheory.Limits.IndObjectPresentation A) (P₂ : CategoryTheory.Limits.IndObjectPresentation B) : CategoryTheory.NonemptyParallelPairPresentationAux.F₁ f g P₁ P₂ ⟶ CategoryTheory.NonemptyParallelPairPresentationAux.F₂ f g P₁ P₂
• CategoryTheory.NonemptyParallelPairPresentationAux.ϕ 📋 Mathlib.CategoryTheory.Limits.Indization.ParallelPair
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : CategoryTheory.Limits.IndObjectPresentation A) (P₂ : CategoryTheory.Limits.IndObjectPresentation B) : CategoryTheory.NonemptyParallelPairPresentationAux.F₁ f g P₁ P₂ ⟶ CategoryTheory.NonemptyParallelPairPresentationAux.F₂ f g P₁ P₂
• CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₁ 📋 Mathlib.CategoryTheory.Limits.Indization.ParallelPair
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : CategoryTheory.Limits.IndObjectPresentation A) (P₂ : CategoryTheory.Limits.IndObjectPresentation B) : CategoryTheory.Limits.IsColimit { pt := A, ι := CategoryTheory.NonemptyParallelPairPresentationAux.ι₁ f g P₁ P₂ }
• CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₂ 📋 Mathlib.CategoryTheory.Limits.Indization.ParallelPair
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : CategoryTheory.Limits.IndObjectPresentation A) (P₂ : CategoryTheory.Limits.IndObjectPresentation B) : CategoryTheory.Limits.IsColimit { pt := B, ι := CategoryTheory.NonemptyParallelPairPresentationAux.ι₂ f g P₁ P₂ }
• CategoryTheory.NonemptyParallelPairPresentationAux.hf 📋 Mathlib.CategoryTheory.Limits.Indization.ParallelPair
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : CategoryTheory.Limits.IndObjectPresentation A) (P₂ : CategoryTheory.Limits.IndObjectPresentation B) : f = (CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₁ f g P₁ P₂).map { pt := B, ι := CategoryTheory.NonemptyParallelPairPresentationAux.ι₂ f g P₁ P₂ } (CategoryTheory.whiskerRight (CategoryTheory.NonemptyParallelPairPresentationAux.ϕ f g P₁ P₂) CategoryTheory.yoneda)
• CategoryTheory.NonemptyParallelPairPresentationAux.hg 📋 Mathlib.CategoryTheory.Limits.Indization.ParallelPair
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : CategoryTheory.Limits.IndObjectPresentation A) (P₂ : CategoryTheory.Limits.IndObjectPresentation B) : g = (CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₁ f g P₁ P₂).map { pt := B, ι := CategoryTheory.NonemptyParallelPairPresentationAux.ι₂ f g P₁ P₂ } (CategoryTheory.whiskerRight (CategoryTheory.NonemptyParallelPairPresentationAux.ψ f g P₁ P₂) CategoryTheory.yoneda)
• CategoryTheory.NonemptyParallelPairPresentationAux.ι₁ 📋 Mathlib.CategoryTheory.Limits.Indization.ParallelPair
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : CategoryTheory.Limits.IndObjectPresentation A) (P₂ : CategoryTheory.Limits.IndObjectPresentation B) : (CategoryTheory.NonemptyParallelPairPresentationAux.F₁ f g P₁ P₂).comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const (CategoryTheory.NonemptyParallelPairPresentationAux.K f g P₁ P₂)).obj A
• CategoryTheory.NonemptyParallelPairPresentationAux.ι₂ 📋 Mathlib.CategoryTheory.Limits.Indization.ParallelPair
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B) (P₁ : CategoryTheory.Limits.IndObjectPresentation A) (P₂ : CategoryTheory.Limits.IndObjectPresentation B) : (CategoryTheory.NonemptyParallelPairPresentationAux.F₂ f g P₁ P₂).comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const (CategoryTheory.NonemptyParallelPairPresentationAux.K f g P₁ P₂)).obj B

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

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

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

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision 40fea08