ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>i j : K<VAR>F : J ⥤ K ⥤ C<VAR>f : i ⟶ j<GOAL>(CategoryTheory.Limits.limit F).map f ≫ (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F j).hom = (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F i).hom ≫ CategoryTheory.Limits.limMap (CategoryTheory.whiskerLeft F ((CategoryTheory.evaluation K C).map f))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>i j : K<VAR>F : J ⥤ K ⥤ C<VAR>f : i ⟶ j<GOAL>(CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F i).inv ≫ (CategoryTheory.Limits.limit F).map f = CategoryTheory.Limits.limMap (CategoryTheory.whiskerLeft F ((CategoryTheory.evaluation K C).map f)) ≫ (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F j).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>H : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>k : K<VAR>W : C<VAR>f g : W ⟶ (CategoryTheory.Limits.limit H).obj k<VAR>w : ∀ (j : J), f ≫ (CategoryTheory.Limits.limit.π H j).app k = g ≫ (CategoryTheory.Limits.limit.π H j).app k<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>F : J ⥤ K ⥤ C<VAR>j : J<VAR>k : K<GOAL>CategoryTheory.Limits.colimit.ι (F ⋙ (CategoryTheory.evaluation K C).obj k) j ≫ (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F k).inv = (CategoryTheory.Limits.colimit.ι F j).app k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>F : J ⥤ K ⥤ C<VAR>j : J<VAR>k : K<GOAL>(CategoryTheory.Limits.colimit.ι F j).app k ≫ (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F k).hom = CategoryTheory.Limits.colimit.ι (F ⋙ (CategoryTheory.evaluation K C).obj k) j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>F : J ⥤ K ⥤ C<VAR>i j : K<VAR>f : i ⟶ j<GOAL>(CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F i).inv ≫ (CategoryTheory.Limits.colimit F).map f = CategoryTheory.Limits.colimMap (CategoryTheory.whiskerLeft F ((CategoryTheory.evaluation K C).map f)) ≫ (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F j).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>F : J ⥤ K ⥤ C<VAR>i j : K<VAR>f : i ⟶ j<GOAL>(CategoryTheory.Limits.colimit F).map f ≫ (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F j).hom = (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F i).hom ≫ CategoryTheory.Limits.colimMap (CategoryTheory.whiskerLeft F ((CategoryTheory.evaluation K C).map f))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>H : J ⥤ K ⥤ C<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>k : K<VAR>W : C<VAR>f g : (CategoryTheory.Limits.colimit H).obj k ⟶ W<VAR>w : ∀ (j : J), (CategoryTheory.Limits.colimit.ι H j).app k ≫ f = (CategoryTheory.Limits.colimit.ι H j).app k ≫ g<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>F : J ⥤ K ⥤ C<VAR>X : K<GOAL>(CategoryTheory.Limits.limitIsoFlipCompLim F).hom.app X = (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F X).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>F : J ⥤ K ⥤ C<VAR>X : K<GOAL>(CategoryTheory.Limits.limitIsoFlipCompLim F).inv.app X = (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F X).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>F : K ⥤ J ⥤ C<VAR>X : K<GOAL>(CategoryTheory.Limits.limitFlipIsoCompLim F).hom.app X = (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F.flip X).hom ≫ (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>F : K ⥤ J ⥤ C<VAR>X : K<GOAL>(CategoryTheory.Limits.limitFlipIsoCompLim F).inv.app X = (CategoryTheory.Limits.HasLimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).inv ≫ (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F.flip X).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>G : J ⥤ K ⥤ C<VAR>X : K<GOAL>(CategoryTheory.Limits.limitIsoSwapCompLim G).hom.app X = (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation G X).hom ≫ CategoryTheory.Limits.limMap ((CategoryTheory.flipIsoCurrySwapUncurry G).hom.app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>G : J ⥤ K ⥤ C<VAR>X : K<GOAL>(CategoryTheory.Limits.limitIsoSwapCompLim G).inv.app X = CategoryTheory.Limits.limMap ((CategoryTheory.flipIsoCurrySwapUncurry G).inv.app X) ≫ (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation G X).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>F : J ⥤ K ⥤ C<VAR>X : K<GOAL>(CategoryTheory.Limits.colimitIsoFlipCompColim F).hom.app X = (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F X).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>F : J ⥤ K ⥤ C<VAR>X : K<GOAL>(CategoryTheory.Limits.colimitIsoFlipCompColim F).inv.app X = (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F X).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>F : K ⥤ J ⥤ C<VAR>X : K<GOAL>(CategoryTheory.Limits.colimitFlipIsoCompColim F).inv.app X = (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).inv ≫ (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F.flip X).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>F : K ⥤ J ⥤ C<VAR>X : K<GOAL>(CategoryTheory.Limits.colimitFlipIsoCompColim F).hom.app X = (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F.flip X).hom ≫ (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>G : J ⥤ K ⥤ C<VAR>X : K<GOAL>(CategoryTheory.Limits.colimitIsoSwapCompColim G).hom.app X = (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation G X).hom ≫ CategoryTheory.Limits.colimMap ((CategoryTheory.flipIsoCurrySwapUncurry G).hom.app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>G : J ⥤ K ⥤ C<VAR>X : K<GOAL>(CategoryTheory.Limits.colimitIsoSwapCompColim G).inv.app X = CategoryTheory.Limits.colimMap ((CategoryTheory.flipIsoCurrySwapUncurry G).inv.app X) ≫ (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation G X).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>a : CategoryTheory.Over P<GOAL>(CategoryTheory.Abelian.app f a).hom = a.hom ≫ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : C<GOAL>Reflexive (CategoryTheory.Abelian.PseudoEqual P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : C<GOAL>Symmetric (CategoryTheory.Abelian.PseudoEqual P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P : C<GOAL>Transitive (CategoryTheory.Abelian.PseudoEqual P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>a : Q ⟶ P<GOAL>Quot.mk (CategoryTheory.Abelian.PseudoEqual P) (CategoryTheory.Over.mk a) = ⟦CategoryTheory.Over.mk a⟧
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>a b : CategoryTheory.Over P<GOAL>a ≈ b → CategoryTheory.Abelian.app f a ≈ CategoryTheory.Abelian.app f b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>a : CategoryTheory.Over P<GOAL>CategoryTheory.Abelian.Pseudoelement.pseudoApply f ⟦a⟧ = ⟦CategoryTheory.Over.mk (a.hom ≫ f)⟧
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<VAR>a : CategoryTheory.Abelian.Pseudoelement P<GOAL>CategoryTheory.Abelian.Pseudoelement.pseudoApply (f ≫ g) a = CategoryTheory.Abelian.Pseudoelement.pseudoApply g (CategoryTheory.Abelian.Pseudoelement.pseudoApply f a)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q R : C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<GOAL>CategoryTheory.Abelian.Pseudoelement.pseudoApply g ∘ CategoryTheory.Abelian.Pseudoelement.pseudoApply f = CategoryTheory.Abelian.Pseudoelement.pseudoApply (f ≫ g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P : C<VAR>Q : C<VAR>f : CategoryTheory.Over P<GOAL>f ≈ CategoryTheory.Over.mk 0 ↔ f.hom = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q R : C<GOAL>⟦CategoryTheory.Over.mk 0⟧ = ⟦CategoryTheory.Over.mk 0⟧
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P : C<GOAL>0 = ⟦CategoryTheory.Over.mk 0⟧
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<GOAL>⟦CategoryTheory.Over.mk 0⟧ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P : C<VAR>a : CategoryTheory.Over P<GOAL>Quot.mk (CategoryTheory.Abelian.PseudoEqual P) a = 0 ↔ a.hom = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>CategoryTheory.Abelian.Pseudoelement.pseudoApply f 0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P : C<VAR>Q : C<VAR>a : CategoryTheory.Abelian.Pseudoelement P<GOAL>CategoryTheory.Abelian.Pseudoelement.pseudoApply 0 a = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>(∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0) → f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>(∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0) → 0 = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>f = 0 ↔ ∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>CategoryTheory.Mono f<GOAL>Function.Injective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>Function.Injective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f) → ∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0 → a = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>(∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0 → a = 0) → CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>CategoryTheory.Epi f<GOAL>Function.Surjective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<GOAL>Function.Surjective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f) → CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.Exact<VAR>b : CategoryTheory.Abelian.Pseudoelement S.X₂<GOAL>CategoryTheory.Abelian.Pseudoelement.pseudoApply S.g b = 0 → ∃ a, CategoryTheory.Abelian.Pseudoelement.pseudoApply S.f a = b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q R : C<VAR>f : Q ⟶ R<VAR>a : P ⟶ Q<GOAL>a ≫ f = 0 → CategoryTheory.Abelian.Pseudoelement.pseudoApply f (Quot.mk (CategoryTheory.Abelian.PseudoEqual Q) (CategoryTheory.Over.mk a)) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : ∀ (b : CategoryTheory.Abelian.Pseudoelement S.X₂), CategoryTheory.Abelian.Pseudoelement.pseudoApply S.g b = 0 → ∃ a, CategoryTheory.Abelian.Pseudoelement.pseudoApply S.f a = b<GOAL>S.Exact
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>x y : CategoryTheory.Abelian.Pseudoelement P<GOAL>CategoryTheory.Abelian.Pseudoelement.pseudoApply f x = CategoryTheory.Abelian.Pseudoelement.pseudoApply f y → ∃ z, CategoryTheory.Abelian.Pseudoelement.pseudoApply f z = 0 ∧ ∀ (R : C) (g : P ⟶ R), CategoryTheory.Abelian.Pseudoelement.pseudoApply g y = 0 → CategoryTheory.Abelian.Pseudoelement.pseudoApply g z = CategoryTheory.Abelian.Pseudoelement.pseudoApply g x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>P Q R : C<VAR>f : P ⟶ R<VAR>g : Q ⟶ R<VAR>p : CategoryTheory.Abelian.Pseudoelement P<VAR>q : CategoryTheory.Abelian.Pseudoelement Q<GOAL>CategoryTheory.Abelian.Pseudoelement.pseudoApply f p = CategoryTheory.Abelian.Pseudoelement.pseudoApply g q → ∃ s, CategoryTheory.Abelian.Pseudoelement.pseudoApply (CategoryTheory.Limits.pullback.fst f g) s = p ∧ CategoryTheory.Abelian.Pseudoelement.pseudoApply (CategoryTheory.Limits.pullback.snd f g) s = q
<VAR>R : Type u_1<VAR>CommRing R<VAR>G : ModuleCat R<VAR>x y : CategoryTheory.Over G<VAR>h : CategoryTheory.Abelian.PseudoEqual G x y<GOAL>LinearMap.range x.hom = LinearMap.range y.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>h : G.op ⊣ F.op<VAR>Y : D<GOAL>(CategoryTheory.Adjunction.adjointOfOpAdjointOp F G h).counit.app Y = (CategoryTheory.opEquiv (Opposite.op Y) (Opposite.op (F.obj (G.obj Y)))) ((h.homEquiv (Opposite.op Y) (Opposite.op (G.obj Y))) ((CategoryTheory.opEquiv (Opposite.op (G.obj Y)) (Opposite.op (G.obj Y))).symm (𝟙 (G.obj Y))))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>h : G.op ⊣ F.op<VAR>X : C<GOAL>(CategoryTheory.Adjunction.adjointOfOpAdjointOp F G h).unit.app X = (CategoryTheory.opEquiv (Opposite.op (G.obj (F.obj X))) (Opposite.op X)) ((h.homEquiv (Opposite.op (F.obj X)) (Opposite.op X)).symm ((CategoryTheory.opEquiv (Opposite.op (F.obj X)) (Opposite.op (F.obj X))).symm (𝟙 (F.obj X))))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>h : G ⊣ F<VAR>Y : Dᵒᵖ<GOAL>(CategoryTheory.Adjunction.opAdjointOpOfAdjoint F G h).counit.app Y = (CategoryTheory.opEquiv (Opposite.op (F.obj (G.obj (Opposite.unop Y)))) Y).symm (h.unit.app (Opposite.unop Y) ≫ F.map ((CategoryTheory.opEquiv (Opposite.op (G.obj (Opposite.unop Y))) (Opposite.op (G.toPrefunctor.1 (Opposite.unop Y)))) (𝟙 (Opposite.op (G.obj (Opposite.unop Y))))))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>h : G ⊣ F<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.Adjunction.opAdjointOpOfAdjoint F G h).unit.app X = (CategoryTheory.opEquiv X (Opposite.op (G.toPrefunctor.1 (F.obj (Opposite.unop X))))).symm (G.map ((CategoryTheory.opEquiv (Opposite.op (F.obj (Opposite.unop X))) (Opposite.op (F.obj (Opposite.unop X)))) (𝟙 (Opposite.op (F.obj (Opposite.unop X))))) ≫ h.counit.app (Opposite.unop X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Z : C<VAR>I : CategoryTheory.InjectiveResolution Z<GOAL>(CategoryTheory.ShortComplex.mk (I.ι.f 0) (I.cocomplex.d 0 1) ⋯).Exact
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Y Z : C<VAR>f : Z ⟶ Y<VAR>I : CategoryTheory.InjectiveResolution Y<VAR>J : CategoryTheory.InjectiveResolution Z<GOAL>J.cocomplex.d 0 1 ≫ CategoryTheory.InjectiveResolution.descFOne f I J = CategoryTheory.InjectiveResolution.descFZero f I J ≫ I.cocomplex.d 0 1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Y Z : C<VAR>f : Z ⟶ Y<VAR>I : CategoryTheory.InjectiveResolution Y<VAR>J : CategoryTheory.InjectiveResolution Z<GOAL>J.ι ≫ CategoryTheory.InjectiveResolution.desc f I J = (CochainComplex.single₀ C).map f ≫ I.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Y Z : C<VAR>f : Z ⟶ Y<VAR>I : CategoryTheory.InjectiveResolution Y<VAR>J : CategoryTheory.InjectiveResolution Z<GOAL>J.ι.f 0 ≫ (CategoryTheory.InjectiveResolution.desc f I J).f 0 = f ≫ I.ι.f 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Y Z : C<VAR>I : CategoryTheory.InjectiveResolution Y<VAR>J : CategoryTheory.InjectiveResolution Z<VAR>f : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι ≫ f = 0<GOAL>I.cocomplex.d 0 1 ≫ CategoryTheory.InjectiveResolution.descHomotopyZeroZero f comm = f.f 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Y Z : C<VAR>I : CategoryTheory.InjectiveResolution Y<VAR>J : CategoryTheory.InjectiveResolution Z<VAR>f : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι ≫ f = 0<GOAL>I.cocomplex.d 1 2 ≫ CategoryTheory.InjectiveResolution.descHomotopyZeroOne f comm = f.f 1 - CategoryTheory.InjectiveResolution.descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>Y Z : C<VAR>I : CategoryTheory.InjectiveResolution Y<VAR>J : CategoryTheory.InjectiveResolution Z<VAR>f : I.cocomplex ⟶ J.cocomplex<VAR>n : ℕ<VAR>g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n<VAR>g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)<VAR>w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)<GOAL>I.cocomplex.d (n + 2) (n + 3) ≫ CategoryTheory.InjectiveResolution.descHomotopyZeroSucc f n g g' w = f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X : C<VAR>I J : CategoryTheory.InjectiveResolution X<GOAL>I.ι ≫ (I.homotopyEquiv J).hom = J.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X : C<VAR>I J : CategoryTheory.InjectiveResolution X<GOAL>J.ι ≫ (I.homotopyEquiv J).inv = I.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : CategoryTheory.InjectiveResolution X<VAR>J : CategoryTheory.InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<GOAL>(CategoryTheory.injectiveResolutions C).map f ≫ J.iso.hom = I.iso.hom ≫ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.HasInjectiveResolutions C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : CategoryTheory.InjectiveResolution X<VAR>J : CategoryTheory.InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<GOAL>I.iso.inv ≫ (CategoryTheory.injectiveResolutions C).map f = (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ ≫ J.iso.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.EnoughInjectives C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.ShortComplex.mk f (CategoryTheory.Injective.d f) ⋯).Exact
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.EnoughInjectives C<VAR>Z : C<GOAL>(CategoryTheory.InjectiveResolution.ofCocomplex Z).d 0 1 = CategoryTheory.Injective.d (CategoryTheory.Injective.ι Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.EnoughInjectives C<VAR>Z : C<VAR>n : ℕ<GOAL>HomologicalComplex.ExactAt (CategoryTheory.InjectiveResolution.ofCocomplex Z) (n + 1)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.EnoughInjectives C<VAR>Z : C<GOAL>CategoryTheory.InjectiveResolution.of Z = CategoryTheory.InjectiveResolution.mk (CategoryTheory.InjectiveResolution.ofCocomplex Z) ⋯ (((CategoryTheory.InjectiveResolution.ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨CategoryTheory.Injective.ι Z, ⋯⟩) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D C<VAR>G.PreservesZeroMorphisms<VAR>i : F.comp G ≅ CategoryTheory.Functor.id C<VAR>CategoryTheory.Limits.PreservesFiniteLimits G<GOAL>CategoryTheory.Limits.HasKernels C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D C<VAR>G.PreservesZeroMorphisms<VAR>i : F.comp G ≅ CategoryTheory.Functor.id C<VAR>adj : G ⊣ F<GOAL>CategoryTheory.Limits.HasCokernels C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>CategoryTheory.Abelian D<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D C<VAR>G.PreservesZeroMorphisms<VAR>i : F.comp G ≅ CategoryTheory.Functor.id C<VAR>adj : G ⊣ F<VAR>CategoryTheory.Limits.HasCokernels C<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Limits.PreservesFiniteLimits G<VAR>F.PreservesZeroMorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.AbelianOfAdjunction.coimageIsoImage F G i adj f).hom = CategoryTheory.Abelian.coimageImageComparison f