Loogle!

Result

Found 60 declarations mentioning CategoryTheory.Limits.HasMulticoequalizer.

• CategoryTheory.Limits.HasMulticoequalizer 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) : Prop
• CategoryTheory.Limits.multicoequalizer 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] : C
• CategoryTheory.Limits.Multicoequalizer.multicofork 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] : CategoryTheory.Limits.Multicofork I
• CategoryTheory.Limits.Multicoequalizer.π 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] (b : J.R) : I.right b ⟶ CategoryTheory.Limits.multicoequalizer I
• CategoryTheory.Limits.Multicoequalizer.sigmaπ 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] : ∐ I.right ⟶ CategoryTheory.Limits.multicoequalizer I
• CategoryTheory.Limits.Multicoequalizer.instEpiSigmaπ 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] : CategoryTheory.Epi (CategoryTheory.Limits.Multicoequalizer.sigmaπ I)
• CategoryTheory.Limits.Multicoequalizer.multicofork_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] (b : J.R) : (CategoryTheory.Limits.Multicoequalizer.multicofork I).π b = CategoryTheory.Limits.Multicoequalizer.π I b
• CategoryTheory.Limits.Multicoequalizer.instHasCoequalizerFstSigmaMapSndSigmaMap 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] : CategoryTheory.Limits.HasCoequalizer I.fstSigmaMap I.sndSigmaMap
• CategoryTheory.Limits.Multicoequalizer.multicofork_ι_app_right' 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] (b : J.R) : CategoryTheory.Limits.colimit.ι I.multispan (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.Limits.Multicoequalizer.π I b
• CategoryTheory.Limits.Multicoequalizer.isoCoequalizer 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] : CategoryTheory.Limits.multicoequalizer I ≅ CategoryTheory.Limits.coequalizer I.fstSigmaMap I.sndSigmaMap
• CategoryTheory.Limits.Multicoequalizer.ι_sigmaπ 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : J.R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) (CategoryTheory.Limits.Multicoequalizer.sigmaπ I) = CategoryTheory.Limits.Multicoequalizer.π I b
• CategoryTheory.Limits.Multicoequalizer.condition 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] (a : J.L) : CategoryTheory.CategoryStruct.comp (I.fst a) (CategoryTheory.Limits.Multicoequalizer.π I (J.fst a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.Limits.Multicoequalizer.π I (J.snd a))
• CategoryTheory.Limits.Multicoequalizer.desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] (W : C) (k : (b : J.R) → I.right b ⟶ W) (h : ∀ (a : J.L), CategoryTheory.CategoryStruct.comp (I.fst a) (k (J.fst a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (k (J.snd a))) : CategoryTheory.Limits.multicoequalizer I ⟶ W
• CategoryTheory.Limits.Multicoequalizer.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] {W : C} (i j : CategoryTheory.Limits.multicoequalizer I ⟶ W) (h : ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) j) : i = j
• CategoryTheory.Limits.Multicoequalizer.hom_ext_iff 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} {I : CategoryTheory.Limits.MultispanIndex J C} [CategoryTheory.Limits.HasMulticoequalizer I] {W : C} {i j : CategoryTheory.Limits.multicoequalizer I ⟶ W} : i = j ↔ ∀ (b : J.R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) j
• CategoryTheory.Limits.Multicoequalizer.condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] (a : J.L) {Z : C} (h : CategoryTheory.Limits.multicoequalizer I ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.fst a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I (J.fst a)) h) = CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I (J.snd a)) h)
• CategoryTheory.Limits.Multicoequalizer.ι_sigmaπ_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : J.R) {Z : C} (h : CategoryTheory.Limits.multicoequalizer I ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.sigmaπ I) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) h
• CategoryTheory.Limits.Multicoequalizer.π_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] (W : C) (k : (b : J.R) → I.right b ⟶ W) (h : ∀ (a : J.L), CategoryTheory.CategoryStruct.comp (I.fst a) (k (J.fst a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (k (J.snd a))) (b : J.R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) (CategoryTheory.Limits.Multicoequalizer.desc I W k h) = k b
• CategoryTheory.Limits.Multicoequalizer.multicofork_ι_app_right 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] (b : J.R) : (CategoryTheory.Limits.Multicoequalizer.multicofork I).ι.app (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.Limits.Multicoequalizer.π I b
• CategoryTheory.Limits.Multicoequalizer.π_desc_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape} (I : CategoryTheory.Limits.MultispanIndex J C) [CategoryTheory.Limits.HasMulticoequalizer I] (W : C) (k : (b : J.R) → I.right b ⟶ W) (h : ∀ (a : J.L), CategoryTheory.CategoryStruct.comp (I.fst a) (k (J.fst a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (k (J.snd a))) (b : J.R) {Z : C} (h✝ : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.desc I W k h) h✝) = CategoryTheory.CategoryStruct.comp (k b) h✝
• CategoryTheory.GlueData.glued 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer D.diagram] : C
• CategoryTheory.GlueData.ι 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer D.diagram] (i : D.J) : D.U i ⟶ D.glued
• CategoryTheory.GlueData.vPullbackCone 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer D.diagram] (i j : D.J) : CategoryTheory.Limits.PullbackCone (D.ι i) (D.ι j)
• CategoryTheory.GlueData.π 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.HasColimits C] : D.sigmaOpens ⟶ D.glued
• CategoryTheory.GlueData.π_epi 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.HasColimits C] : CategoryTheory.Epi D.π
• CategoryTheory.GlueData.hasColimit_multispan_comp 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] : CategoryTheory.Limits.HasColimit (D.diagram.multispan.comp F)
• CategoryTheory.GlueData.hasColimit_mapGlueData_diagram 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] : CategoryTheory.Limits.HasMulticoequalizer (D.mapGlueData F).diagram
• CategoryTheory.GlueData.gluedIso 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] : F.obj D.glued ≅ (D.mapGlueData F).glued
• CategoryTheory.GlueData.glue_condition 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer D.diagram] (i j : D.J) : CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.CategoryStruct.comp (D.f j i) (D.ι j)) = CategoryTheory.CategoryStruct.comp (D.f i j) (D.ι i)
• CategoryTheory.GlueData.ι_gluedIso_inv 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) : CategoryTheory.CategoryStruct.comp ((D.mapGlueData F).ι i) (D.gluedIso F).inv = F.map (D.ι i)
• CategoryTheory.GlueData.ι_gluedIso_hom 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) : CategoryTheory.CategoryStruct.comp (F.map (D.ι i)) (D.gluedIso F).hom = (D.mapGlueData F).ι i
• CategoryTheory.GlueData.ι_jointly_surjective 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer D.diagram] (F : CategoryTheory.Functor C (Type v)) [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (x : F.obj D.glued) : ∃ i y, (CategoryTheory.ConcreteCategory.hom (F.map (D.ι i))) y = x
• CategoryTheory.GlueData.vPullbackConeIsLimitOfMap 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (i j : D.J) [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan (D.ι i) (D.ι j)) F] (hc : CategoryTheory.Limits.IsLimit ((D.mapGlueData F).vPullbackCone i j)) : CategoryTheory.Limits.IsLimit (D.vPullbackCone i j)
• CategoryTheory.GlueData.ι_gluedIso_inv_assoc 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) {Z : C'} (h : F.obj D.glued ⟶ Z) : CategoryTheory.CategoryStruct.comp ((D.mapGlueData F).ι i) (CategoryTheory.CategoryStruct.comp (D.gluedIso F).inv h) = CategoryTheory.CategoryStruct.comp (F.map (D.ι i)) h
• CategoryTheory.GlueData.ι_gluedIso_hom_assoc 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C') [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] [∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] (i : D.J) {Z : C'} (h : (D.mapGlueData F).glued ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (D.ι i)) (CategoryTheory.CategoryStruct.comp (D.gluedIso F).hom h) = CategoryTheory.CategoryStruct.comp ((D.mapGlueData F).ι i) h
• CategoryTheory.GlueData.glue_condition_apply 📋 Mathlib.CategoryTheory.GlueData
  {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) [CategoryTheory.Limits.HasMulticoequalizer D.diagram] (i j : D.J) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier (D.V (i, j))) : (CategoryTheory.ConcreteCategory.hom (D.ι j)) ((CategoryTheory.ConcreteCategory.hom (D.f j i)) ((CategoryTheory.ConcreteCategory.hom (D.t i j)) x)) = (CategoryTheory.ConcreteCategory.hom (D.ι i)) ((CategoryTheory.ConcreteCategory.hom (D.f i j)) x)
