Documentation Verification Report

Tilde

📁 Source: Mathlib/AlgebraicGeometry/Modules/Tilde.lean

Statistics

Metric	Count
Definitions `fromTildeΓ`, `fromTildeΓNatTrans`, `SpecModulesToSheafFullyFaithful`, `moduleSpecΓFunctor`, `modulesSpecToSheaf`, `presentationTilde`, `tilde`, `adjunction`, `fullyFaithfulFunctor`, `functor`, `instModuleCarrierCarrierStalkAbPresheaf`, `isoTop`, `map`, `modulesSpecToSheafIso`, `toOpen`, `toStalk`, `toTildeΓNatIso`, `tildeFinsupp`, `tildeSelf`, `toOpen`, `toStalk`, `tilde`	22
Theorems `toOpen_fromTildeΓ_app`, `toOpen_fromTildeΓ_app_assoc`, `instAdditiveModuleCatCarrierModulesSpecOfFunctor`, `instFaithfulModuleCatCarrierModulesSpecOfFunctor`, `instFullModuleCatCarrierModulesSpecOfFunctor`, `instIsIsoFunctorModuleCatCarrierUnitModulesSpecOfAdjunction`, `instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat`, `instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf`, `instIsLeftAdjointModuleCatCarrierModulesSpecOfFunctor`, `instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde`, `isIso_fromTildeΓ_iff`, `functor_map`, `functor_obj`, `instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen`, `instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk`, `isIso_toOpen_top`, `isUnit_algebraMap_end_basicOpen`, `isoTop_hom`, `map_add`, `map_comp`, `map_comp_assoc`, `map_id`, `map_id_assoc`, `map_neg`, `map_sub`, `map_zero`, `toOpen_map_app`, `toOpen_map_app_assoc`, `toOpen_res`, `toOpen_res_assoc`, `toOpen_res`	31
Total	53

AlgebraicGeometry

Definitions

