ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>φ : S₁ ⟶ S₂<GOAL>(CategoryTheory.ShortComplex.unopMap φ).τ₃ = φ.τ₁.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>φ : S₁ ⟶ S₂<GOAL>(CategoryTheory.ShortComplex.unopMap φ).τ₁ = φ.τ₃.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ<VAR>φ : S₁ ⟶ S₂<GOAL>(CategoryTheory.ShortComplex.unopMap φ).τ₂ = φ.τ₂.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<GOAL>CategoryTheory.ShortComplex.unopMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id S.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>∀ {X Y : (CategoryTheory.ShortComplex C)ᵒᵖ} (φ : X ⟶ Y), (CategoryTheory.ShortComplex.opFunctor C).map φ = CategoryTheory.ShortComplex.opMap φ.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : (CategoryTheory.ShortComplex C)ᵒᵖ<GOAL>(CategoryTheory.ShortComplex.opFunctor C).obj S = (Opposite.unop S).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex Cᵒᵖ<GOAL>(CategoryTheory.ShortComplex.unopFunctor C).obj S = Opposite.op S.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>∀ {X Y : CategoryTheory.ShortComplex Cᵒᵖ} (φ : X ⟶ Y), (CategoryTheory.ShortComplex.unopFunctor C).map φ = (CategoryTheory.ShortComplex.unopMap φ).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>(CategoryTheory.ShortComplex.opEquiv C).inverse = CategoryTheory.ShortComplex.unopFunctor C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>(CategoryTheory.ShortComplex.opEquiv C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.ShortComplex C)ᵒᵖ)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>(CategoryTheory.ShortComplex.opEquiv C).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.ShortComplex.unopFunctor C).comp (CategoryTheory.ShortComplex.opFunctor C))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<GOAL>(CategoryTheory.ShortComplex.opEquiv C).functor = CategoryTheory.ShortComplex.opFunctor C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.CategoryStruct.comp S.abelianImageToKernel (CategoryTheory.Limits.kernel.ι S.g) = CategoryTheory.Abelian.image.ι S.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.CategoryStruct.comp S.abelianImageToKernel (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).π = CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).i = CategoryTheory.Limits.kernel.ι S.g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).H = CategoryTheory.Abelian.coimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian S).K = CategoryTheory.Limits.kernel S.g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π S.f) S.cokernelToAbelianCoimage = CategoryTheory.Abelian.coimage.π S.g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)) S.cokernelToAbelianCoimage = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).p = CategoryTheory.Limits.cokernel.π S.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).H = CategoryTheory.Abelian.image (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).ι = CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex C<GOAL>(CategoryTheory.ShortComplex.RightHomologyData.ofAbelian S).Q = CategoryTheory.Limits.cokernel S.f
<VAR>R : Type u<VAR>Ring R<VAR>X₁ X₂ X₃ : Type v<VAR>AddCommGroup X₁<VAR>AddCommGroup X₂<VAR>AddCommGroup X₃<VAR>Module R X₁<VAR>Module R X₂<VAR>Module R X₃<VAR>f : X₁ →ₗ[R] X₂<VAR>g : X₂ →ₗ[R] X₃<VAR>hfg : g ∘ₗ f = 0<GOAL>(CategoryTheory.ShortComplex.moduleCatMk f g hfg).X₁ = ModuleCat.of R X₁
<VAR>R : Type u<VAR>Ring R<VAR>X₁ X₂ X₃ : Type v<VAR>AddCommGroup X₁<VAR>AddCommGroup X₂<VAR>AddCommGroup X₃<VAR>Module R X₁<VAR>Module R X₂<VAR>Module R X₃<VAR>f : X₁ →ₗ[R] X₂<VAR>g : X₂ →ₗ[R] X₃<VAR>hfg : g ∘ₗ f = 0<GOAL>(CategoryTheory.ShortComplex.moduleCatMk f g hfg).g = ModuleCat.ofHom g
<VAR>R : Type u<VAR>Ring R<VAR>X₁ X₂ X₃ : Type v<VAR>AddCommGroup X₁<VAR>AddCommGroup X₂<VAR>AddCommGroup X₃<VAR>Module R X₁<VAR>Module R X₂<VAR>Module R X₃<VAR>f : X₁ →ₗ[R] X₂<VAR>g : X₂ →ₗ[R] X₃<VAR>hfg : g ∘ₗ f = 0<GOAL>(CategoryTheory.ShortComplex.moduleCatMk f g hfg).f = ModuleCat.ofHom f
<VAR>R : Type u<VAR>Ring R<VAR>X₁ X₂ X₃ : Type v<VAR>AddCommGroup X₁<VAR>AddCommGroup X₂<VAR>AddCommGroup X₃<VAR>Module R X₁<VAR>Module R X₂<VAR>Module R X₃<VAR>f : X₁ →ₗ[R] X₂<VAR>g : X₂ →ₗ[R] X₃<VAR>hfg : g ∘ₗ f = 0<GOAL>(CategoryTheory.ShortComplex.moduleCatMk f g hfg).X₃ = ModuleCat.of R X₃
<VAR>R : Type u<VAR>Ring R<VAR>X₁ X₂ X₃ : Type v<VAR>AddCommGroup X₁<VAR>AddCommGroup X₂<VAR>AddCommGroup X₃<VAR>Module R X₁<VAR>Module R X₂<VAR>Module R X₃<VAR>f : X₁ →ₗ[R] X₂<VAR>g : X₂ →ₗ[R] X₃<VAR>hfg : g ∘ₗ f = 0<GOAL>(CategoryTheory.ShortComplex.moduleCatMk f g hfg).X₂ = ModuleCat.of R X₂
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<VAR>x : ↑S.X₁<GOAL>S.g (S.f x) = 0
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>S.Exact ↔ ∀ (x₂ : ↑S.X₂), S.g x₂ = 0 → ∃ x₁, S.f x₁ = x₂
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>S.Exact ↔ LinearMap.ker S.g ≤ LinearMap.range S.f
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>S.Exact ↔ LinearMap.range S.f = LinearMap.ker S.g
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<VAR>hS : S.Exact<GOAL>LinearMap.range S.f = LinearMap.ker S.g
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<VAR>hS : S.ShortExact<GOAL>Function.Injective ⇑S.f
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<VAR>hS : S.ShortExact<GOAL>Function.Surjective ⇑S.g
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>S.Exact ↔ Function.Exact ⇑S.f ⇑S.g
<VAR>R : Type u<VAR>Ring R<VAR>X₁ X₂ X₃ : ModuleCat R<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>hfg : LinearMap.range f ≤ LinearMap.ker g<GOAL>(CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg).X₃ = X₃
<VAR>R : Type u<VAR>Ring R<VAR>X₁ X₂ X₃ : ModuleCat R<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>hfg : LinearMap.range f ≤ LinearMap.ker g<GOAL>(CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg).f = f
<VAR>R : Type u<VAR>Ring R<VAR>X₁ X₂ X₃ : ModuleCat R<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>hfg : LinearMap.range f ≤ LinearMap.ker g<GOAL>(CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg).X₂ = X₂
<VAR>R : Type u<VAR>Ring R<VAR>X₁ X₂ X₃ : ModuleCat R<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>hfg : LinearMap.range f ≤ LinearMap.ker g<GOAL>(CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg).g = g
<VAR>R : Type u<VAR>Ring R<VAR>X₁ X₂ X₃ : ModuleCat R<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>hfg : LinearMap.range f ≤ LinearMap.ker g<GOAL>(CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg).X₁ = X₁
<VAR>R : Type u<VAR>Ring R<VAR>X₁ X₂ X₃ : ModuleCat R<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<VAR>hfg : LinearMap.range f = LinearMap.ker g<GOAL>(CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g ⋯).Exact
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<VAR>x : ↑S.X₁<GOAL>↑(S.moduleCatToCycles x) = S.f x
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>S.moduleCatLeftHomologyData.i = (LinearMap.ker S.g).subtype
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>S.moduleCatLeftHomologyData.H = S.moduleCatHomology
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>S.moduleCatLeftHomologyData.π = S.moduleCatHomologyπ
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>S.moduleCatLeftHomologyData.K = ModuleCat.of R ↥(LinearMap.ker S.g)
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>S.moduleCatLeftHomologyData.f' = S.moduleCatToCycles
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom (LinearMap.ker S.g).subtype = S.iCycles
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.inv S.iCycles = (LinearMap.ker S.g).subtype
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>CategoryTheory.CategoryStruct.comp S.toCycles S.moduleCatCyclesIso.hom = S.moduleCatToCycles
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>CategoryTheory.CategoryStruct.comp S.homologyπ S.moduleCatHomologyIso.hom = CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom S.moduleCatHomologyπ
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.inv S.homologyπ = CategoryTheory.CategoryStruct.comp S.moduleCatHomologyπ S.moduleCatHomologyIso.inv
<VAR>R : Type u<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<GOAL>S.Exact ↔ Function.Surjective ⇑S.moduleCatToCycles
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ R : Cᵒᵖ ⥤ RingCat<VAR>α : R₀ ⟶ R<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Cᵒᵖ ⥤ AddCommGrp<VAR>φ : M₀.presheaf ⟶ A<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>hA : CategoryTheory.Presheaf.IsSeparated J A<VAR>Y : C<VAR>r₀ r₀' : ↑(R₀.obj (Opposite.op Y))<VAR>m₀ m₀' : ↑(M₀.presheaf.obj (Opposite.op Y))<VAR>hr₀ : (α.app (Opposite.op Y)) r₀ = (α.app (Opposite.op Y)) r₀'<VAR>hm₀ : (φ.app (Opposite.op Y)) m₀ = (φ.app (Opposite.op Y)) m₀'<GOAL>(φ.app (Opposite.op Y)) (r₀ • m₀) = (φ.app (Opposite.op Y)) (r₀' • m₀')
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ R : Cᵒᵖ ⥤ RingCat<VAR>α : R₀ ⟶ R<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Cᵒᵖ ⥤ AddCommGrp<VAR>φ : M₀.presheaf ⟶ A<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>hA : CategoryTheory.Presheaf.IsSeparated J A<VAR>X : C<VAR>r : ↑(R.obj (Opposite.op X))<VAR>m : ↑(A.obj (Opposite.op X))<VAR>Y Z : C<VAR>f : Y ⟶ X<VAR>g : Z ⟶ Y<VAR>r₀ : ↑(R₀.obj (Opposite.op Y))<VAR>r₀' : ↑(R₀.obj (Opposite.op Z))<VAR>m₀ : ↑(M₀.presheaf.obj (Opposite.op Y))<VAR>m₀' : ↑(M₀.presheaf.obj (Opposite.op Z))<VAR>hr₀ : (α.app (Opposite.op Y)) r₀ = (R.map f.op) r<VAR>hr₀' : (α.app (Opposite.op Z)) r₀' = (R.map (f.op ≫ g.op)) r<VAR>hm₀ : (φ.app (Opposite.op Y)) m₀ = (A.map f.op) m<VAR>hm₀' : (φ.app (Opposite.op Z)) m₀' = (A.map (f.op ≫ g.op)) m<GOAL>(φ.app (Opposite.op Z)) ((M₀.presheaf.map g.op) (r₀ • m₀)) = (φ.app (Opposite.op Z)) (r₀' • m₀')
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ R : Cᵒᵖ ⥤ RingCat<VAR>α : R₀ ⟶ R<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Cᵒᵖ ⥤ AddCommGrp<VAR>φ : M₀.presheaf ⟶ A<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>hA : CategoryTheory.Presheaf.IsSeparated J A<VAR>X : C<VAR>r : ↑(R.obj (Opposite.op X))<VAR>m : ↑(A.obj (Opposite.op X))<VAR>P : CategoryTheory.Presieve X<VAR>r₀ : CategoryTheory.Presieve.FamilyOfElements (R₀ ⋙ CategoryTheory.forget RingCat) P<VAR>m₀ : CategoryTheory.Presieve.FamilyOfElements (M₀.presheaf ⋙ CategoryTheory.forget AddCommGrp) P<VAR>hr₀ : (r₀.map (CategoryTheory.whiskerRight α (CategoryTheory.forget RingCat))).IsAmalgamation r<VAR>hm₀ : (m₀.map (CategoryTheory.whiskerRight φ (CategoryTheory.forget AddCommGrp))).IsAmalgamation m<GOAL>((r₀.smul m₀).map (CategoryTheory.whiskerRight φ (CategoryTheory.forget AddCommGrp))).Compatible
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>M₀ : PresheafOfModules R₀<VAR>A : CategoryTheory.Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>X : Cᵒᵖ<VAR>r : ↑(R.val.obj X)<VAR>m : ↑(A.val.obj X)<VAR>self : PresheafOfModules.Sheafify.SMulCandidate α φ r m<VAR>Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>r₀ : ↑(R₀.obj Y)<VAR>hr₀ : (α.app Y) r₀ = (R.val.map f) r<VAR>m₀ : ↑(M₀.obj Y)<VAR>hm₀ : (φ.app Y) m₀ = (A.val.map f) m<GOAL>(A.val.map f) self.x = (φ.app Y) (r₀ • m₀)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>CategoryTheory.Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : CategoryTheory.Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>CategoryTheory.Presheaf.IsLocallySurjective J φ<VAR>X : Cᵒᵖ<VAR>r : ↑(R.val.obj X)<VAR>m : ↑(A.val.obj X)<VAR>Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>r₀ : ↑(R₀.obj Y)<VAR>hr₀ : (α.app Y) r₀ = (R.val.map f) r<VAR>m₀ : ↑(M₀.obj Y)<VAR>hm₀ : (φ.app Y) m₀ = (A.val.map f) m<GOAL>(A.val.map f) (PresheafOfModules.Sheafify.smul α φ r m) = (φ.app Y) (r₀ • m₀)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>CategoryTheory.Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : CategoryTheory.Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>CategoryTheory.Presheaf.IsLocallySurjective J φ<VAR>X : Cᵒᵖ<VAR>m : ↑(A.val.obj X)<GOAL>PresheafOfModules.Sheafify.smul α φ 1 m = m
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>CategoryTheory.Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : CategoryTheory.Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>CategoryTheory.Presheaf.IsLocallySurjective J φ<VAR>X : Cᵒᵖ<VAR>m : ↑(A.val.obj X)<GOAL>PresheafOfModules.Sheafify.smul α φ 0 m = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>CategoryTheory.Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : CategoryTheory.Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>CategoryTheory.Presheaf.IsLocallySurjective J φ<VAR>X : Cᵒᵖ<VAR>r : ↑(R.val.obj X)<GOAL>PresheafOfModules.Sheafify.smul α φ r 0 = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>CategoryTheory.Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : CategoryTheory.Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>CategoryTheory.Presheaf.IsLocallySurjective J φ<VAR>X : Cᵒᵖ<VAR>r : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<GOAL>PresheafOfModules.Sheafify.smul α φ r (m + m') = PresheafOfModules.Sheafify.smul α φ r m + PresheafOfModules.Sheafify.smul α φ r m'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>CategoryTheory.Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : CategoryTheory.Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>CategoryTheory.Presheaf.IsLocallySurjective J φ<VAR>X : Cᵒᵖ<VAR>r r' : ↑(R.val.obj X)<VAR>m : ↑(A.val.obj X)<GOAL>PresheafOfModules.Sheafify.smul α φ (r + r') m = PresheafOfModules.Sheafify.smul α φ r m + PresheafOfModules.Sheafify.smul α φ r' m
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>CategoryTheory.Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : CategoryTheory.Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>CategoryTheory.Presheaf.IsLocallySurjective J φ<VAR>X : Cᵒᵖ<VAR>r r' : ↑(R.val.obj X)<VAR>m : ↑(A.val.obj X)<GOAL>PresheafOfModules.Sheafify.smul α φ (r * r') m = PresheafOfModules.Sheafify.smul α φ r (PresheafOfModules.Sheafify.smul α φ r' m)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>CategoryTheory.Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : CategoryTheory.Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>CategoryTheory.Presheaf.IsLocallySurjective J φ<VAR>X : Cᵒᵖ<VAR>Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r : ↑(R.val.obj X)<VAR>m : ↑(A.val.obj X)<GOAL>(A.val.map π) (PresheafOfModules.Sheafify.smul α φ r m) = PresheafOfModules.Sheafify.smul α φ ((R.val.map π) r) ((A.val.map π) m)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>CategoryTheory.Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : CategoryTheory.Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>CategoryTheory.Presheaf.IsLocallySurjective J φ<GOAL>(PresheafOfModules.toSheafify α φ).hom = φ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>CategoryTheory.Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : CategoryTheory.Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>CategoryTheory.Presheaf.IsLocallySurjective J φ<VAR>J.WEqualsLocallyBijective AddCommGrp<VAR>F : PresheafOfModules R.val<VAR>hF : CategoryTheory.Presheaf.IsSheaf J F.presheaf<VAR>f : M₀ ⟶ (PresheafOfModules.restrictScalars α).obj F<GOAL>φ ≫ ((PresheafOfModules.sheafifyHomEquiv' α φ hF).symm f).hom = f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J α<VAR>CategoryTheory.Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : CategoryTheory.Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ<VAR>CategoryTheory.Presheaf.IsLocallySurjective J φ<VAR>J.WEqualsLocallyBijective AddCommGrp<VAR>M₀' : PresheafOfModules R₀<VAR>A' : CategoryTheory.Sheaf J AddCommGrp<VAR>φ' : M₀'.presheaf ⟶ A'.val<VAR>CategoryTheory.Presheaf.IsLocallyInjective J φ'<VAR>CategoryTheory.Presheaf.IsLocallySurjective J φ'<VAR>τ₀ : M₀ ⟶ M₀'<VAR>τ : A ⟶ A'<VAR>fac : τ₀.hom ≫ φ' = φ ≫ τ.val<GOAL>(PresheafOfModules.sheafifyMap α φ φ' τ₀ τ fac).val.hom = τ.val
<VAR>V : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} V<VAR>CategoryTheory.Abelian V<VAR>X Y Z : V<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>w : f ≫ g = 0<GOAL>imageToKernel g.op f.op ⋯ = (CategoryTheory.Limits.imageSubobjectIso g.op ≪≫ (CategoryTheory.imageOpOp g).symm).hom ≫ (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.factorThruImage g) ⋯).op ≫ (CategoryTheory.Limits.kernelSubobjectIso f.op ≪≫ CategoryTheory.kernelOpOp f).inv
<VAR>V : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} V<VAR>CategoryTheory.Abelian V<VAR>X Y Z : Vᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>w : f ≫ g = 0<GOAL>imageToKernel g.unop f.unop ⋯ = (CategoryTheory.Limits.imageSubobjectIso g.unop ≪≫ (CategoryTheory.imageUnopUnop g).symm).hom ≫ (CategoryTheory.Limits.cokernel.desc f (CategoryTheory.Limits.factorThruImage g) ⋯).unop ≫ (CategoryTheory.Limits.kernelSubobjectIso f.unop ≪≫ CategoryTheory.kernelUnopUnop f).inv
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex V c<VAR>i : ι<GOAL>X.op.X i = Opposite.op (X.X i)
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex V c<VAR>i j : ι<GOAL>X.op.d i j = (X.d j i).op
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex V c.symm<VAR>i : ι<GOAL>X.opSymm.X i = Opposite.op (X.X i)
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} V<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X : HomologicalComplex V c.symm<VAR>i j : ι<GOAL>X.opSymm.d i j = (X.d j i).op