Flat

📁 Source: Mathlib/CategoryTheory/Functor/Flat.lean

Statistics

Metric	Count
Definitions `RepresentablyCoflat`, `RepresentablyFlat`, `lanEvaluationIsoColim`	3
Theorems `fac`, `uniq`, `comp`, `filtered`, `id`, `of_isLeftAdjoint`, `of_iso`, `cofiltered`, `comp`, `id`, `of_isRightAdjoint`, `of_iso`, `coflat_of_preservesFiniteColimits`, `final_of_representablyFlat`, `flat_iff_lan_flat`, `flat_of_preservesFiniteLimits`, `initial_of_representablyCoflat`, `instFinalStructuredArrowCompPreOfRepresentablyFlat`, `instInitialCostructuredArrowCompPreOfRepresentablyCoflat`, `instIsCofilteredElementsCompOfRepresentablyFlat`, `instIsCofilteredStructuredArrowCompOfRepresentablyFlat`, `instIsFilteredCostructuredArrowCompOfRepresentablyCoflat`, `instRepresentablyCoflatOppositeOpOfRepresentablyFlat`, `instRepresentablyFlatOppositeOpOfRepresentablyCoflat`, `lan_flat_of_flat`, `lan_preservesFiniteLimits_of_flat`, `lan_preservesFiniteLimits_of_preservesFiniteLimits`, `preservesFiniteColimits_iff_coflat`, `preservesFiniteColimits_of_coflat`, `preservesFiniteLimits_iff_flat`, `preservesFiniteLimits_iff_lan_preservesFiniteLimits`, `preservesFiniteLimits_of_flat`, `representablyCoflat_op_iff`, `representablyFlat_op_iff`	34
Total	37

CategoryTheory

Definitions

