Loogle!

Result

Found 31 declarations mentioning CategoryTheory.Square.map.

• CategoryTheory.Square.map 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : CategoryTheory.Square D
• CategoryTheory.Square.map_X₁ 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).X₁ = F.obj sq.X₁
• CategoryTheory.Square.map_X₂ 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).X₂ = F.obj sq.X₂
• CategoryTheory.Square.map_X₃ 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).X₃ = F.obj sq.X₃
• CategoryTheory.Square.map_X₄ 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).X₄ = F.obj sq.X₄
• CategoryTheory.Functor.mapSquare_obj 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (sq : CategoryTheory.Square C) : F.mapSquare.obj sq = sq.map F
• CategoryTheory.Square.map_f₁₂ 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).f₁₂ = F.map sq.f₁₂
• CategoryTheory.Square.map_f₁₃ 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).f₁₃ = F.map sq.f₁₃
• CategoryTheory.Square.map_f₂₄ 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).f₂₄ = F.map sq.f₂₄
• CategoryTheory.Square.map_f₃₄ 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).f₃₄ = F.map sq.f₃₄
• CategoryTheory.Functor.mapSquare_map_τ₁ 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (F.mapSquare.map φ).τ₁ = F.map φ.τ₁
• CategoryTheory.Functor.mapSquare_map_τ₂ 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (F.mapSquare.map φ).τ₂ = F.map φ.τ₂
• CategoryTheory.Functor.mapSquare_map_τ₃ 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (F.mapSquare.map φ).τ₃ = F.map φ.τ₃
• CategoryTheory.Functor.mapSquare_map_τ₄ 📋 Mathlib.CategoryTheory.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (F.mapSquare.map φ).τ₄ = F.map φ.τ₄
• CategoryTheory.Square.IsPullback.map 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {sq : CategoryTheory.Square C} (h : sq.IsPullback) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F] : (sq.map F).IsPullback
• CategoryTheory.Square.IsPullback.of_map 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {sq : CategoryTheory.Square C} (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F] (h : (sq.map F).IsPullback) : sq.IsPullback
• CategoryTheory.Square.IsPushout.map 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {sq : CategoryTheory.Square C} (h : sq.IsPushout) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span sq.f₁₂ sq.f₁₃) F] : (sq.map F).IsPushout
• CategoryTheory.Square.IsPushout.of_map 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {sq : CategoryTheory.Square C} (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span sq.f₁₂ sq.f₁₃) F] (h : (sq.map F).IsPushout) : sq.IsPushout
• CategoryTheory.Square.isPullback_iff_map_coyoneda_isPullback 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.IsPullback ↔ ∀ (X : Cᵒᵖ), (sq.map (CategoryTheory.coyoneda.obj X)).IsPullback
• CategoryTheory.Square.isPushout_iff_op_map_yoneda_isPullback 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.IsPushout ↔ ∀ (X : C), (sq.op.map (CategoryTheory.yoneda.obj X)).IsPullback
• CategoryTheory.Square.IsPullback.map_iff 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F] [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F] : (sq.map F).IsPullback ↔ sq.IsPullback
• CategoryTheory.Square.IsPushout.map_iff 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span sq.f₁₂ sq.f₁₃) F] [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span sq.f₁₂ sq.f₁₃) F] : (sq.map F).IsPushout ↔ sq.IsPushout
• CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk' 📋 Mathlib.CategoryTheory.Sites.MayerVietorisSquare
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (sq : CategoryTheory.Square C) [CategoryTheory.Mono sq.f₁₃] (H : ∀ (F : CategoryTheory.Sheaf J (Type v)), (sq.op.map F.val).IsPullback) : J.MayerVietorisSquare
• CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk'_toSquare 📋 Mathlib.CategoryTheory.Sites.MayerVietorisSquare
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (sq : CategoryTheory.Square C) [CategoryTheory.Mono sq.f₁₃] (H : ∀ (F : CategoryTheory.Sheaf J (Type v)), (sq.op.map F.val).IsPullback) : (CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk' sq H).toSquare = sq
• CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushout 📋 Mathlib.CategoryTheory.Sites.MayerVietorisSquare
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (self : J.MayerVietorisSquare) : (self.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout
• CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk 📋 Mathlib.CategoryTheory.Sites.MayerVietorisSquare
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (toSquare : CategoryTheory.Square C) (mono_f₁₃ : CategoryTheory.Mono toSquare.f₁₃ := by infer_instance) (isPushout : (toSquare.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout) : J.MayerVietorisSquare
• CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk.injEq 📋 Mathlib.CategoryTheory.Sites.MayerVietorisSquare
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (toSquare : CategoryTheory.Square C) (mono_f₁₃ : CategoryTheory.Mono toSquare.f₁₃ := by infer_instance) (isPushout : (toSquare.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout) (toSquare✝ : CategoryTheory.Square C) (mono_f₁₃✝ : CategoryTheory.Mono toSquare✝.f₁₃ := by infer_instance) (isPushout✝ : (toSquare✝.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout) : ({ toSquare := toSquare, mono_f₁₃ := mono_f₁₃, isPushout := isPushout } = { toSquare := toSquare✝, mono_f₁₃ := mono_f₁₃✝, isPushout := isPushout✝ }) = (toSquare = toSquare✝)
• CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff 📋 Mathlib.CategoryTheory.Sites.MayerVietorisSquare
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (F : CategoryTheory.Sheaf J (Type v)) (sq : CategoryTheory.Square C) : (sq.op.map ((CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v))).op.comp (CategoryTheory.yoneda.obj F))).IsPullback ↔ (sq.op.map F.val).IsPullback
• CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk.sizeOf_spec 📋 Mathlib.CategoryTheory.Sites.MayerVietorisSquare
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [SizeOf C] (toSquare : CategoryTheory.Square C) (mono_f₁₃ : CategoryTheory.Mono toSquare.f₁₃ := by infer_instance) (isPushout : (toSquare.map (CategoryTheory.yoneda.comp (CategoryTheory.presheafToSheaf J (Type v)))).IsPushout) : sizeOf { toSquare := toSquare, mono_f₁₃ := mono_f₁₃, isPushout := isPushout } = 1 + sizeOf toSquare + sizeOf mono_f₁₃ + sizeOf isPushout
• CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf 📋 Mathlib.CategoryTheory.Sites.MayerVietorisSquare
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] (S : J.MayerVietorisSquare) [CategoryTheory.HasWeakSheafify J AddCommGrp] : (S.map (CategoryTheory.yoneda.comp (((CategoryTheory.whiskeringRight Cᵒᵖ (Type v) AddCommGrp).obj AddCommGrp.free).comp (CategoryTheory.presheafToSheaf J AddCommGrp)))).IsPushout
• CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f 📋 Mathlib.CategoryTheory.Sites.MayerVietorisSquare
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J (Type v)] [CategoryTheory.HasSheafify J AddCommGrp] (S : J.MayerVietorisSquare) : S.shortComplex.f = CategoryTheory.Limits.biprod.lift ((CategoryTheory.presheafToSheaf J AddCommGrp).map (CategoryTheory.whiskerRight (CategoryTheory.yoneda.map S.f₁₂) AddCommGrp.free)) (-(CategoryTheory.presheafToSheaf J AddCommGrp).map (CategoryTheory.whiskerRight (CategoryTheory.yoneda.map S.f₁₃) AddCommGrp.free))

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