Name	Category	Theorems
`SpecModulesToSheafFullyFaithful` 📖	CompOp	—
`moduleSpecΓFunctor` 📖	CompOp	1 math math: `instIsIsoFunctorModuleCatCarrierUnitModulesSpecOfAdjunction`
`modulesSpecToSheaf` 📖	CompOp	14 math math: `Scheme.Modules.toOpen_fromTildeΓ_app`, `tilde.isoTop_hom`, `ModuleCat.Tilde.toOpen_res`, `Scheme.Modules.toOpen_fromTildeΓ_app_assoc`, `tilde.isIso_toOpen_top`, `instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf`, `tilde.toOpen_res`, `tilde.toOpen_res_assoc`, `tilde.isUnit_algebraMap_end_basicOpen`, `tilde.toOpen_map_app_assoc`, `isIso_fromTildeΓ_iff`, `instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat`, `tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen`, `tilde.toOpen_map_app`
`presentationTilde` 📖	CompOp	—
`tilde` 📖	CompOp	24 math math: `tilde.map_id`, `tilde.map_sub`, `Scheme.Modules.toOpen_fromTildeΓ_app`, `tilde.isoTop_hom`, `ModuleCat.Tilde.toOpen_res`, `tilde.map_comp_assoc`, `Scheme.Modules.toOpen_fromTildeΓ_app_assoc`, `tilde.isIso_toOpen_top`, `tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk`, `instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf`, `tilde.map_add`, `tilde.toOpen_res`, `tilde.toOpen_res_assoc`, `tilde.map_zero`, `tilde.functor_obj`, `tilde.toOpen_map_app_assoc`, `instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde`, `tilde.map_comp`, `tilde.map_neg`, `isIso_fromTildeΓ_iff`, `tilde.map_id_assoc`, `instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat`, `tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen`, `tilde.toOpen_map_app`
`tildeFinsupp` 📖	CompOp	—
`tildeSelf` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAdditiveModuleCatCarrierModulesSpecOfFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Additive` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `Scheme.Modules` `Spec` `CommRingCat.of` `ModuleCat.moduleCategory` `Scheme.Modules.instCategory` `ModuleCat.instPreadditive` `CategoryTheory.Abelian.toPreadditive` `Scheme.Modules.instAbelian` `tilde.functor`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_initial_object` `ModuleCat.instHasZeroObject` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits` `CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits` `CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint` `instIsLeftAdjointModuleCatCarrierModulesSpecOfFunctor` `CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryCoproducts` `CategoryTheory.Functor.additive_of_preservesBinaryBiproducts` `CategoryTheory.Abelian.hasBinaryBiproducts`
`instFaithfulModuleCatCarrierModulesSpecOfFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `ModuleCat.moduleCategory` `Scheme.Modules` `Spec` `CommRingCat.of` `Scheme.Modules.instCategory` `tilde.functor`	—	`CategoryTheory.Functor.FullyFaithful.faithful`
`instFullModuleCatCarrierModulesSpecOfFunctor` 📖	mathematical	—	`CategoryTheory.Functor.Full` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `ModuleCat.moduleCategory` `Scheme.Modules` `Spec` `CommRingCat.of` `Scheme.Modules.instCategory` `tilde.functor`	—	`CategoryTheory.Functor.FullyFaithful.full`
`instIsIsoFunctorModuleCatCarrierUnitModulesSpecOfAdjunction` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `ModuleCat.moduleCategory` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `Scheme.Modules` `Spec` `CommRingCat.of` `Scheme.Modules.instCategory` `tilde.functor` `moduleSpecΓFunctor` `CategoryTheory.Adjunction.unit` `tilde.adjunction`	—	`CategoryTheory.Iso.isIso_hom`
`instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat` 📖	mathematical	—	`CategoryTheory.IsIso` `Scheme.Modules` `Spec` `CommRingCat.of` `CommRingCat.carrier` `CommRingCat.commRing` `Scheme.Modules.instCategory` `tilde` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `TopCat.Sheaf.presheaf` `TopCat.Sheaf` `TopCat.instCategorySheaf` `modulesSpecToSheaf` `SheafOfModules.free` `Opens.grothendieckTopology` `Scheme.ringCatSheaf` `CategoryTheory.sheafToPresheaf_isRightAdjoint` `AddCommGrpCat` `AddCommGrpCat.instCategory` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `AddCommGrpCat.forget_preservesLimitsOfShape` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `UnivLE.small` `UnivLE.self` `AddCommGrpCat.hasLimit` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `small_subtype` `small_Pi` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.forget` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `AddCommGrpCat.hasColimitsOfShape` `CategoryTheory.GrothendieckTopology.Cover` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf` `CategoryTheory.GrothendieckTopology.Cover.instInhabited` `AddCommGrpCat.forget_reflects_isos` `CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.Functor.corepresentable_preservesLimit` `AddCommGrpCat.forget_isCorepresentable` `CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms` `AddCommGrpCat.forget_preservesLimits` `AddCommGrpCat.hasLimitsOfShape` `RingCat` `RingCat.instCategory` `CategoryTheory.forget₂` `RingHom` `RingCat.carrier` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingCat.ring` `RingHom.instFunLike` `RingCat.instConcreteCategoryRingHomCarrier` `RingCat.hasForgetToAddCommGrp` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `Opposite.op` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Scheme.Modules.fromTildeΓ`	—	`CategoryTheory.sheafToPresheaf_isRightAdjoint` `AddCommGrpCat.forget_preservesLimitsOfShape` `UnivLE.small` `UnivLE.self` `AddCommGrpCat.hasLimit` `small_subtype` `small_Pi` `AddCommGrpCat.hasColimitsOfShape` `Opposite.small` `CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `AddCommGrpCat.forget_reflects_isos` `CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.Functor.corepresentable_preservesLimit` `AddCommGrpCat.forget_isCorepresentable` `CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms` `AddCommGrpCat.forget_preservesLimits` `AddCommGrpCat.hasLimitsOfShape` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `RingCat.forget₂AddCommGroup_preservesLimitsOfSize` `univLE_of_max` `isIso_fromTildeΓ_iff`
`instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf` 📖	mathematical	—	`CategoryTheory.IsIso` `Scheme.Modules` `Spec` `CommRingCat.of` `CommRingCat.carrier` `CommRingCat.commRing` `Scheme.Modules.instCategory` `tilde` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `TopCat.Sheaf.presheaf` `TopCat.Sheaf` `TopCat.instCategorySheaf` `modulesSpecToSheaf` `SheafOfModules.unit` `Opens.grothendieckTopology` `Scheme.ringCatSheaf` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `RingCat` `RingCat.instCategory` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.forget₂` `RingHom` `RingCat.carrier` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingCat.ring` `RingHom.instFunLike` `RingCat.instConcreteCategoryRingHomCarrier` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `RingCat.hasForgetToAddCommGrp` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `Opposite.op` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Scheme.Modules.fromTildeΓ`	—	`CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `RingCat.forget₂AddCommGroup_preservesLimits` `isIso_fromTildeΓ_iff`
`instIsLeftAdjointModuleCatCarrierModulesSpecOfFunctor` 📖	mathematical	—	`CategoryTheory.Functor.IsLeftAdjoint` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `ModuleCat.moduleCategory` `Scheme.Modules` `Spec` `CommRingCat.of` `Scheme.Modules.instCategory` `tilde.functor`	—	`CategoryTheory.Adjunction.isLeftAdjoint`
`instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde` 📖	mathematical	—	`SheafOfModules.IsQuasicoherent` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Spec` `TopCat.str` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opens.grothendieckTopology` `Scheme.ringCatSheaf` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `RingCat` `RingCat.instCategory` `AddCommGrpCat` `AddCommGrpCat.instCategory` `CategoryTheory.GrothendieckTopology.over` `CategoryTheory.forget₂` `RingHom` `RingCat.carrier` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingCat.ring` `RingHom.instFunLike` `RingCat.instConcreteCategoryRingHomCarrier` `AddMonoidHom` `AddCommGrpCat.carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGrpCat.str` `AddMonoidHom.instFunLike` `AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier` `RingCat.hasForgetToAddCommGrp` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `CategoryTheory.sheafToPresheaf_isRightAdjoint` `AddCommGrpCat.forget_preservesLimitsOfShape` `UnivLE.small` `UnivLE.self` `AddCommGrpCat.hasLimit` `small_subtype` `small_Pi` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.forget` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `AddCommGrpCat.hasColimitsOfShape` `Opposite` `CategoryTheory.GrothendieckTopology.Cover` `CategoryTheory.Category.opposite` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf` `CategoryTheory.GrothendieckTopology.Cover.instInhabited` `AddCommGrpCat.forget_reflects_isos` `CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget` `CategoryTheory.Functor.corepresentable_preservesLimit` `AddCommGrpCat.forget_isCorepresentable` `CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms` `AddCommGrpCat.forget_preservesLimits` `AddCommGrpCat.hasLimitsOfShape` `tilde`	—	`SheafOfModules.Presentation.isQuasicoherent` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits` `CategoryTheory.Limits.CompleteLattice.hasFiniteLimits_of_semilatticeInf_orderTop` `Finite.of_fintype` `CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover` `AddCommGrpCat.hasLimit` `small_subtype` `small_Pi` `UnivLE.small` `UnivLE.self` `AddCommGrpCat.hasColimitsOfShape` `Opposite.small` `CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `AddCommGrpCat.FilteredColimits.forget_preservesFilteredColimits` `CategoryTheory.isFiltered_op_of_isCofiltered` `CategoryTheory.isCofiltered_of_directed_ge_nonempty` `SemilatticeInf.instIsCodirectedOrder` `AddCommGrpCat.forget_reflects_isos` `AddCommGrpCat.forget_preservesLimitsOfShape` `AddCommGrpCat.forget_preservesLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `AddCommGrpCat.hasLimits` `CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget` `CategoryTheory.sheafToPresheaf_isRightAdjoint` `CategoryTheory.hasSheafCompose_of_preservesMulticospan` `CategoryTheory.Functor.corepresentable_preservesLimit` `AddCommGrpCat.forget_isCorepresentable` `CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms` `AddCommGrpCat.hasLimitsOfShape` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape` `RingCat.forget₂AddCommGroup_preservesLimits` `Submodule.span_univ` `Submodule.span_eq`
`isIso_fromTildeΓ_iff` 📖	mathematical	—	`CategoryTheory.IsIso` `Scheme.Modules` `Spec` `CommRingCat.of` `CommRingCat.carrier` `CommRingCat.commRing` `Scheme.Modules.instCategory` `tilde` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `TopCat.Sheaf.presheaf` `TopCat.Sheaf` `TopCat.instCategorySheaf` `modulesSpecToSheaf` `Opposite.op` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Scheme.Modules.fromTildeΓ` `CategoryTheory.Functor.essImage` `tilde.functor`	—	`CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage` `instFaithfulModuleCatCarrierModulesSpecOfFunctor` `instFullModuleCatCarrierModulesSpecOfFunctor`

AlgebraicGeometry.Scheme.Modules

Definitions

Name	Category	Theorems
`fromTildeΓ` 📖	CompOp	5 math math: `toOpen_fromTildeΓ_app`, `toOpen_fromTildeΓ_app_assoc`, `AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf`, `AlgebraicGeometry.isIso_fromTildeΓ_iff`, `AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat`
`fromTildeΓNatTrans` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toOpen_fromTildeΓ_app` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRingCat.carrier` `CommRingCat.of` `CommRingCat.commRing` `CommRing.toRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Spec` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.Sheaf.presheaf` `AlgebraicGeometry.Scheme.Modules` `instCategory` `TopCat.Sheaf` `TopCat.instCategorySheaf` `AlgebraicGeometry.modulesSpecToSheaf` `Opposite.op` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `AlgebraicGeometry.tilde` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `AlgebraicGeometry.tilde.toOpen` `CategoryTheory.NatTrans.app` `CategoryTheory.Sheaf.Hom.val` `CategoryTheory.Functor.map` `fromTildeΓ` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.homOfLE` `le_top`	—	`le_top` `CategoryTheory.Functor.FullyFaithful.map_preimage` `TopCat.Sheaf.extend_hom_app` `ModuleCat.hom_ext` `LinearMap.ext` `IsLocalizedModule.lift_apply` `AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen` `smulCommClass_self` `IsScalarTower.left` `Submonoid.powers_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `PrimeSpectrum.basicOpen_one` `AlgebraicGeometry.tilde.toOpen_res` `CategoryTheory.Category.assoc` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Functor.map_comp` `CategoryTheory.op_comp` `LE.le.trans` `CategoryTheory.homOfLE_comp`
`toOpen_fromTildeΓ_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Spec` `CommRingCat.of` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.Sheaf.presheaf` `AlgebraicGeometry.Scheme.Modules` `instCategory` `TopCat.Sheaf` `TopCat.instCategorySheaf` `AlgebraicGeometry.modulesSpecToSheaf` `Opposite.op` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `AlgebraicGeometry.tilde` `AlgebraicGeometry.tilde.toOpen` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `CategoryTheory.NatTrans.app` `CategoryTheory.Sheaf.Hom.val` `CategoryTheory.Functor.map` `fromTildeΓ` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.homOfLE` `le_top`	—	`le_top` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `toOpen_fromTildeΓ_app`

AlgebraicGeometry.tilde

Definitions

Name	Category	Theorems
`adjunction` 📖	CompOp	1 math math: `AlgebraicGeometry.instIsIsoFunctorModuleCatCarrierUnitModulesSpecOfAdjunction`
`fullyFaithfulFunctor` 📖	CompOp	—
`functor` 📖	CompOp	8 math math: `AlgebraicGeometry.instIsLeftAdjointModuleCatCarrierModulesSpecOfFunctor`, `AlgebraicGeometry.instAdditiveModuleCatCarrierModulesSpecOfFunctor`, `AlgebraicGeometry.instFullModuleCatCarrierModulesSpecOfFunctor`, `functor_map`, `AlgebraicGeometry.instFaithfulModuleCatCarrierModulesSpecOfFunctor`, `functor_obj`, `AlgebraicGeometry.instIsIsoFunctorModuleCatCarrierUnitModulesSpecOfAdjunction`, `AlgebraicGeometry.isIso_fromTildeΓ_iff`
`instModuleCarrierCarrierStalkAbPresheaf` 📖	CompOp	1 math math: `instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk`
`isoTop` 📖	CompOp	1 math math: `isoTop_hom`
`map` 📖	CompOp	11 math math: `map_id`, `map_sub`, `functor_map`, `map_comp_assoc`, `map_add`, `map_zero`, `toOpen_map_app_assoc`, `map_comp`, `map_neg`, `map_id_assoc`, `toOpen_map_app`
`modulesSpecToSheafIso` 📖	CompOp	—
`toOpen` 📖	CompOp	10 math math: `AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app`, `isoTop_hom`, `ModuleCat.Tilde.toOpen_res`, `AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc`, `isIso_toOpen_top`, `toOpen_res`, `toOpen_res_assoc`, `toOpen_map_app_assoc`, `instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen`, `toOpen_map_app`
`toStalk` 📖	CompOp	1 math math: `instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk`
`toTildeΓNatIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`functor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `ModuleCat.moduleCategory` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Spec` `CommRingCat.of` `AlgebraicGeometry.Scheme.Modules.instCategory` `functor` `map`	—	—
`functor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `ModuleCat.moduleCategory` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Spec` `CommRingCat.of` `AlgebraicGeometry.Scheme.Modules.instCategory` `functor` `AlgebraicGeometry.tilde`	—	—
`instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen` 📖	mathematical	—	`IsLocalizedModule` `CommRingCat.carrier` `CommRing.toCommSemiring` `CommRingCat.commRing` `ModuleCat.carrier` `CommRing.toRing` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Spec` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `ModuleCat` `ModuleCat.moduleCategory` `TopCat.Sheaf.presheaf` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Scheme.Modules.instCategory` `TopCat.Sheaf` `TopCat.instCategorySheaf` `AlgebraicGeometry.modulesSpecToSheaf` `AlgebraicGeometry.tilde` `Opposite.op` `PrimeSpectrum.basicOpen` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ModuleCat.Hom.hom` `toOpen`	—	`IsLocalizedModule.of_linearEquiv` `RingHomInvPair.ids` `AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ`
`instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk` 📖	mathematical	—	`IsLocalizedModule` `CommRingCat.carrier` `CommRing.toCommSemiring` `CommRingCat.commRing` `ModuleCat.carrier` `CommRing.toRing` `ModuleCat.of` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `AddCommGrpCat.carrier` `TopCat.Presheaf.stalk` `Ab` `AddCommGrpCat.instCategory` `AddCommGrpCat.hasColimitsOfSize` `UnivLE.self` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.Modules.presheaf` `AlgebraicGeometry.tilde` `AddCommGrpCat.str` `instModuleCarrierCarrierStalkAbPresheaf` `AddCommGroup.toAddCommMonoid` `Ideal.primeCompl` `CommSemiring.toSemiring` `PrimeSpectrum.asIdeal` `PrimeSpectrum.isPrime` `ModuleCat.Hom.hom` `toStalk`	—	`AddCommGrpCat.hasColimitsOfSize` `UnivLE.self` `PrimeSpectrum.isPrime` `AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ`
`isIso_toOpen_top` 📖	mathematical	—	`CategoryTheory.IsIso` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `ModuleCat.moduleCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Spec` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.Sheaf.presheaf` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Scheme.Modules.instCategory` `TopCat.Sheaf` `TopCat.instCategorySheaf` `AlgebraicGeometry.modulesSpecToSheaf` `AlgebraicGeometry.tilde` `Opposite.op` `Top.top` `AlgebraicGeometry.Scheme.Opens` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `toOpen`	—	`toOpen.eq_1` `CategoryTheory.isIso_comp_right_iff` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.ConcreteCategory.isIso_iff_bijective` `ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier` `AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijective`
`isUnit_algebraMap_end_basicOpen` 📖	mathematical	—	`IsUnit` `Module.End` `CommRingCat.carrier` `ModuleCat.carrier` `CommRingCat.of` `CommRingCat.commRing` `CommRing.toRing` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Spec` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `ModuleCat` `ModuleCat.moduleCategory` `TopCat.Sheaf.presheaf` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Scheme.Modules.instCategory` `TopCat.Sheaf` `TopCat.instCategorySheaf` `AlgebraicGeometry.modulesSpecToSheaf` `Opposite.op` `PrimeSpectrum.basicOpen` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `Module.End.instMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Module.End.instSemiring` `RingHom.instFunLike` `algebraMap` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`smulCommClass_self` `IsScalarTower.left` `Module.End.isUnit_iff` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsLocalization.Away.algebraMap_isUnit` `AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen`
`isoTop_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `ModuleCat.moduleCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Spec` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.Sheaf.presheaf` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Scheme.Modules.instCategory` `TopCat.Sheaf` `TopCat.instCategorySheaf` `AlgebraicGeometry.modulesSpecToSheaf` `AlgebraicGeometry.tilde` `Opposite.op` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `isoTop` `toOpen` `AlgebraicGeometry.Scheme.Opens` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	—
`map_add` 📖	mathematical	—	`map` `Quiver.Hom` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `ModuleCat.instAddHom` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.Modules.instCategory` `AlgebraicGeometry.tilde` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.Abelian.toPreadditive` `AlgebraicGeometry.Scheme.Modules.instAbelian`	—	`CategoryTheory.Functor.map_add` `AlgebraicGeometry.instAdditiveModuleCatCarrierModulesSpecOfFunctor`
`map_comp` 📖	mathematical	—	`map` `CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.Modules.instCategory` `AlgebraicGeometry.tilde`	—	`AlgebraicGeometry.Scheme.Modules.hom_ext` `AddCommGrpCat.hom_ext` `AddMonoidHom.ext` `DFunLike.congr_fun` `PrimeSpectrum.isPrime` `IsScalarTower.left` `IsScalarTower.right` `smulCommClass_self` `localizedModuleIsLocalizedModule` `RingHomCompTriple.ids` `IsLocalizedModule.map_comp'`
`map_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Spec` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.Modules.instCategory` `AlgebraicGeometry.tilde` `map` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `ModuleCat.moduleCategory`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_comp`
`map_id` 📖	mathematical	—	`map` `CategoryTheory.CategoryStruct.id` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.Modules.instCategory` `AlgebraicGeometry.tilde`	—	`AlgebraicGeometry.Scheme.Modules.hom_ext` `AddCommGrpCat.hom_ext` `AddMonoidHom.ext` `DFunLike.congr_fun` `smulCommClass_self` `IsScalarTower.left` `IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `OreLocalization.instIsScalarTower_1` `LocalizedModule.map_id`
`map_id_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Spec` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.Modules.instCategory` `AlgebraicGeometry.tilde` `map` `CategoryTheory.CategoryStruct.id` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `ModuleCat.moduleCategory`	—	`CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_id`
`map_neg` 📖	mathematical	—	`map` `Quiver.Hom` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `ModuleCat.instNegHom` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.Modules.instCategory` `AlgebraicGeometry.tilde` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.Abelian.toPreadditive` `AlgebraicGeometry.Scheme.Modules.instAbelian`	—	`CategoryTheory.Functor.map_neg` `AlgebraicGeometry.instAdditiveModuleCatCarrierModulesSpecOfFunctor`
`map_sub` 📖	mathematical	—	`map` `Quiver.Hom` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `ModuleCat.instSubHom` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.Modules.instCategory` `AlgebraicGeometry.tilde` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.Abelian.toPreadditive` `AlgebraicGeometry.Scheme.Modules.instAbelian`	—	`CategoryTheory.Functor.map_sub` `AlgebraicGeometry.instAdditiveModuleCatCarrierModulesSpecOfFunctor`
`map_zero` 📖	mathematical	—	`map` `Quiver.Hom` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `ModuleCat.instZeroHom` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.Modules.instCategory` `AlgebraicGeometry.tilde` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AlgebraicGeometry.Scheme.Modules.instAbelian`	—	`CategoryTheory.Functor.map_zero` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `AlgebraicGeometry.instAdditiveModuleCatCarrierModulesSpecOfFunctor`
`toOpen_map_app` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Spec` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.Sheaf.presheaf` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Scheme.Modules.instCategory` `TopCat.Sheaf` `TopCat.instCategorySheaf` `AlgebraicGeometry.modulesSpecToSheaf` `AlgebraicGeometry.tilde` `Opposite.op` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `toOpen` `CategoryTheory.NatTrans.app` `CategoryTheory.Sheaf.Hom.val` `CategoryTheory.Functor.map` `map`	—	`ModuleCat.hom_ext` `LinearMap.ext` `IsLocalizedModule.map_apply` `PrimeSpectrum.isPrime` `IsScalarTower.left` `IsScalarTower.right` `localizedModuleIsLocalizedModule`
`toOpen_map_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Spec` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.Sheaf.presheaf` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Scheme.Modules.instCategory` `TopCat.Sheaf` `TopCat.instCategorySheaf` `AlgebraicGeometry.modulesSpecToSheaf` `AlgebraicGeometry.tilde` `Opposite.op` `toOpen` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `CategoryTheory.NatTrans.app` `CategoryTheory.Sheaf.Hom.val` `CategoryTheory.Functor.map` `map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `toOpen_map_app`
`toOpen_res` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Spec` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.Sheaf.presheaf` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Scheme.Modules.instCategory` `TopCat.Sheaf` `TopCat.instCategorySheaf` `AlgebraicGeometry.modulesSpecToSheaf` `AlgebraicGeometry.tilde` `Opposite.op` `AlgebraicGeometry.PrimeSpectrum.Top` `toOpen` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	—
`toOpen_res_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Spec` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.Sheaf.presheaf` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Scheme.Modules.instCategory` `TopCat.Sheaf` `TopCat.instCategorySheaf` `AlgebraicGeometry.modulesSpecToSheaf` `AlgebraicGeometry.tilde` `Opposite.op` `toOpen` `AlgebraicGeometry.PrimeSpectrum.Top` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `toOpen_res`

ModuleCat

Definitions

Name	Category	Theorems
`tilde` 📖	CompOp	—

ModuleCat.Tilde

Definitions

Name	Category	Theorems
`toOpen` 📖	CompOp	—
`toStalk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toOpen_res` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `ModuleCat` `CommRingCat.carrier` `CommRing.toRing` `CommRingCat.commRing` `CategoryTheory.Category.toCategoryStruct` `ModuleCat.moduleCategory` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Spec` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.Sheaf.presheaf` `AlgebraicGeometry.Scheme.Modules` `AlgebraicGeometry.Scheme.Modules.instCategory` `TopCat.Sheaf` `TopCat.instCategorySheaf` `AlgebraicGeometry.modulesSpecToSheaf` `AlgebraicGeometry.tilde` `Opposite.op` `AlgebraicGeometry.PrimeSpectrum.Top` `AlgebraicGeometry.tilde.toOpen` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver`	—	`AlgebraicGeometry.tilde.toOpen_res`

---

← Back to Index