Ab

📁 Source: Mathlib/Algebra/Homology/ShortComplex/Ab.lean

Statistics

Metric	Count
Definitions Ab, abCyclesIso, abHomologyIso, abLeftHomologyData, abToCycles	5
Theorems ab_finite, ab_range_eq_ker, ab_exact_iff_function_exact, ab_finite_iff, ab_injective_f, ab_surjective_g, abCyclesIso_inv_apply_iCycles, abLeftHomologyData_H_coe, abLeftHomologyData_K_coe, abLeftHomologyData_f', abLeftHomologyData_i, abLeftHomologyData_π, abToCycles_apply_coe, ab_exact_iff, ab_exact_iff_function_exact, ab_exact_iff_ker_le_range, ab_exact_iff_range_eq_ker, ab_zero_apply, exact_iff_surjective_abToCycles	19
Total	24

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
abCyclesIso 📖	CompOp	1 math math: abCyclesIso_inv_apply_iCycles
abHomologyIso 📖	CompOp	—
abLeftHomologyData 📖	CompOp	5 math math: abLeftHomologyData_π, abLeftHomologyData_K_coe, abLeftHomologyData_f', abLeftHomologyData_i, abLeftHomologyData_H_coe
abToCycles 📖	CompOp	5 math math: abToCycles_apply_coe, abLeftHomologyData_π, exact_iff_surjective_abToCycles, abLeftHomologyData_f', abLeftHomologyData_H_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abCyclesIso_inv_apply_iCycles 📖	mathematical	—	DFunLike.coe cycles Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian AddCommGrpCat.instAbelian X₂ AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier iCycles AddCommGrpCat.of AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker X₃ AddCommGrpCat.Hom.hom g AddSubgroup.toAddCommGroup CategoryTheory.Iso.inv abCyclesIso	—	hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ConcreteCategory.comp_apply LeftHomologyData.cyclesIso_inv_comp_iCycles
abLeftHomologyData_H_coe 📖	mathematical	—	AddCommGrpCat.carrier LeftHomologyData.H Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive abLeftHomologyData HasQuotient.Quotient X₂ AddSubgroup AddCommGroup.toAddGroup AddCommGrpCat.str SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker X₃ AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGrpCat.Hom.hom g AddSubgroup.toAddGroup QuotientAddGroup.instHasQuotientAddSubgroup AddMonoidHom.range X₁ abToCycles	—	—
abLeftHomologyData_K_coe 📖	mathematical	—	AddCommGrpCat.carrier LeftHomologyData.K Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive abLeftHomologyData X₂ AddSubgroup AddCommGroup.toAddGroup AddCommGrpCat.str SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker X₃ AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGrpCat.Hom.hom g	—	—
abLeftHomologyData_f' 📖	mathematical	—	LeftHomologyData.f' Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive abLeftHomologyData AddCommGrpCat.ofHom AddCommGrpCat.carrier X₁ X₂ AddSubgroup AddCommGroup.toAddGroup AddCommGrpCat.str SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker X₃ AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGrpCat.Hom.hom g AddSubgroup.toAddCommGroup abToCycles	—	—
abLeftHomologyData_i 📖	mathematical	—	LeftHomologyData.i Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive abLeftHomologyData AddCommGrpCat.ofHom AddCommGrpCat.carrier X₂ AddSubgroup AddCommGroup.toAddGroup AddCommGrpCat.str SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker X₃ AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGrpCat.Hom.hom g AddSubgroup.toAddCommGroup AddSubgroup.subtype	—	—
abLeftHomologyData_π 📖	mathematical	—	LeftHomologyData.π Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive abLeftHomologyData AddCommGrpCat.ofHom AddCommGrpCat.carrier X₂ AddSubgroup AddCommGroup.toAddGroup AddCommGrpCat.str SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker X₃ AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGrpCat.Hom.hom g HasQuotient.Quotient AddSubgroup.toAddGroup QuotientAddGroup.instHasQuotientAddSubgroup AddMonoidHom.range X₁ abToCycles AddSubgroup.toAddCommGroup QuotientAddGroup.Quotient.addCommGroup QuotientAddGroup.mk'	—	—
abToCycles_apply_coe 📖	mathematical	—	AddCommGrpCat.carrier X₂ Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive AddSubgroup AddCommGroup.toAddGroup AddCommGrpCat.str SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker X₃ AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGrpCat.Hom.hom g DFunLike.coe AddMonoidHom X₁ AddZeroClass.toAddZero AddSubgroup.toAddGroup AddMonoidHom.instFunLike abToCycles CategoryTheory.ConcreteCategory.hom AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier f	—	—
ab_exact_iff 📖	mathematical	—	Exact Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive AddCommGrpCat.carrier X₁ DFunLike.coe X₂ CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier f	—	exact_iff_surjective_abToCycles
ab_exact_iff_function_exact 📖	mathematical	—	Exact Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive Function.Exact AddCommGrpCat.carrier X₁ X₂ X₃ DFunLike.coe CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier f g NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	ab_exact_iff ab_zero_apply
ab_exact_iff_ker_le_range 📖	mathematical	—	Exact Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive AddSubgroup AddCommGrpCat.carrier X₂ AddCommGroup.toAddGroup AddCommGrpCat.str Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder AddMonoidHom.ker X₃ AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGrpCat.Hom.hom g AddMonoidHom.range X₁ f	—	ab_exact_iff
ab_exact_iff_range_eq_ker 📖	mathematical	—	Exact Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive AddMonoidHom.range AddCommGrpCat.carrier X₁ AddCommGroup.toAddGroup AddCommGrpCat.str X₂ AddCommGrpCat.Hom.hom f AddMonoidHom.ker X₃ AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid g	—	ab_exact_iff_ker_le_range le_antisymm AddMonoidHom.mem_ker CategoryTheory.ConcreteCategory.comp_apply zero le_refl
ab_zero_apply 📖	mathematical	—	DFunLike.coe X₂ Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive X₃ AddCommGrpCat.carrier CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier g X₁ f NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	CategoryTheory.ConcreteCategory.comp_apply zero
exact_iff_surjective_abToCycles 📖	mathematical	—	Exact Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive AddCommGrpCat.carrier X₁ X₂ AddSubgroup AddCommGroup.toAddGroup AddCommGrpCat.str SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.ker X₃ AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGrpCat.Hom.hom g DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddSubgroup.toAddGroup AddMonoidHom.instFunLike abToCycles	—	LeftHomologyData.exact_iff_epi_f' CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian abLeftHomologyData_f' AddCommGrpCat.epi_iff_surjective

