ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>s : Set A<VAR>FunLike F (↥(StarAlgebra.adjoin R s)) B<VAR>AlgHomClass F R (↥(StarAlgebra.adjoin R s)) B<VAR>StarAlgHomClass F R (↥(StarAlgebra.adjoin R s)) B<VAR>f g : F<VAR>h : ∀ (x : ↥(StarAlgebra.adjoin R s)), ↑x ∈ s → f x = g x<GOAL>f = g
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>a : A<VAR>FunLike F (↥(StarAlgebra.adjoin R {a})) B<VAR>AlgHomClass F R (↥(StarAlgebra.adjoin R {a})) B<VAR>StarAlgHomClass F R (↥(StarAlgebra.adjoin R {a})) B<VAR>f g : F<VAR>h : f ⟨a, ⋯⟩ = g ⟨a, ⋯⟩<GOAL>f = g
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>StarModule R A<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>StarModule R B<VAR>φ : A →⋆ₐ[R] B<GOAL>φ.range = StarSubalgebra.map φ ⊤
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>StarModule R B<VAR>f : A →⋆ₐ[R] B<VAR>S : StarSubalgebra R B<VAR>hf : ∀ (x : A), f x ∈ S<VAR>x : A<GOAL>↑((f.codRestrict S hf) x) = f x
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>StarModule R B<VAR>f : A →⋆ₐ[R] B<VAR>S : StarSubalgebra R B<VAR>hf : ∀ (x : A), f x ∈ S<GOAL>S.subtype.comp (f.codRestrict S hf) = f
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>StarModule R B<VAR>f : A →⋆ₐ[R] B<VAR>S : StarSubalgebra R B<VAR>hf : ∀ (x : A), f x ∈ S<GOAL>Function.Injective ⇑(f.codRestrict S hf) ↔ Function.Injective ⇑f
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>StarModule R B<VAR>f : A →⋆ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>a : A<GOAL>(StarAlgEquiv.ofInjective f hf) a = f.rangeRestrict a
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>Algebra R A<VAR>StarRing A<VAR>Semiring B<VAR>Algebra R B<VAR>StarRing B<VAR>StarModule R B<VAR>f : A →⋆ₐ[R] B<VAR>hf : Function.Injective ⇑f<GOAL>∀ (a : ↥(↑f).range), (StarAlgEquiv.ofInjective f hf).symm a = (AlgEquiv.ofInjective (↑f) hf).invFun a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>Star A<VAR>Star B<VAR>f : A →⋆ₐ[S] B<GOAL>∀ (a : A), (StarAlgHom.restrictScalars R f) a = f a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>Star A<VAR>Star B<GOAL>Function.Injective (StarAlgHom.restrictScalars R)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>Star A<VAR>Star B<VAR>f : A ≃⋆ₐ[S] B<VAR>a : A<GOAL>(StarAlgEquiv.restrictScalars R f) a = f a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>Star A<VAR>Star B<VAR>f : A ≃⋆ₐ[S] B<GOAL>∀ (a : B), (StarAlgEquiv.restrictScalars R f).symm a = f.invFun a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra S B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsScalarTower R S A<VAR>IsScalarTower R S B<VAR>Star A<VAR>Star B<GOAL>Function.Injective (StarAlgEquiv.restrictScalars R)
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R R' : CategoryTheory.Sheaf J RingCat<VAR>α : R ⟶ R'<GOAL>∀ {X Y : SheafOfModules R'} (φ : X ⟶ Y), ((SheafOfModules.restrictScalars α).map φ).val = (PresheafOfModules.restrictScalars α.val).map φ.val
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R R' : CategoryTheory.Sheaf J RingCat<VAR>α : R ⟶ R'<VAR>M' : SheafOfModules R'<GOAL>((SheafOfModules.restrictScalars α).obj M').val = (PresheafOfModules.restrictScalars α.val).obj M'.val
<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>J.WEqualsLocallyBijective AddCommGrp<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<GOAL>∀ {X Y : PresheafOfModules R₀} (f : X ⟶ Y), (PresheafOfModules.sheafification α).map f = PresheafOfModules.sheafifyMap α (CategoryTheory.toSheafify J X.presheaf) (CategoryTheory.toSheafify J Y.presheaf) f ((CategoryTheory.presheafToSheaf J AddCommGrp).map 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>J.WEqualsLocallyBijective AddCommGrp<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>P : PresheafOfModules R₀<VAR>F : SheafOfModules R<VAR>f : (PresheafOfModules.sheafification α).obj P ⟶ F<GOAL>((PresheafOfModules.sheafificationHomEquiv α) f).hom = CategoryTheory.toSheafify J P.presheaf ≫ f.val.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>J.WEqualsLocallyBijective AddCommGrp<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>P : PresheafOfModules R₀<VAR>F : SheafOfModules R<VAR>f : (PresheafOfModules.sheafification α).obj P ⟶ F<GOAL>((PresheafOfModules.sheafificationHomEquiv α) f).hom = ((CategoryTheory.sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)) ((SheafOfModules.toSheaf R).map f)
<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>J.WEqualsLocallyBijective AddCommGrp<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>P : PresheafOfModules R₀<VAR>F : SheafOfModules R<VAR>g : P ⟶ (PresheafOfModules.restrictScalars α).obj ((SheafOfModules.forget R).obj F)<GOAL>(SheafOfModules.toSheaf R).map ((PresheafOfModules.sheafificationHomEquiv α).symm g) = ((CategoryTheory.sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm g.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>J.WEqualsLocallyBijective AddCommGrp<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>X : PresheafOfModules R₀<VAR>Y : SheafOfModules R<GOAL>∀ (a : PresheafOfModules.sheafify α (CategoryTheory.toSheafify J X.presheaf) ⟶ Y), ((PresheafOfModules.sheafificationAdjunction α).homEquiv X Y) a = (PresheafOfModules.sheafifyHomEquiv' α (CategoryTheory.toSheafify J X.presheaf) ⋯) ((SheafOfModules.fullyFaithfulForget R).homEquiv a)
<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>J.WEqualsLocallyBijective AddCommGrp<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>M₀ : PresheafOfModules R₀<GOAL>((PresheafOfModules.sheafificationAdjunction α).unit.app M₀).hom = CategoryTheory.toSheafify J M₀.presheaf
<VAR>R : Type u<VAR>CommRing R<VAR>X : CoalgebraCat R<GOAL>X.toComonObj.X = ModuleCat.of R ↑X.toModuleCat
<VAR>R : Type u<VAR>CommRing R<VAR>X : CoalgebraCat R<GOAL>X.toComonObj.counit = ModuleCat.ofHom Coalgebra.counit
<VAR>R : Type u<VAR>CommRing R<VAR>X : CoalgebraCat R<GOAL>X.toComonObj.comul = ModuleCat.ofHom Coalgebra.comul
<VAR>R : Type u<VAR>CommRing R<GOAL>∀ {X Y : CoalgebraCat R} (f : X ⟶ Y), ((CoalgebraCat.toComon R).map f).hom = ModuleCat.ofHom ↑f.toCoalgHom
<VAR>R : Type u<VAR>CommRing R<VAR>X : CoalgebraCat R<GOAL>(CoalgebraCat.toComon R).obj X = X.toComonObj
<VAR>R : Type u<VAR>CommRing R<VAR>X : Comon_ (ModuleCat R)<GOAL>Coalgebra.comul = X.comul
<VAR>R : Type u<VAR>CommRing R<VAR>X : Comon_ (ModuleCat R)<GOAL>Coalgebra.counit = X.counit
<VAR>R : Type u<VAR>CommRing R<GOAL>(CoalgebraCat.comonEquivalence R).functor = CoalgebraCat.toComon R
<VAR>R : Type u<VAR>CommRing R<GOAL>(CoalgebraCat.comonEquivalence R).inverse = CoalgebraCat.ofComon R
<VAR>R : Type u<VAR>CommRing R<GOAL>(CoalgebraCat.comonEquivalence R).unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CoalgebraCat R)).obj x)) ⋯
<VAR>R : Type u<VAR>CommRing R<GOAL>(CoalgebraCat.comonEquivalence R).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (((CoalgebraCat.ofComon R).comp (CoalgebraCat.toComon R)).obj x)) ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>K L : CoalgebraCat R<GOAL>Coalgebra.comul = ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ TensorProduct.map Coalgebra.comul Coalgebra.comul
<VAR>R : Type u<VAR>CommRing R<VAR>M N P Q : Type u<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>AddCommGroup Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Coalgebra R M<VAR>Coalgebra R N<VAR>Coalgebra R P<VAR>Coalgebra R Q<VAR>f : M →ₗc[R] N<VAR>g : P →ₗc[R] Q<GOAL>(CategoryTheory.MonoidalCategory.tensorHom (CoalgebraCat.ofHom f) (CoalgebraCat.ofHom g)).toCoalgHom.toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap
<VAR>R : Type u<VAR>CommRing R<VAR>M N P : Type u<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Coalgebra R M<VAR>Coalgebra R N<VAR>Coalgebra R P<GOAL>(CategoryTheory.MonoidalCategory.associator (CoalgebraCat.of R M) (CoalgebraCat.of R N) (CoalgebraCat.of R P)).hom.toCoalgHom.toLinearMap = ↑(TensorProduct.assoc R M N P)
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>Coalgebra R M<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor (CoalgebraCat.of R M)).hom.toCoalgHom.toLinearMap = ↑(TensorProduct.lid R M)
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>Coalgebra R M<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor (CoalgebraCat.of R M)).hom.toCoalgHom.toLinearMap = ↑(TensorProduct.rid R M)
<VAR>R : Type u<VAR>CommRing R<VAR>M N : Type u<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Coalgebra R M<VAR>Coalgebra R N<GOAL>Coalgebra.comul = Coalgebra.comul
<VAR>R : Type u<VAR>CommRing R<VAR>M N P : Type u<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Coalgebra R M<VAR>Coalgebra R N<VAR>Coalgebra R P<GOAL>Coalgebra.comul = Coalgebra.comul
<VAR>R : Type u<VAR>CommRing R<VAR>M N : Type u<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Coalgebra R M<VAR>Coalgebra R N<GOAL>Coalgebra.counit = Coalgebra.counit
<VAR>R : Type u<VAR>CommRing R<VAR>M N P : Type u<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Coalgebra R M<VAR>Coalgebra R N<VAR>Coalgebra R P<GOAL>Coalgebra.counit = Coalgebra.counit
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>J.WEqualsLocallyBijective AddCommGrp<VAR>J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>M : SheafOfModules R<VAR>self : M.GeneratingSections<GOAL>CategoryTheory.Epi (M.freeHomEquiv.symm self.s)
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>J.WEqualsLocallyBijective AddCommGrp<VAR>J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>M N : SheafOfModules R<VAR>σ : M.GeneratingSections<VAR>p : M ⟶ N<VAR>CategoryTheory.Epi p<VAR>i : σ.I<GOAL>(σ.ofEpi p).s i = SheafOfModules.sectionsMap p (σ.s i)
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>J.WEqualsLocallyBijective AddCommGrp<VAR>J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>M N : SheafOfModules R<VAR>σ : M.GeneratingSections<VAR>p : M ⟶ N<VAR>CategoryTheory.Epi p<GOAL>(σ.ofEpi p).I = σ.I
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>J.WEqualsLocallyBijective AddCommGrp<VAR>J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>M : SheafOfModules R<VAR>σ : M.GeneratingSections<GOAL>σ.ofEpi (𝟙 M) = σ
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>J.WEqualsLocallyBijective AddCommGrp<VAR>J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>M N P : SheafOfModules R<VAR>σ : M.GeneratingSections<VAR>p : M ⟶ N<VAR>q : N ⟶ P<VAR>CategoryTheory.Epi p<VAR>CategoryTheory.Epi q<GOAL>σ.ofEpi (p ≫ q) = (σ.ofEpi p).ofEpi q
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>M : SheafOfModules R<VAR>∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp<VAR>∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp<VAR>∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>self : M.LocalGeneratorsData<GOAL>J.CoversTop self.X
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>M : SheafOfModules R<VAR>∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp<VAR>∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp<VAR>∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>self : M.IsFiniteType<GOAL>∃ σ, ∀ (i : σ.I), Finite (σ.generators i).I
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>F : C ⥤ D<VAR>S : CategoryTheory.Sheaf J RingCat<VAR>R : CategoryTheory.Sheaf K RingCat<VAR>F.IsContinuous J K<VAR>F.IsContinuous J K<VAR>φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R<GOAL>∀ {X Y : SheafOfModules R} (f : X ⟶ Y), ((SheafOfModules.pushforward φ).map f).val = (PresheafOfModules.pushforward φ.val).map f.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>F : C ⥤ D<VAR>S : CategoryTheory.Sheaf J RingCat<VAR>R : CategoryTheory.Sheaf K RingCat<VAR>F.IsContinuous J K<VAR>F.IsContinuous J K<VAR>φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R<VAR>M : SheafOfModules R<GOAL>((SheafOfModules.pushforward φ).obj M).val = (PresheafOfModules.pushforward φ.val).obj M.val
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>J.WEqualsLocallyBijective AddCommGrp<VAR>J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>M N : SheafOfModules R<VAR>I : Type u<VAR>f : SheafOfModules.free I ⟶ M<VAR>p : M ⟶ N<VAR>i : I<GOAL>N.freeHomEquiv (f ≫ p) i = SheafOfModules.sectionsMap p (M.freeHomEquiv f i)
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>J.WEqualsLocallyBijective AddCommGrp<VAR>J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>M N : SheafOfModules R<VAR>I : Type u<VAR>s : I → M.sections<VAR>p : M ⟶ N<GOAL>M.freeHomEquiv.symm s ≫ p = N.freeHomEquiv.symm fun i => SheafOfModules.sectionsMap p (s i)
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>J.WEqualsLocallyBijective AddCommGrp<VAR>J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>I : Type u<GOAL>∀ {J_1 : Type u} (f : I → J_1), (SheafOfModules.free J_1).freeHomEquiv (SheafOfModules.freeMap f) = SheafOfModules.freeSection ∘ f
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>CategoryTheory.HasWeakSheafify J AddCommGrp<VAR>J.WEqualsLocallyBijective AddCommGrp<VAR>J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>I : Type u<GOAL>∀ {J_1 : Type u} (f : I → J_1) (i : I), SheafOfModules.sectionsMap (SheafOfModules.freeMap f) (SheafOfModules.freeSection i) = SheafOfModules.freeSection (f i)
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>M : SheafOfModules R<VAR>∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp<VAR>∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp<VAR>self : M.QuasicoherentData<GOAL>J.CoversTop self.X
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>M : SheafOfModules R<VAR>∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp<VAR>∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp<VAR>q : M.QuasicoherentData<GOAL>q.localGeneratorsData.I = q.I
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>M : SheafOfModules R<VAR>∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp<VAR>∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp<VAR>q : M.QuasicoherentData<GOAL>∀ (a : q.I), q.localGeneratorsData.X a = q.X a
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>M : SheafOfModules R<VAR>∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp<VAR>∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp<VAR>q : M.QuasicoherentData<VAR>i : q.I<GOAL>q.localGeneratorsData.generators i = (q.presentation i).generators
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>M : SheafOfModules R<VAR>∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp<VAR>∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp<VAR>self : M.IsQuasicoherent<GOAL>Nonempty M.QuasicoherentData
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>M : SheafOfModules R<VAR>∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp<VAR>∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp<VAR>self : M.IsFinitePresentation<GOAL>∃ σ, ∀ (i : σ.I), Finite (σ.presentation i).generators.I ∧ Finite (σ.presentation i).relations.I
<VAR>R : Type u<VAR>Ring R<VAR>J : Type v<VAR>CategoryTheory.Category.{t, v} J<VAR>Small.{w, v} J<GOAL>CategoryTheory.Limits.HasLimitsOfShape J (ModuleCat R)
<VAR>R : Type u<VAR>Ring R<VAR>UnivLE.{v, w}<GOAL>CategoryTheory.Limits.HasLimitsOfSize.{t, v, w, max (w + 1) u} (ModuleCat R)
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type v<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>i : ι<GOAL>(ModuleCat.directLimitDiagram G f).obj i = ModuleCat.of R (G i)
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type v<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<GOAL>∀ {X Y : ι} (hij : X ⟶ Y), (ModuleCat.directLimitDiagram G f).map hij = f X Y ⋯
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type v<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>DecidableEq ι<GOAL>(ModuleCat.directLimitCocone G f).pt = ModuleCat.of R (Module.DirectLimit G f)
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type v<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>DecidableEq ι<VAR>i : ι<GOAL>(ModuleCat.directLimitCocone G f).ι.app i = Module.DirectLimit.of R ι G f i
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type v<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>DecidableEq ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : CategoryTheory.Limits.Cocone (ModuleCat.directLimitDiagram G f)<GOAL>(ModuleCat.directLimitIsColimit G f).desc s = Module.DirectLimit.lift R ι G f s.ι.app ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>F : D ⥤ PresheafOfModules R<VAR>∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ PresheafOfModules.evaluation R X) ⋙ CategoryTheory.forget (ModuleCat ↑(R.obj X))).sections<VAR>c : CategoryTheory.Limits.Cone F<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>hF : ∀ (j : D), CategoryTheory.Presheaf.IsSheaf J (F.obj j).presheaf<VAR>CategoryTheory.Limits.HasLimitsOfShape D AddCommGrp<GOAL>CategoryTheory.Presheaf.IsSheaf J c.pt.presheaf
<VAR>R : Type u<VAR>Ring R<VAR>M N : ModuleCat R<VAR>f₁ f₂ : M ⟶ N<VAR>h : ∀ (x : ↑M), f₁ x = f₂ x<GOAL>f₁ = f₂