PullbackFree

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

Statistics

Metric	Count
Definitions freeFunctorCompPullbackIso, pullbackObjFreeIso, pullbackObjUnitToUnit, pushforwardSections, unitToPushforwardObjUnit	5
Theorems bijective_pushforwardSections, instIsIsoPullbackObjUnitToUnitOfFinal, pullbackObjFreeIso_hom_naturality, pullbackObjFreeIso_hom_naturality_assoc, pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit, pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit, pullback_map_ιFree_comp_pullbackObjFreeIso_hom, pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc, pushforwardSections_coe, pushforwardSections_unitHomEquiv, unitToPushforwardObjUnit_val_app_apply	11
Total	16

SheafOfModules

Definitions

Name	Category	Theorems
freeFunctorCompPullbackIso 📖	CompOp	—
pullbackObjFreeIso 📖	CompOp	4 math math: pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc, pullbackObjFreeIso_hom_naturality_assoc, pullbackObjFreeIso_hom_naturality, pullback_map_ιFree_comp_pullbackObjFreeIso_hom
pullbackObjUnitToUnit 📖	CompOp	5 math math: pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit, pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc, instIsIsoPullbackObjUnitToUnitOfFinal, pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit, pullback_map_ιFree_comp_pullbackObjFreeIso_hom
pushforwardSections 📖	CompOp	3 math math: bijective_pushforwardSections, pushforwardSections_coe, pushforwardSections_unitHomEquiv
unitToPushforwardObjUnit 📖	CompOp	4 math math: pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit, unitToPushforwardObjUnit_val_app_apply, pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit, pushforwardSections_unitHomEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_pushforwardSections 📖	mathematical	—	Function.Bijective sections CategoryTheory.Functor.obj SheafOfModules instCategory pushforward pushforwardSections	—	CategoryTheory.Functor.bijective_sectionsPrecomp CategoryTheory.Functor.initial_op_of_final
instIsIsoPullbackObjUnitToUnitOfFinal 📖	mathematical	—	CategoryTheory.IsIso SheafOfModules instCategory CategoryTheory.Functor.obj pullback unit pullbackObjUnitToUnit	—	CategoryTheory.isIso_iff_coyoneda_map_bijective Function.Bijective.of_comp_iff' Equiv.bijective pushforwardSections_unitHomEquiv EmbeddingLike.apply_eq_iff_eq EquivLike.toEmbeddingLike CategoryTheory.Adjunction.homEquiv_naturality_right pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit Function.Bijective.comp bijective_pushforwardSections
pullbackObjFreeIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj pullback free CategoryTheory.Functor.map freeMap CategoryTheory.Iso.hom pullbackObjFreeIso	—	CategoryTheory.Limits.Cofan.IsColimit.hom_ext CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint instIsLeftAdjointPullback ιFree_freeMap pullback_map_ιFree_comp_pullbackObjFreeIso_hom pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc
pullbackObjFreeIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj pullback free CategoryTheory.Functor.map freeMap CategoryTheory.Iso.hom pullbackObjFreeIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullbackObjFreeIso_hom_naturality
pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj pullback unit pushforward EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv pullbackPushforwardAdjunction pullbackObjUnitToUnit unitToPushforwardObjUnit	—	Equiv.apply_symm_apply
pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory unit CategoryTheory.Functor.obj pushforward pullback EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv pullbackPushforwardAdjunction unitToPushforwardObjUnit pullbackObjUnitToUnit	—	—
pullback_map_ιFree_comp_pullbackObjFreeIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj pullback unit free CategoryTheory.Functor.map ιFree CategoryTheory.Iso.hom pullbackObjFreeIso pullbackObjUnitToUnit	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instIsIsoPullbackObjUnitToUnitOfFinal CategoryTheory.Limits.map_ι_comp_inv_sigmaComparison_assoc CategoryTheory.Limits.ι_colimMap
pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SheafOfModules CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor.obj pullback unit free CategoryTheory.Functor.map ιFree CategoryTheory.Iso.hom pullbackObjFreeIso pullbackObjUnitToUnit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pullback_map_ιFree_comp_pullbackObjFreeIso_hom
pushforwardSections_coe 📖	mathematical	—	Set Set.instMembership CategoryTheory.Functor.sections Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp Ab AddCommGrpCat.instCategory CategoryTheory.types PresheafOfModules.presheaf CategoryTheory.Sheaf.val RingCat RingCat.instCategory val CategoryTheory.Functor.obj SheafOfModules instCategory pushforward CategoryTheory.forget AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier pushforwardSections CategoryTheory.Functor.op	—	—
pushforwardSections_unitHomEquiv 📖	mathematical	—	pushforwardSections DFunLike.coe Equiv Quiver.Hom SheafOfModules CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory unit sections EquivLike.toFunLike Equiv.instEquivLike unitHomEquiv CategoryTheory.Functor.obj pushforward CategoryTheory.CategoryStruct.comp unitToPushforwardObjUnit CategoryTheory.Functor.map	—	PresheafOfModules.sections_ext unitToPushforwardObjUnit_val_app_apply RingHomCompTriple.ids PresheafOfModules.comp_app map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
unitToPushforwardObjUnit_val_app_apply 📖	mathematical	—	DFunLike.coe PresheafOfModules.obj CategoryTheory.Sheaf.val RingCat RingCat.instCategory val unit CategoryTheory.Functor.obj SheafOfModules instCategory pushforward ModuleCat.carrier RingCat.carrier Opposite CategoryTheory.Category.opposite RingCat.ring CategoryTheory.ConcreteCategory.hom ModuleCat ModuleCat.moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier PresheafOfModules.Hom.app Hom.val unitToPushforwardObjUnit CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous RingHom RingHom.instFunLike RingCat.instConcreteCategoryRingHomCarrier CategoryTheory.NatTrans.app CategoryTheory.Sheaf.Hom.val	—	—

---

← Back to Index