CategoryTheory.ShortComplex.Exact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ab_finite 📖	mathematical	CategoryTheory.ShortComplex.Exact Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive	Finite AddCommGrpCat.carrier CategoryTheory.ShortComplex.X₂ Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive	—	Set.finite_range ab_range_eq_ker Finite.of_equiv AddSubgroup.instFiniteSubtypeMem AddMonoidHom.normal_ker Finite.of_addSubgroup_quotient
ab_range_eq_ker 📖	mathematical	CategoryTheory.ShortComplex.Exact Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive	AddMonoidHom.range AddCommGrpCat.carrier CategoryTheory.ShortComplex.X₁ Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive AddCommGroup.toAddGroup AddCommGrpCat.str CategoryTheory.ShortComplex.X₂ AddCommGrpCat.Hom.hom CategoryTheory.ShortComplex.f AddMonoidHom.ker CategoryTheory.ShortComplex.X₃ AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid CategoryTheory.ShortComplex.g	—	CategoryTheory.ShortComplex.ab_exact_iff_range_eq_ker

CategoryTheory.ShortComplex.ShortExact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ab_exact_iff_function_exact 📖	mathematical	—	CategoryTheory.ShortComplex.Exact Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive Function.Exact AddCommGrpCat.carrier CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ DFunLike.coe CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.g NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	CategoryTheory.ShortComplex.ab_exact_iff_function_exact
ab_finite_iff 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive	Finite AddCommGrpCat.carrier CategoryTheory.ShortComplex.X₂ Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₃	—	Finite.of_injective ab_injective_f Finite.of_surjective ab_surjective_g CategoryTheory.ShortComplex.Exact.ab_finite exact
ab_injective_f 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive	AddCommGrpCat.carrier CategoryTheory.ShortComplex.X₁ Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive CategoryTheory.ShortComplex.X₂ DFunLike.coe CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.ShortComplex.f	—	AddCommGrpCat.mono_iff_injective mono_f
ab_surjective_g 📖	mathematical	CategoryTheory.ShortComplex.ShortExact Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive	AddCommGrpCat.carrier CategoryTheory.ShortComplex.X₂ Ab AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive CategoryTheory.ShortComplex.X₃ DFunLike.coe CategoryTheory.ConcreteCategory.hom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier CategoryTheory.ShortComplex.g	—	AddCommGrpCat.epi_iff_surjective epi_g

