Free

📁 Source: Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean

Statistics

Metric	Count
Definitions free, freeCofan, freeFunctor, freeHomEquiv, freeMap, freeSection, freeSumIso, isColimitFreeCofan, mapFree, ιFree	10
Theorems freeCofan_inj, freeFunctor_map, freeFunctor_obj, freeHomEquiv_apply, freeHomEquiv_comp_apply, freeHomEquiv_freeMap, freeHomEquiv_symm_comp, inl_freeSumIso_hom, inl_freeSumIso_hom_assoc, inr_freeSumIso_hom, inr_freeSumIso_hom_assoc, instPreservesColimitsOfSizeFreeFunctor, map_ιFree_mapFree_hom, map_ιFree_mapFree_hom_assoc, sectionMap_freeMap_freeSection, sectionsMap_freeHomEquiv_symm_freeSection, unitHomEquiv_symm_freeHomEquiv_apply, ιFree_freeMap, ιFree_freeMap_assoc, ιFree_mapFree_inv, ιFree_mapFree_inv_assoc	21
Total	31

SheafOfModules

Definitions

Name	Category	Theorems
free 📖	CompOp	34 math math: inl_freeSumIso_hom, freeHomEquiv_freeMap, inr_freeSumIso_hom, unitHomEquiv_symm_freeHomEquiv_apply, GeneratingSections.epi, ιFree_mapFree_inv_assoc, pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc, freeHomEquiv_symm_comp, sectionMap_freeMap_freeSection, pullbackObjFreeIso_hom_naturality_assoc, freeHomEquiv_comp_apply, ιFree_freeMap, freeFunctor_obj, inl_freeSumIso_hom_assoc, ιFree_freeMap_assoc, inr_freeSumIso_hom_assoc, Presentation.map_relations_I, freeHomEquiv_apply, ιFree_mapFree_inv, Presentation.mapRelations_mapGenerators, relationsOfIsCokernelFree_I, Presentation.of_isIso_relations, Presentation.mapRelations_mapGenerators_assoc, GeneratingSections.ofEpi_π, map_ιFree_mapFree_hom, relationsOfIsCokernelFree_s, pullbackObjFreeIso_hom_naturality, pullback_map_ιFree_comp_pullbackObjFreeIso_hom, map_ιFree_mapFree_hom_assoc, Presentation.IsFinite.finite_relations, sectionsMap_freeHomEquiv_symm_freeSection, generatorsOfIsCokernelFree_s, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, Presentation.map_π_eq
freeCofan 📖	CompOp	1 math math: freeCofan_inj
freeFunctor 📖	CompOp	3 math math: instPreservesColimitsOfSizeFreeFunctor, freeFunctor_obj, freeFunctor_map
freeHomEquiv 📖	CompOp	10 math math: freeHomEquiv_freeMap, unitHomEquiv_symm_freeHomEquiv_apply, GeneratingSections.epi, freeHomEquiv_symm_comp, freeHomEquiv_comp_apply, Presentation.map_relations_I, freeHomEquiv_apply, relationsOfIsCokernelFree_s, sectionsMap_freeHomEquiv_symm_freeSection, generatorsOfIsCokernelFree_s
freeMap 📖	CompOp	11 math math: inl_freeSumIso_hom, freeHomEquiv_freeMap, inr_freeSumIso_hom, sectionMap_freeMap_freeSection, pullbackObjFreeIso_hom_naturality_assoc, ιFree_freeMap, freeFunctor_map, inl_freeSumIso_hom_assoc, ιFree_freeMap_assoc, inr_freeSumIso_hom_assoc, pullbackObjFreeIso_hom_naturality
freeSection 📖	CompOp	4 math math: freeHomEquiv_freeMap, sectionMap_freeMap_freeSection, freeHomEquiv_apply, sectionsMap_freeHomEquiv_symm_freeSection
freeSumIso 📖	CompOp	4 math math: inl_freeSumIso_hom, inr_freeSumIso_hom, inl_freeSumIso_hom_assoc, inr_freeSumIso_hom_assoc
isColimitFreeCofan 📖	CompOp	—
mapFree 📖	CompOp	6 math math: ιFree_mapFree_inv_assoc, Presentation.map_relations_I, ιFree_mapFree_inv, map_ιFree_mapFree_hom, map_ιFree_mapFree_hom_assoc, Presentation.map_π_eq
ιFree 📖	CompOp	10 math math: unitHomEquiv_symm_freeHomEquiv_apply, ιFree_mapFree_inv_assoc, pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc, ιFree_freeMap, ιFree_freeMap_assoc, ιFree_mapFree_inv, map_ιFree_mapFree_hom, pullback_map_ιFree_comp_pullbackObjFreeIso_hom, map_ιFree_mapFree_hom_assoc, freeCofan_inj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
freeCofan_inj 📖	mathematical	—	SheafOfModules instCategory unit freeCofan ιFree	—	—
freeFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.types SheafOfModules instCategory freeFunctor freeMap	—	—
freeFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types SheafOfModules instCategory freeFunctor free	—	—
freeHomEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory free EquivLike.toFunLike Equiv.instEquivLike freeHomEquiv sectionsMap freeSection	—	—
freeHomEquiv_comp_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory free EquivLike.toFunLike Equiv.instEquivLike freeHomEquiv CategoryTheory.CategoryStruct.comp sectionsMap	—	—
freeHomEquiv_freeMap 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory free EquivLike.toFunLike Equiv.instEquivLike freeHomEquiv freeMap sections freeSection	—	Equiv.injective Equiv.symm_apply_apply
freeHomEquiv_symm_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory free DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm freeHomEquiv sectionsMap	—	Equiv.injective PresheafOfModules.sections_ext Equiv.apply_symm_apply
inl_freeSumIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory free CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀ instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf PresheafOfModules.hasColimitsOfSize CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf AddCommGrpCat.hasColimitsOfSize univLE_of_max UnivLE.self Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.coprod.inl CategoryTheory.Iso.hom freeSumIso freeMap	—	CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀ instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf PresheafOfModules.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize univLE_of_max UnivLE.self Finite.of_fintype
inl_freeSumIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory free CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀ instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf PresheafOfModules.hasColimitsOfSize CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf AddCommGrpCat.hasColimitsOfSize univLE_of_max UnivLE.self Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.coprod.inl CategoryTheory.Iso.hom freeSumIso freeMap	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀ instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf PresheafOfModules.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize univLE_of_max UnivLE.self Finite.of_fintype CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_freeSumIso_hom
inr_freeSumIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory free CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀ instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf PresheafOfModules.hasColimitsOfSize CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf AddCommGrpCat.hasColimitsOfSize univLE_of_max UnivLE.self Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.coprod.inr CategoryTheory.Iso.hom freeSumIso freeMap	—	CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀ instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf PresheafOfModules.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize univLE_of_max UnivLE.self Finite.of_fintype
inr_freeSumIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory free CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀ instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf PresheafOfModules.hasColimitsOfSize CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite RingCat RingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf AddCommGrpCat.hasColimitsOfSize univLE_of_max UnivLE.self Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.coprod.inr CategoryTheory.Iso.hom freeSumIso freeMap	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀ instHasColimitsOfSizeOfPresheafOfModulesObjFunctorOppositeRingCatIsSheaf PresheafOfModules.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize univLE_of_max UnivLE.self Finite.of_fintype CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_freeSumIso_hom
instPreservesColimitsOfSizeFreeFunctor 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.types SheafOfModules instCategory freeFunctor	—	CategoryTheory.Limits.Types.isColimit_iff_coconeTypesIsColimit CategoryTheory.Limits.Cocone.w freeHomEquiv_comp_apply freeHomEquiv_freeMap freeHomEquiv_apply Equiv.injective sectionsMap_freeHomEquiv_symm_freeSection CategoryTheory.Functor.CoconeTypes.IsColimit.fac_apply CategoryTheory.Functor.CoconeTypes.IsColimit.ι_jointly_surjective Equiv.congr_arg CategoryTheory.Functor.coconeTypesEquiv_symm_apply_ι
map_ιFree_mapFree_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj unit free CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.map ιFree CategoryTheory.Iso.hom mapFree	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id_assoc
map_ιFree_mapFree_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj unit free CategoryTheory.Functor.map ιFree CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Iso.hom mapFree	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_ιFree_mapFree_hom
sectionMap_freeMap_freeSection 📖	mathematical	—	sectionsMap free freeMap freeSection	—	CategoryTheory.Category.id_comp freeHomEquiv_freeMap
sectionsMap_freeHomEquiv_symm_freeSection 📖	mathematical	—	sectionsMap free DFunLike.coe Equiv Quiver.Hom SheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory EquivLike.toFunLike Equiv.instEquivLike Equiv.symm freeHomEquiv freeSection	—	Equiv.surjective Equiv.symm_apply_apply
unitHomEquiv_symm_freeHomEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv sections Quiver.Hom SheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory unit EquivLike.toFunLike Equiv.instEquivLike Equiv.symm unitHomEquiv free freeHomEquiv CategoryTheory.CategoryStruct.comp ιFree	—	Equiv.symm_apply_apply
ιFree_freeMap 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory unit free ιFree freeMap	—	unitHomEquiv_symm_freeHomEquiv_apply freeHomEquiv_freeMap CategoryTheory.Category.comp_id
ιFree_freeMap_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory unit free ιFree freeMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιFree_freeMap
ιFree_mapFree_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory unit free CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Functor.obj ιFree CategoryTheory.Iso.inv mapFree CategoryTheory.Functor.map	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.Limits.IsColimit.fac CategoryTheory.Category.assoc CategoryTheory.Equivalence.invFunIdAssoc_inv_app CategoryTheory.Discrete.functor_map_id CategoryTheory.Category.id_comp
ιFree_mapFree_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory unit free CategoryTheory.instHasWeakSheafifyOfHasSheafify AddCommGrpCat AddCommGrpCat.instCategory ιFree CategoryTheory.Functor.obj CategoryTheory.Iso.inv mapFree CategoryTheory.Functor.map	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιFree_mapFree_inv

---

← Back to Index