Name	Category	Theorems
`RepresentablyCoflat` 📖	CompData	10 math math: `representablyFlat_op_iff`, `RepresentablyCoflat.of_isLeftAdjoint`, `instRepresentablyCoflatOppositeOpOfRepresentablyFlat`, `RepresentablyCoflat.comp`, `preservesFiniteColimits_iff_coflat`, `RepresentablyCoflat.id`, `RepresentablyCoflat.of_iso`, `coflat_of_preservesFiniteColimits`, `instRepresentablyCoflatIndYoneda`, `representablyCoflat_op_iff`
`RepresentablyFlat` 📖	CompData	12 math math: `RepresentablyFlat.comp`, `RepresentablyFlat.of_isRightAdjoint`, `instRepresentablyFlatOppositeOpOfRepresentablyCoflat`, `representablyFlat_op_iff`, `RepresentablyFlat.of_iso`, `flat_iff_lan_flat`, `lan_flat_of_flat`, `RepresentablyFlat.id`, `preservesFiniteLimits_iff_flat`, `flat_of_preservesFiniteLimits`, `representablyCoflat_op_iff`, `instRepresentablyFlatOpensCarrierMap`
`lanEvaluationIsoColim` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coflat_of_preservesFiniteColimits` 📖	mathematical	—	`RepresentablyCoflat`	—	`Limits.preservesFiniteLimits_op` `representablyFlat_op_iff` `flat_of_preservesFiniteLimits` `Limits.hasFiniteLimits_opposite`
`final_of_representablyFlat` 📖	mathematical	—	`Functor.Final`	—	`IsCofiltered.isConnected` `RepresentablyFlat.cofiltered`
`flat_iff_lan_flat` 📖	mathematical	—	`RepresentablyFlat` `Functor` `Opposite` `Category.opposite` `types` `Functor.category` `Functor.lan` `Functor.op` `Functor.instHasLeftKanExtension` `Limits.Types.hasColimit` `CostructuredArrow` `instCategoryCostructuredArrow` `UnivLE.small` `UnivLE.self` `Functor.comp` `CostructuredArrow.proj`	—	`Functor.instHasLeftKanExtension` `Limits.Types.hasColimit` `UnivLE.small` `UnivLE.self` `lan_flat_of_flat` `Limits.Types.hasLimitsOfSize` `Limits.Types.hasColimitsOfSize` `Types.instReflectsLimitsOfSizeForgetTypeHom` `Limits.PreservesColimits.preservesFilteredColimits` `Types.instPreservesColimitsOfSizeForgetTypeHom` `Types.instPreservesLimitsOfSizeForgetTypeHom` `flat_of_preservesFiniteLimits` `Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize` `preservesLimit_of_lan_preservesLimit` `Limits.preservesLimitsOfShapeOfPreservesFiniteLimits` `preservesFiniteLimits_of_flat`
`flat_of_preservesFiniteLimits` 📖	mathematical	—	`RepresentablyFlat`	—	`IsCofiltered.of_hasFiniteLimits` `Limits.hasFiniteLimits_of_hasFiniteLimits_of_size` `StructuredArrow.hasLimit` `Limits.hasLimitOfHasLimitsOfShape` `Limits.hasLimitsOfShape_of_hasFiniteLimits` `preservesLimit_comp_of_createsLimit` `Limits.preservesLimitsOfShapeOfPreservesFiniteLimits` `Limits.PreservesLimitsOfShape.preservesLimit` `Limits.comp_preservesLimitsOfShape` `preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape`
`initial_of_representablyCoflat` 📖	mathematical	—	`Functor.Initial`	—	`IsFiltered.isConnected` `RepresentablyCoflat.filtered`
`instFinalStructuredArrowCompPreOfRepresentablyFlat` 📖	mathematical	—	`Functor.Final` `StructuredArrow` `Functor.comp` `instCategoryStructuredArrow` `StructuredArrow.pre`	—	`isConnected_of_equivalent` `IsCofiltered.isConnected` `RepresentablyFlat.cofiltered`
`instInitialCostructuredArrowCompPreOfRepresentablyCoflat` 📖	mathematical	—	`Functor.Initial` `CostructuredArrow` `Functor.comp` `instCategoryCostructuredArrow` `CostructuredArrow.pre`	—	`isConnected_of_equivalent` `IsFiltered.isConnected` `RepresentablyCoflat.filtered`
`instIsCofilteredElementsCompOfRepresentablyFlat` 📖	mathematical	—	`IsCofiltered` `Functor.Elements` `Functor.comp` `types` `categoryOfElements`	—	`IsCofiltered.of_equivalence` `instIsCofilteredStructuredArrowCompOfRepresentablyFlat`
`instIsCofilteredStructuredArrowCompOfRepresentablyFlat` 📖	mathematical	—	`IsCofiltered` `StructuredArrow` `Functor.comp` `instCategoryStructuredArrow`	—	`IsCofiltered.nonempty` `RepresentablyFlat.cofiltered` `IsCofiltered.toIsCofilteredOrEmpty` `Category.assoc` `StructuredArrow.w` `IsCofiltered.eq_condition` `StructuredArrow.hom_ext`
`instIsFilteredCostructuredArrowCompOfRepresentablyCoflat` 📖	mathematical	—	`IsFiltered` `CostructuredArrow` `Functor.comp` `instCategoryCostructuredArrow`	—	`isCofiltered_op_iff_isFiltered` `IsCofiltered.iff_of_equivalence` `instIsCofilteredStructuredArrowCompOfRepresentablyFlat` `instRepresentablyFlatOppositeOpOfRepresentablyCoflat`
`instRepresentablyCoflatOppositeOpOfRepresentablyFlat` 📖	mathematical	—	`RepresentablyCoflat` `Opposite` `Category.opposite` `Functor.op`	—	`representablyCoflat_op_iff`
`instRepresentablyFlatOppositeOpOfRepresentablyCoflat` 📖	mathematical	—	`RepresentablyFlat` `Opposite` `Category.opposite` `Functor.op`	—	`representablyFlat_op_iff`
`lan_flat_of_flat` 📖	mathematical	—	`RepresentablyFlat` `Functor` `Opposite` `Category.opposite` `Functor.category` `Functor.lan` `Functor.op` `Functor.instHasLeftKanExtension` `Limits.hasColimitOfHasColimitsOfShape` `CostructuredArrow` `instCategoryCostructuredArrow` `Limits.hasColimitsOfShapeOfHasColimitsOfSize` `Functor.comp` `CostructuredArrow.proj`	—	`flat_of_preservesFiniteLimits` `Limits.hasFiniteLimits_of_hasLimits` `Limits.functorCategoryHasLimitsOfSize` `Functor.instHasLeftKanExtension` `Limits.hasColimitOfHasColimitsOfShape` `Limits.hasColimitsOfShapeOfHasColimitsOfSize` `lan_preservesFiniteLimits_of_flat`
`lan_preservesFiniteLimits_of_flat` 📖	mathematical	—	`Limits.PreservesFiniteLimits` `Functor` `Opposite` `Category.opposite` `Functor.category` `Functor.lan` `Functor.op` `Functor.instHasLeftKanExtension` `Limits.hasColimitOfHasColimitsOfShape` `CostructuredArrow` `instCategoryCostructuredArrow` `Limits.hasColimitsOfShapeOfHasColimitsOfSize` `Functor.comp` `CostructuredArrow.proj`	—	`Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize` `Functor.instHasLeftKanExtension` `Limits.hasColimitOfHasColimitsOfShape` `Limits.hasColimitsOfShapeOfHasColimitsOfSize` `Limits.preservesLimitsOfShape_of_evaluation` `Limits.preservesLimitsOfShape_of_natIso` `Limits.comp_preservesLimitsOfShape` `whiskeringLeft_preservesLimitsOfShape` `Limits.hasLimitsOfShape_of_hasFiniteLimits` `Limits.hasFiniteLimits_of_hasLimits` `Limits.filtered_colim_preservesFiniteLimits` `UnivLE.small` `UnivLE.self` `IsFiltered.of_equivalence` `isFiltered_op_of_isCofiltered` `RepresentablyFlat.cofiltered` `Limits.reflectsLimitsOfShape_of_reflectsLimits` `Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits` `Limits.preservesLimitsOfShapeOfPreservesFiniteLimits` `Limits.PreservesLimits.preservesFiniteLimits`
`lan_preservesFiniteLimits_of_preservesFiniteLimits` 📖	mathematical	—	`Limits.PreservesFiniteLimits` `Functor` `Opposite` `Category.opposite` `Functor.category` `Functor.lan` `Functor.op` `Functor.instHasLeftKanExtension` `Limits.hasColimitOfHasColimitsOfShape` `CostructuredArrow` `instCategoryCostructuredArrow` `Limits.hasColimitsOfShapeOfHasColimitsOfSize` `Functor.comp` `CostructuredArrow.proj`	—	`Functor.instHasLeftKanExtension` `Limits.hasColimitOfHasColimitsOfShape` `Limits.hasColimitsOfShapeOfHasColimitsOfSize` `lan_preservesFiniteLimits_of_flat` `flat_of_preservesFiniteLimits`
`preservesFiniteColimits_iff_coflat` 📖	mathematical	—	`RepresentablyCoflat` `Limits.PreservesFiniteColimits`	—	`preservesFiniteColimits_of_coflat` `coflat_of_preservesFiniteColimits`
`preservesFiniteColimits_of_coflat` 📖	mathematical	—	`Limits.PreservesFiniteColimits`	—	`Limits.preservesFiniteColimits_of_op` `preservesFiniteLimits_of_flat` `instRepresentablyFlatOppositeOpOfRepresentablyCoflat`
`preservesFiniteLimits_iff_flat` 📖	mathematical	—	`RepresentablyFlat` `Limits.PreservesFiniteLimits`	—	`preservesFiniteLimits_of_flat` `flat_of_preservesFiniteLimits`
`preservesFiniteLimits_iff_lan_preservesFiniteLimits` 📖	mathematical	—	`Limits.PreservesFiniteLimits` `Functor` `Opposite` `Category.opposite` `types` `Functor.category` `Functor.lan` `Functor.op` `Functor.instHasLeftKanExtension` `Limits.Types.hasColimit` `CostructuredArrow` `instCategoryCostructuredArrow` `UnivLE.small` `UnivLE.self` `Functor.comp` `CostructuredArrow.proj`	—	`Functor.instHasLeftKanExtension` `Limits.Types.hasColimit` `UnivLE.small` `UnivLE.self` `lan_preservesFiniteLimits_of_preservesFiniteLimits` `Limits.Types.hasLimitsOfSize` `Limits.Types.hasColimitsOfSize` `Types.instReflectsLimitsOfSizeForgetTypeHom` `Limits.PreservesColimits.preservesFilteredColimits` `Types.instPreservesColimitsOfSizeForgetTypeHom` `Types.instPreservesLimitsOfSizeForgetTypeHom` `Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize` `preservesLimit_of_lan_preservesLimit` `Limits.preservesLimitsOfShapeOfPreservesFiniteLimits`
`preservesFiniteLimits_of_flat` 📖	mathematical	—	`Limits.PreservesFiniteLimits`	—	`Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize` `PreservesFiniteLimitsOfFlat.fac` `PreservesFiniteLimitsOfFlat.uniq`
`representablyCoflat_op_iff` 📖	mathematical	—	`RepresentablyCoflat` `Opposite` `Category.opposite` `Functor.op` `RepresentablyFlat`	—	`IsFiltered.of_equivalence` `RepresentablyCoflat.filtered` `isCofiltered_of_isFiltered_op` `IsCofiltered.of_equivalence` `isCofiltered_op_of_isFiltered` `isFiltered_op_of_isCofiltered` `RepresentablyFlat.cofiltered` `isFiltered_of_isCofiltered_op`
`representablyFlat_op_iff` 📖	mathematical	—	`RepresentablyFlat` `Opposite` `Category.opposite` `Functor.op` `RepresentablyCoflat`	—	`IsCofiltered.of_equivalence` `RepresentablyFlat.cofiltered` `isFiltered_of_isCofiltered_op` `IsFiltered.of_equivalence` `isFiltered_op_of_isCofiltered` `isCofiltered_op_of_isFiltered` `RepresentablyCoflat.filtered` `isCofiltered_of_isFiltered_op`

CategoryTheory.PreservesFiniteLimitsOfFlat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fac` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `lift` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Functor.mapCone` `CategoryTheory.Limits.Cone.π`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Limits.IsLimit.fac` `CategoryTheory.Category.comp_id` `CategoryTheory.StructuredArrow.w`
`uniq` 📖	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Functor.mapCone` `CategoryTheory.Limits.Cone.π`	—	—	`CategoryTheory.StructuredArrow.eqToHom_right` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.RepresentablyFlat.cofiltered` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Limits.Cone.w` `CategoryTheory.NatTrans.ext'` `CategoryTheory.Limits.IsLimit.uniq` `CategoryTheory.CommaMorphism.w`