• AlgebraicGeometry.Scheme.GlueData.instHasMulticoequalizerDiagram 📋 Mathlib.AlgebraicGeometry.Gluing
  (D : AlgebraicGeometry.Scheme.GlueData) : CategoryTheory.Limits.HasMulticoequalizer D.diagram
• CategoryTheory.OrthogonalReflection.succ 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C) [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] : C
• CategoryTheory.OrthogonalReflection.succStruct 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] (Z₀ : C) : CategoryTheory.SmallObject.SuccStruct C
• CategoryTheory.OrthogonalReflection.toSucc 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C) [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] : Z ⟶ CategoryTheory.OrthogonalReflection.succ W Z
• CategoryTheory.OrthogonalReflection.fromStep 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C) [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] : CategoryTheory.OrthogonalReflection.step W Z ⟶ CategoryTheory.OrthogonalReflection.succ W Z
• CategoryTheory.OrthogonalReflection.isLocal_isLocal_toSucc 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C) [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] : W.isLocal.isLocal (CategoryTheory.OrthogonalReflection.toSucc W Z)
• CategoryTheory.OrthogonalReflection.isIso_toSucc_iff 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C) [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] : CategoryTheory.IsIso (CategoryTheory.OrthogonalReflection.toSucc W Z) ↔ W.isLocal Z
• CategoryTheory.OrthogonalReflection.reflectionObj 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C) [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] : C
• CategoryTheory.OrthogonalReflection.reflection 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C) [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] : Z ⟶ CategoryTheory.OrthogonalReflection.reflectionObj W Z κ
• CategoryTheory.OrthogonalReflection.isLocal_isLocal_reflection 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C) [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] : W.isLocal.isLocal (CategoryTheory.OrthogonalReflection.reflection W Z κ)
• CategoryTheory.OrthogonalReflection.toSucc_surjectivity 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C} [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] {X Y : C} (f : X ⟶ Y) (hf : W f) (g : X ⟶ Z) : ∃ g', CategoryTheory.CategoryStruct.comp f g' = CategoryTheory.CategoryStruct.comp g (CategoryTheory.OrthogonalReflection.toSucc W Z)
• CategoryTheory.OrthogonalReflection.iteration 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C) [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] : CategoryTheory.Functor κ.ord.ToType C
• CategoryTheory.OrthogonalReflection.isLocal_reflectionObj 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} (Z : C) [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] {κ : Cardinal.{w}} [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] (hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → CategoryTheory.IsCardinalPresentable X κ ∧ CategoryTheory.IsCardinalPresentable Y κ) : W.isLocal (CategoryTheory.OrthogonalReflection.reflectionObj W Z κ)
• CategoryTheory.OrthogonalReflection.toSucc_injectivity 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C} [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] {X Y : C} (f : X ⟶ Y) (hf : W f) (g₁ g₂ : Y ⟶ Z) (hg : CategoryTheory.CategoryStruct.comp f g₁ = CategoryTheory.CategoryStruct.comp f g₂) : CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.OrthogonalReflection.toSucc W Z) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.OrthogonalReflection.toSucc W Z)
• CategoryTheory.OrthogonalReflection.isRightAdjoint_ι 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] (hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → CategoryTheory.IsCardinalPresentable X κ ∧ CategoryTheory.IsCardinalPresentable Y κ) : W.isLocal.ι.IsRightAdjoint
• CategoryTheory.OrthogonalReflection.D₂.condition 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C} [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] {X Y : C} (f : X ⟶ Y) (hf : W f) {g₁ g₂ : Y ⟶ CategoryTheory.OrthogonalReflection.step W Z} (h : CategoryTheory.CategoryStruct.comp f g₁ = CategoryTheory.CategoryStruct.comp f g₂) : CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.OrthogonalReflection.fromStep W Z) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.OrthogonalReflection.fromStep W Z)
• CategoryTheory.OrthogonalReflection.corepresentableBy 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} (Z : C) [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] {κ : Cardinal.{w}} [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] (hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → CategoryTheory.IsCardinalPresentable X κ ∧ CategoryTheory.IsCardinalPresentable Y κ) : (W.isLocal.ι.comp (CategoryTheory.coyoneda.obj (Opposite.op Z))).CorepresentableBy { obj := CategoryTheory.OrthogonalReflection.reflectionObj W Z κ, property := ⋯ }
• CategoryTheory.OrthogonalReflection.D₂.condition_assoc 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C} [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] {X Y : C} (f : X ⟶ Y) (hf : W f) {g₁ g₂ : Y ⟶ CategoryTheory.OrthogonalReflection.step W Z} (h : CategoryTheory.CategoryStruct.comp f g₁ = CategoryTheory.CategoryStruct.comp f g₂) {Z✝ : C} (h✝ : CategoryTheory.OrthogonalReflection.succ W Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.fromStep W Z) h✝) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.fromStep W Z) h✝)
• CategoryTheory.OrthogonalReflection.transfiniteCompositionOfShapeReflection 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C) [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] : W.isLocal.isLocal.TransfiniteCompositionOfShape κ.ord.ToType (CategoryTheory.OrthogonalReflection.reflection W Z κ)
• CategoryTheory.OrthogonalReflection.iterationObjSuccIso 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C) [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] (j : κ.ord.ToType) : (CategoryTheory.OrthogonalReflection.iteration W Z κ).obj (Order.succ j) ≅ CategoryTheory.OrthogonalReflection.succ W ((CategoryTheory.OrthogonalReflection.iteration W Z κ).obj j)
• CategoryTheory.OrthogonalReflection.iteration_map_succ_surjectivity 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C} [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] {κ : Cardinal.{w}} [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] {X Y : C} (f : X ⟶ Y) (hf : W f) {j : κ.ord.ToType} (g : X ⟶ (CategoryTheory.OrthogonalReflection.iteration W Z κ).obj j) : ∃ g', CategoryTheory.CategoryStruct.comp f g' = CategoryTheory.CategoryStruct.comp g ((CategoryTheory.OrthogonalReflection.iteration W Z κ).map (CategoryTheory.homOfLE ⋯))
• CategoryTheory.OrthogonalReflection.iteration_map_succ_injectivity 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C} [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] {κ : Cardinal.{w}} [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] {X Y : C} (f : X ⟶ Y) (hf : W f) {j : κ.ord.ToType} (g₁ g₂ : Y ⟶ (CategoryTheory.OrthogonalReflection.iteration W Z κ).obj j) (hg : CategoryTheory.CategoryStruct.comp f g₁ = CategoryTheory.CategoryStruct.comp f g₂) : CategoryTheory.CategoryStruct.comp g₁ ((CategoryTheory.OrthogonalReflection.iteration W Z κ).map (CategoryTheory.homOfLE ⋯)) = CategoryTheory.CategoryStruct.comp g₂ ((CategoryTheory.OrthogonalReflection.iteration W Z κ).map (CategoryTheory.homOfLE ⋯))
• CategoryTheory.OrthogonalReflection.iteration_map_succ 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C) [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] (j : κ.ord.ToType) : (CategoryTheory.OrthogonalReflection.iteration W Z κ).map (CategoryTheory.homOfLE ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.toSucc W ((CategoryTheory.OrthogonalReflection.iteration W Z κ).obj j)) (CategoryTheory.OrthogonalReflection.iterationObjSuccIso W Z κ j).inv
• CategoryTheory.OrthogonalReflection.iteration_map_succ_assoc 📋 Mathlib.CategoryTheory.Presentable.OrthogonalReflection
  {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C) [CategoryTheory.Limits.HasPushouts C] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] [∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] [∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] (j : κ.ord.ToType) {Z✝ : C} (h : (CategoryTheory.OrthogonalReflection.iteration W Z κ).obj (Order.succ j) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.OrthogonalReflection.iteration W Z κ).map (CategoryTheory.homOfLE ⋯)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.toStep W ((CategoryTheory.OrthogonalReflection.iteration W Z κ).obj j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.fromStep W ((CategoryTheory.OrthogonalReflection.iteration W Z κ).obj j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.iterationObjSuccIso W Z κ j).inv h))

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:

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.

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