FinitePresentation

📁 Source: Mathlib/Algebra/Category/Ring/FinitePresentation.lean

Statistics

Metric	Count
Definitions	0
Theorems isFinitelyPresentable_hom, isFinitelyPresentable_under, preservesColimit_coyoneda_of_finitePresentation, preservesFilteredColimits_coyoneda, exists_comp_map_eq_of_isColimit, exists_eq_comp_ι_app_of_isColimit, isFinitelyPresentable, preservesColimit_coyoneda_of_finitePresentation, preservesFilteredColimits_coyoneda	9
Total	9

CommRingCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFinitelyPresentable_hom 📖	mathematical	—	CategoryTheory.MorphismProperty.isFinitelyPresentable CommRingCat instCategory	—	isFinitelyPresentable_under
isFinitelyPresentable_under 📖	mathematical	—	CategoryTheory.IsFinitelyPresentable CategoryTheory.Under CommRingCat instCategory CategoryTheory.instCategoryUnder	—	CategoryTheory.isFinitelyPresentable_iff_preservesFilteredColimits preservesFilteredColimits_coyoneda
preservesColimit_coyoneda_of_finitePresentation 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Under CommRingCat instCategory CategoryTheory.instCategoryUnder CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op	—	CategoryTheory.Category.id_comp CategoryTheory.Under.w RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit CategoryTheory.Limits.PreservesColimit.preserves CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.Limits.instPreservesFilteredColimitsOfSizeUnderForget CategoryTheory.Under.UnderMorphism.ext RingHom.EssFiniteType.exists_comp_map_eq_of_isColimit RingHom.FiniteType.essFiniteType RingHom.FiniteType.of_finitePresentation
preservesFilteredColimits_coyoneda 📖	mathematical	—	CategoryTheory.Limits.PreservesFilteredColimits CategoryTheory.Under CommRingCat instCategory CategoryTheory.instCategoryUnder CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op	—	preservesColimit_coyoneda_of_finitePresentation CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits FilteredColimits.forget_preservesFilteredColimits

RingHom.EssFiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_comp_map_eq_of_isColimit 📖	mathematical	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι	CategoryTheory.Functor.map	—	CategoryTheory.IsFiltered.cocone_nonempty CommRingCat.hom_ext ext CommRingCat.hom_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.NatTrans.naturality CategoryTheory.Category.id_comp CategoryTheory.Limits.Cocone.w CategoryTheory.Functor.map_comp CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff CategoryTheory.IsFiltered.toIsFilteredOrEmpty
exists_eq_comp_ι_app_of_isColimit 📖	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	—	RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass CommRingCat.hom_ext AlgHom.comp_algebraMap CategoryTheory.IsFiltered.sup_objs_exists MvPolynomial.ringHom_ext MvPolynomial.eval₂_C CategoryTheory.Category.assoc MvPolynomial.eval₂_X CategoryTheory.Limits.Cocone.w RingHom.ext CategoryTheory.Limits.Types.jointly_surjective_of_isColimit CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff CategoryTheory.IsFiltered.toIsFilteredOrEmpty Eq.le Ideal.subset_span map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass CategoryTheory.IsFiltered.cocone_nonempty Ideal.span_le RingHom.ker.congr_simp CategoryTheory.Functor.map_comp CategoryTheory.NatTrans.naturality CategoryTheory.Category.id_comp RingHom.liftOfRightInverse_comp_apply

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFinitelyPresentable 📖	mathematical	—	CategoryTheory.IsFinitelyPresentable CategoryTheory.Under CommRingCat CommRingCat.instCategory CategoryTheory.instCategoryUnder	—	CommRingCat.isFinitelyPresentable_under
preservesColimit_coyoneda_of_finitePresentation 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit CategoryTheory.Under CommRingCat CommRingCat.instCategory CategoryTheory.instCategoryUnder CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op	—	CommRingCat.preservesColimit_coyoneda_of_finitePresentation
preservesFilteredColimits_coyoneda 📖	mathematical	—	CategoryTheory.Limits.PreservesFilteredColimits CategoryTheory.Under CommRingCat CommRingCat.instCategory CategoryTheory.instCategoryUnder CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda Opposite.op	—	CommRingCat.preservesFilteredColimits_coyoneda

---

← Back to Index