CategoryTheory.RepresentablyCoflat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`CategoryTheory.RepresentablyCoflat` `CategoryTheory.Functor.comp`	—	`CategoryTheory.representablyFlat_op_iff` `CategoryTheory.RepresentablyFlat.comp` `CategoryTheory.instRepresentablyFlatOppositeOpOfRepresentablyCoflat`
`filtered` 📖	mathematical	—	`CategoryTheory.IsFiltered` `CategoryTheory.CostructuredArrow` `CategoryTheory.instCategoryCostructuredArrow`	—	—
`id` 📖	mathematical	—	`CategoryTheory.RepresentablyCoflat` `CategoryTheory.Functor.id`	—	`of_isLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Functor.isEquivalence_refl`
`of_isLeftAdjoint` 📖	mathematical	—	`CategoryTheory.RepresentablyCoflat`	—	`CategoryTheory.IsFiltered.of_isTerminal`
`of_iso` 📖	mathematical	—	`CategoryTheory.RepresentablyCoflat`	—	`CategoryTheory.IsFiltered.of_equivalence` `filtered`

CategoryTheory.RepresentablyFlat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cofiltered` 📖	mathematical	—	`CategoryTheory.IsCofiltered` `CategoryTheory.StructuredArrow` `CategoryTheory.instCategoryStructuredArrow`	—	—
`comp` 📖	mathematical	—	`CategoryTheory.RepresentablyFlat` `CategoryTheory.Functor.comp`	—	`CategoryTheory.IsCofiltered.of_cone_nonempty` `CategoryTheory.IsCofiltered.cone_nonempty` `cofiltered` `CategoryTheory.Limits.Cone.w` `CategoryTheory.Functor.map_id` `CategoryTheory.StructuredArrow.homMk.congr_simp` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.StructuredArrow.w` `CategoryTheory.Category.id_comp`
`id` 📖	mathematical	—	`CategoryTheory.RepresentablyFlat` `CategoryTheory.Functor.id`	—	`of_isRightAdjoint` `CategoryTheory.Functor.isRightAdjoint_of_isEquivalence` `CategoryTheory.Functor.isEquivalence_refl`
`of_isRightAdjoint` 📖	mathematical	—	`CategoryTheory.RepresentablyFlat`	—	`CategoryTheory.IsCofiltered.of_isInitial`
`of_iso` 📖	mathematical	—	`CategoryTheory.RepresentablyFlat`	—	`CategoryTheory.IsCofiltered.of_equivalence` `cofiltered`

---

← Back to Index