Loogle!

Result

Found 17 declarations mentioning CategoryTheory.Limits.Sigma.map.

• CategoryTheory.Limits.Sigma.map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] (p : (b : β) → f b ⟶ g b) : ∐ f ⟶ ∐ g
• CategoryTheory.Limits.Sigma.map_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} [CategoryTheory.Limits.HasCoproduct f] : (CategoryTheory.Limits.Sigma.map fun a => CategoryTheory.CategoryStruct.id (f a)) = CategoryTheory.CategoryStruct.id (∐ f)
• CategoryTheory.Limits.Sigma.map_epi 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] (p : (b : β) → f b ⟶ g b) [∀ (i : β), CategoryTheory.Epi (p i)] : CategoryTheory.Epi (CategoryTheory.Limits.Sigma.map p)
• CategoryTheory.Limits.Sigma.map'_id 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : α → C} [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] (p : (b : α) → f b ⟶ g b) : CategoryTheory.Limits.Sigma.map' id p = CategoryTheory.Limits.Sigma.map p
• CategoryTheory.Limits.Sigma.map_isIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ⟶ g b) [∀ (b : β), CategoryTheory.IsIso (p b)] : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.map p)
• CategoryTheory.Limits.Sigma.map_comp_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g h : α → C} [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] [CategoryTheory.Limits.HasCoproduct h] (q : (a : α) → f a ⟶ g a) (q' : (a : α) → g a ⟶ h a) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map q) (CategoryTheory.Limits.Sigma.map q') = CategoryTheory.Limits.Sigma.map fun a => CategoryTheory.CategoryStruct.comp (q a) (q' a)
• CategoryTheory.Limits.Sigma.map_comp_map' 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : α → C} {h : β → C} [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] [CategoryTheory.Limits.HasCoproduct h] (p : α → β) (q : (a : α) → f a ⟶ g a) (q' : (a : α) → g a ⟶ h (p a)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map q) (CategoryTheory.Limits.Sigma.map' p q') = CategoryTheory.Limits.Sigma.map' p fun a => CategoryTheory.CategoryStruct.comp (q a) (q' a)
• CategoryTheory.Limits.Sigma.map'_comp_map 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : α → C} {g h : β → C} [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] [CategoryTheory.Limits.HasCoproduct h] (p : α → β) (q : (a : α) → f a ⟶ g (p a)) (q' : (b : β) → g b ⟶ h b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map' p q) (CategoryTheory.Limits.Sigma.map q') = CategoryTheory.Limits.Sigma.map' p fun a => CategoryTheory.CategoryStruct.comp (q a) (q' (p a))
• CategoryTheory.Limits.sigmaConst_map_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (n : Type w) : (CategoryTheory.Limits.sigmaConst.map f).app n = CategoryTheory.Limits.Sigma.map fun x => f
• CategoryTheory.Limits.Sigma.map_mono 📋 Mathlib.CategoryTheory.Limits.Shapes.Biproducts
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [CategoryTheory.Limits.HasBiproduct f] [CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) [∀ (j : J), CategoryTheory.Mono (p j)] : CategoryTheory.Mono (CategoryTheory.Limits.Sigma.map p)
• CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShape.mk 📋 Mathlib.CategoryTheory.MorphismProperty.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1) [W.RespectsIso] (hW : ∀ (X₁ X₂ : J → C) [inst : CategoryTheory.Limits.HasCoproduct X₁] [inst_1 : CategoryTheory.Limits.HasCoproduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (CategoryTheory.Limits.Sigma.map f)) : W.IsStableUnderCoproductsOfShape J
• CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset.eq_1 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α = { obj := CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj, map := fun {X Y} β => { app := fun x => CategoryTheory.Limits.Sigma.map fun x_1 => β.app ↑x_1, naturality := ⋯ }, map_id := ⋯, map_comp := ⋯ }
• CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_map_app 📋 Mathlib.CategoryTheory.Limits.Constructions.Filtered
  (C : Type u) [CategoryTheory.Category.{v, u} C] (α : Type w) [CategoryTheory.Limits.HasFiniteCoproducts C] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.Discrete α) C} (β : X✝ ⟶ Y✝) (x✝ : Finset (CategoryTheory.Discrete α)) : ((CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α).map β).app x✝ = CategoryTheory.Limits.Sigma.map fun x => β.app ↑x
• CategoryTheory.instHasLiftingPropertyMap_1 📋 Mathlib.CategoryTheory.LiftingProperties.Limits
  {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {J : Type u_2} {A B : J → C} [CategoryTheory.Limits.HasCoproduct A] [CategoryTheory.Limits.HasCoproduct B] (f : (j : J) → A j ⟶ B j) {X Y : C} (p : X ⟶ Y) [∀ (j : J), CategoryTheory.HasLiftingProperty (f j) p] : CategoryTheory.HasLiftingProperty (CategoryTheory.Limits.Sigma.map f) p
• HomotopicalAlgebra.instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.Limits.HasCoproduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Cofibration (f i)] [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] : HomotopicalAlgebra.Cofibration (CategoryTheory.Limits.Sigma.map f)
• HomotopicalAlgebra.instWeakEquivalenceMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations 📋 Mathlib.AlgebraicTopology.ModelCategory.Instances
  {C : Type u} [CategoryTheory.Category.{v, u} C] [HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.CategoryWithCofibrations C] [HomotopicalAlgebra.CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.Limits.HasCoproduct Y] [h : ∀ (i : J), HomotopicalAlgebra.Cofibration (f i)] [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)] [∀ (i : J), HomotopicalAlgebra.WeakEquivalence (f i)] : HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Limits.Sigma.map f)
• CategoryTheory.Limits.FormalCoproduct.eval_map_app 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts
  (C : Type u) [CategoryTheory.Category.{v, u} C] (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasCoproducts A] {X✝ Y✝ : CategoryTheory.Functor C A} (α : X✝ ⟶ Y✝) (f : CategoryTheory.Limits.FormalCoproduct C) : ((CategoryTheory.Limits.FormalCoproduct.eval C A).map α).app f = CategoryTheory.Limits.Sigma.map fun i => α.app (f.obj i)

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 ff04530 serving mathlib revision 8623f65