Loogle!

Result

Found 16 declarations mentioning CategoryTheory.Subobject.map.

• CategoryTheory.Subobject.map 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Functor (CategoryTheory.Subobject X) (CategoryTheory.Subobject Y)
• CategoryTheory.Subobject.mapPullbackAdj 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Subobject.map f ⊣ CategoryTheory.Subobject.pullback f
• CategoryTheory.Subobject.exists_iso_map 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasImages C] (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Subobject.exists f = CategoryTheory.Subobject.map f
• CategoryTheory.Subobject.map_id 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (x : CategoryTheory.Subobject X) : (CategoryTheory.Subobject.map (CategoryTheory.CategoryStruct.id X)).obj x = x
• CategoryTheory.Subobject.map_obj_injective 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : Function.Injective (CategoryTheory.Subobject.map f).obj
• CategoryTheory.Subobject.map_mk 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A X Y : C} (i : A ⟶ X) [CategoryTheory.Mono i] (f : X ⟶ Y) [CategoryTheory.Mono f] : (CategoryTheory.Subobject.map f).obj (CategoryTheory.Subobject.mk i) = CategoryTheory.Subobject.mk (CategoryTheory.CategoryStruct.comp i f)
• CategoryTheory.Subobject.pullback_map_self 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] (f : X ⟶ Y) [CategoryTheory.Mono f] (g : CategoryTheory.Subobject X) : (CategoryTheory.Subobject.pullback f).obj ((CategoryTheory.Subobject.map f).obj g) = g
• CategoryTheory.Subobject.mapIsoToOrderIso_apply 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) (P : CategoryTheory.Subobject X) : (CategoryTheory.Subobject.mapIsoToOrderIso e) P = (CategoryTheory.Subobject.map e.hom).obj P
• CategoryTheory.Subobject.mapIsoToOrderIso_symm_apply 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) (Q : CategoryTheory.Subobject Y) : (CategoryTheory.Subobject.mapIsoToOrderIso e).symm Q = (CategoryTheory.Subobject.map e.inv).obj Q
• CategoryTheory.Subobject.map_comp 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Mono f] [CategoryTheory.Mono g] (x : CategoryTheory.Subobject X) : (CategoryTheory.Subobject.map (CategoryTheory.CategoryStruct.comp f g)).obj x = (CategoryTheory.Subobject.map g).obj ((CategoryTheory.Subobject.map f).obj x)
• CategoryTheory.Subobject.map_pullback 📋 Mathlib.CategoryTheory.Subobject.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z W : C} {f : X ⟶ Y} {g : X ⟶ Z} {h : Y ⟶ W} {k : Z ⟶ W} [CategoryTheory.Mono h] [CategoryTheory.Mono g] (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk f g comm)) (p : CategoryTheory.Subobject Y) : (CategoryTheory.Subobject.map g).obj ((CategoryTheory.Subobject.pullback f).obj p) = (CategoryTheory.Subobject.pullback k).obj ((CategoryTheory.Subobject.map h).obj p)
• CategoryTheory.Subobject.map_top 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : (CategoryTheory.Subobject.map f).obj ⊤ = CategoryTheory.Subobject.mk f
• CategoryTheory.Subobject.map_bot 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.InitialMonoClass C] (f : X ⟶ Y) [CategoryTheory.Mono f] : (CategoryTheory.Subobject.map f).obj ⊥ = ⊥
• CategoryTheory.Subobject.inf_map 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {X Y : C} (g : Y ⟶ X) [CategoryTheory.Mono g] (f₁ f₂ : CategoryTheory.Subobject Y) : (CategoryTheory.Subobject.map g).obj (f₁ ⊓ f₂) = (CategoryTheory.Subobject.map g).obj f₁ ⊓ (CategoryTheory.Subobject.map g).obj f₂
• CategoryTheory.Subobject.inf_eq_map_pullback 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} (f₁ : CategoryTheory.MonoOver A) (f₂ : CategoryTheory.Subobject A) : Quotient.mk'' f₁ ⊓ f₂ = (CategoryTheory.Subobject.map f₁.arrow).obj ((CategoryTheory.Subobject.pullback f₁.arrow).obj f₂)
• CategoryTheory.Subobject.inf_eq_map_pullback' 📋 Mathlib.CategoryTheory.Subobject.Lattice
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C] {A : C} (f₁ : CategoryTheory.MonoOver A) (f₂ : CategoryTheory.Subobject A) : (CategoryTheory.Subobject.inf.obj (Quotient.mk'' f₁)).obj f₂ = (CategoryTheory.Subobject.map f₁.arrow).obj ((CategoryTheory.Subobject.pullback f₁.arrow).obj f₂)

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 bce1d65