(root)

Definitions

Name	Category	Theorems
Ab 📖	CompOp	130 math math: CategoryTheory.ShortComplex.ShortExact.ab_finite_iff, AlgebraicGeometry.Scheme.Modules.pushforward_obj_presheaf_map, PresheafOfModules.Sheafify.app_eq_of_isLocallyInjective, AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, AlgebraicGeometry.Scheme.Modules.pushforwardId_inv_app_app, CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul, PresheafOfModules.toPresheaf_preservesFiniteLimits, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_counit_app_app, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_hom_app_app, AlgebraicGeometry.Scheme.Modules.pushforward_obj_obj, CategoryTheory.ShortComplex.ShortExact.ab_surjective_g, AlgebraicGeometry.Scheme.Modules.instPreservesLimitsPresheafAbCarrierCommRingCatToPresheaf, PresheafOfModules.homEquivOfIsLocallyBijective_symm_apply, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app, PresheafOfModules.sections_property, PresheafOfModules.toSheafify_app_apply', AlgebraicGeometry.Scheme.Modules.Hom.zero_app, CategoryTheory.ShortComplex.ShortExact.d_eq_zero_of_f_eq_d_apply, CategoryTheory.ShortComplex.Exact.ab_finite, AlgebraicGeometry.Scheme.Modules.pushforwardComp_inv_app_app, PresheafOfModules.toPresheaf_map_toSheafify, PresheafOfModules.sectionsMap_coe, CategoryTheory.ShortComplex.abToCycles_apply_coe, PresheafOfModules.Sheafify.map_smul_eq, PresheafOfModules.instFaithfulFunctorOppositeAbToPresheaf, CategoryTheory.ShortComplex.Exact.ab_range_eq_ker, PresheafOfModules.toPresheaf_preservesLimit, PresheafOfModules.toPresheaf_obj_coe, SheafOfModules.isSheaf, AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_hom_app, CategoryTheory.ShortComplex.ShortExact.ab_injective_f, CategoryTheory.ShortComplex.abLeftHomologyData_π, AlgebraicGeometry.Scheme.Modules.toPresheaf_obj, AlgebraicGeometry.Scheme.Modules.instFaithfulPresheafAbCarrierCommRingCatToPresheaf, CategoryTheory.ShortComplex.exact_iff_surjective_abToCycles, CategoryTheory.ShortComplex.exact_iff_of_hasForget, CategoryTheory.ShortComplex.ab_exact_iff_function_exact, AlgebraicGeometry.Scheme.Modules.isSheaf, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_hom_app_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app, PresheafOfModules.presheaf_map_apply_coe, AlgebraicGeometry.Scheme.Modules.restrict_map, CategoryTheory.ShortComplex.i_cyclesMk, CategoryTheory.ShortComplex.abLeftHomologyData_K_coe, AlgebraicGeometry.Scheme.Modules.toPresheaf_map, PresheafOfModules.sheafification_map, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_inv_app_app, CategoryTheory.Preadditive.epi_iff_surjective, CategoryTheory.Preadditive.mono_iff_injective, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, HomologicalComplex.i_cyclesMk, AlgebraicGeometry.Scheme.Modules.restrictFunctorCongr_hom_app_app, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_inv_app_app, PresheafOfModules.unitHomEquiv_apply_coe, AlgebraicGeometry.Scheme.Modules.pushforwardComp_hom_app_app, PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms, AlgebraicGeometry.Scheme.Modules.mapPresheaf_app, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, CategoryTheory.ShortComplex.ShortExact.δ_apply', PresheafOfModules.freeAdjunctionUnit_app, PresheafOfModules.presheaf_obj_coe, AlgebraicGeometry.Scheme.Modules.Hom.id_app, PresheafOfModules.homMk_app, PresheafOfModules.isSheaf_of_isLimit, CategoryTheory.ShortComplex.ab_exact_iff_ker_le_range, AlgebraicGeometry.Scheme.Modules.Hom.isIso_iff_isIso_app, CategoryTheory.ShortComplex.abLeftHomologyData_f', AlgebraicGeometry.Scheme.Modules.Hom.comp_app, AlgebraicGeometry.isSheaf_fpqcTopology_continuousMapPresheafAb, PresheafOfModules.toPresheaf_map_app_apply, PresheafOfModules.instPreservesLimitsOfShapeFunctorOppositeAbToPresheaf, CategoryTheory.ShortComplex.ShortExact.injective_f, PresheafOfModules.instPreservesLimitsOfSizeFunctorOppositeAbToPresheaf, PresheafOfModules.Elements.fromFreeYoneda_app_apply, AlgebraicGeometry.Scheme.Modules.instIsIsoAbApp, CategoryTheory.ShortComplex.ab_exact_iff, CategoryTheory.ShortComplex.ShortExact.surjective_g, CategoryTheory.ShortComplex.zero_apply, AlgebraicGeometry.Scheme.Modules.Hom.sub_app, PresheafOfModules.ofPresheaf_obj_carrier, CategoryTheory.ShortComplex.abLeftHomologyData_i, PresheafOfModules.comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom, AlgebraicGeometry.Scheme.Modules.pushforwardId_hom_app_app, AlgebraicGeometry.Scheme.Modules.restrict_obj, PresheafOfModules.sectionsMk_coe, AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app, AlgebraicGeometry.Scheme.Modules.Hom.add_app, PresheafOfModules.Finite.toPresheaf_preservesFiniteColimits, PresheafOfModules.toPresheaf_preservesColimitsOfShape, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, CategoryTheory.ShortComplex.SnakeInput.δ_apply', CategoryTheory.ShortComplex.ShortExact.δ_apply, SheafOfModules.toSheaf_map_hom, CategoryTheory.ShortComplex.ab_zero_apply, CategoryTheory.Limits.IsColimit.ι_smul, PresheafOfModules.instIsLocalizationSheafOfModulesSheafificationInverseImageFunctorOppositeAbWToPresheaf, AlgebraicGeometry.Scheme.isZero_ellAdicSheaf_of_isEmpty, PresheafOfModules.toPresheaf_preservesColimit, PresheafOfModules.freeAdjunction_unit_app, CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul_aux, AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app, PresheafOfModules.toPresheaf_preservesColimitsOfSize, CategoryTheory.ShortComplex.ab_exact_iff_range_eq_ker, AlgebraicGeometry.Scheme.Modules.instReflectsIsomorphismsPresheafAbCarrierCommRingCatToPresheaf, PresheafOfModules.sections_ext_iff, PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app, AlgebraicGeometry.Scheme.instIsGrothendieckAbelianSheafProEtTopologyAb, PresheafOfModules.ofPresheaf_map, PresheafOfModules.germ_ringCat_smul, AlgebraicGeometry.Scheme.Modules.restrictFunctorId_hom_app_app, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, AlgebraicGeometry.Scheme.Modules.Hom.app_smul, SheafOfModules.pushforwardSections_coe, PresheafOfModules.fromFreeYonedaCoproduct_app_mk, PresheafOfModules.germ_smul, PresheafOfModules.toSheafify_app_apply, CategoryTheory.ShortComplex.abLeftHomologyData_H_coe, PresheafOfModules.freeAdjunction_homEquiv, PresheafOfModules.ofPresheaf_obj_isAddCommGroup, AlgebraicGeometry.Scheme.Modules.inv_app, PresheafOfModules.freeObjDesc_app, PresheafOfModules.instAdditiveFunctorOppositeAbToPresheaf, CategoryTheory.ShortComplex.exact_iff_exact_map_forget₂, PresheafOfModules.Sheafify.SMulCandidate.h, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, CategoryTheory.ShortComplex.ShortExact.ab_exact_iff_function_exact, CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier, AlgebraicGeometry.Scheme.Modules.map_smul, CategoryTheory.ShortComplex.abCyclesIso_inv_apply_iCycles, SheafOfModules.unitHomEquiv_apply_coe

---

← Back to Index