Documentation Verification Report

TopCatAdjunction

📁 Source: Mathlib/Condensed/TopCatAdjunction.lean

Statistics

Metric	Count
Definitions `compactlyGeneratedAdjunction`, `compactlyGeneratedAdjunctionCounitHomeo`, `compactlyGeneratedAdjunctionCounitIso`, `compactlyGeneratedToCondensedSet`, `condensedSetToCompactlyGenerated`, `fullyFaithfulCompactlyGeneratedToCondensedSet`, `toTopCat`, `toTopCatMap`, `topCatAdjunction`, `topCatAdjunctionCounit`, `topCatAdjunctionCounitEquiv`, `topCatAdjunctionUnit`, `condensedSetToTopCat`, `instTopologicalSpaceObjOppositeCompHausObjFunctorTypeIsSheafCoherentTopologyOpOfPUnit`	14
Theorems `continuous_coinducingCoprod`, `instEpiTopCatAppCounitTopCatAdjunction`, `instFaithfulTopCatTopCatToCondensedSet`, `instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction`, `instUCompactlyGeneratedSpaceCarrierObjTopCatCondensedSetToTopCat`, `instUCompactlyGeneratedSpaceCarrierToTopCat`, `toTopCatMap_hom_apply`, `topCatAdjunctionCounit_bijective`, `topCatAdjunctionCounit_hom_apply`, `topCatAdjunctionUnit_hom_app`, `topCatAdjunctionUnit_hom_app_apply`, `condensedSetToTopCat_map`, `condensedSetToTopCat_obj_carrier`	13
Total	27

CondensedSet

Definitions

Name	Category	Theorems
`compactlyGeneratedAdjunction` 📖	CompOp	1 math math: `instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction`
`compactlyGeneratedAdjunctionCounitHomeo` 📖	CompOp	—
`compactlyGeneratedAdjunctionCounitIso` 📖	CompOp	—
`compactlyGeneratedToCondensedSet` 📖	CompOp	1 math math: `instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction`
`condensedSetToCompactlyGenerated` 📖	CompOp	1 math math: `instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction`
`fullyFaithfulCompactlyGeneratedToCondensedSet` 📖	CompOp	—
`toTopCat` 📖	CompOp	6 math math: `instUCompactlyGeneratedSpaceCarrierToTopCat`, `topCatAdjunctionUnit_hom_app_apply`, `topCatAdjunctionCounit_bijective`, `topCatAdjunctionCounit_hom_apply`, `toTopCatMap_hom_apply`, `topCatAdjunctionUnit_hom_app`
`toTopCatMap` 📖	CompOp	2 math math: `condensedSetToTopCat_map`, `toTopCatMap_hom_apply`
`topCatAdjunction` 📖	CompOp	1 math math: `instEpiTopCatAppCounitTopCatAdjunction`
`topCatAdjunctionCounit` 📖	CompOp	2 math math: `topCatAdjunctionCounit_bijective`, `topCatAdjunctionCounit_hom_apply`
`topCatAdjunctionCounitEquiv` 📖	CompOp	—
`topCatAdjunctionUnit` 📖	CompOp	2 math math: `topCatAdjunctionUnit_hom_app_apply`, `topCatAdjunctionUnit_hom_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_coinducingCoprod` 📖	mathematical	—	`Continuous` `TopCat.carrier` `CompHausLike.toTop` `CompHaus` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.coherentTopology` `Opposite.op` `CompHaus.of` `instTopologicalSpacePUnit` `instCompactSpace` `instIndiscreteTopologyPUnit` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `instMetricSpacePUnit` `TopCat.str` `instTopologicalSpaceObjOppositeCompHausObjFunctorTypeIsSheafCoherentTopologyOpOfPUnit`	—	`instCompactSpace` `instIndiscreteTopologyPUnit` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `continuous_sigma_iff` `continuous_coinduced_rng`
`instEpiTopCatAppCounitTopCatAdjunction` 📖	mathematical	—	`CategoryTheory.Epi` `TopCat` `TopCat.instCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CondensedSet` `instCategoryCondensed` `CategoryTheory.types` `topCatToCondensedSet` `condensedSetToTopCat` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.counit` `topCatAdjunction`	—	`TopCat.epi_iff_surjective` `topCatAdjunctionCounit_bijective`
`instFaithfulTopCatTopCatToCondensedSet` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `TopCat` `TopCat.instCategory` `CondensedSet` `instCategoryCondensed` `CategoryTheory.types` `topCatToCondensedSet`	—	`CategoryTheory.Adjunction.faithful_R_of_epi_counit_app` `instEpiTopCatAppCounitTopCatAdjunction`
`instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CompactlyGenerated` `CompactlyGenerated.instCategory` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CondensedSet` `instCategoryCondensed` `CategoryTheory.types` `compactlyGeneratedToCondensedSet` `condensedSetToCompactlyGenerated` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.counit` `compactlyGeneratedAdjunction`	—	`CategoryTheory.NatTrans.isIso_iff_isIso_app`
`instUCompactlyGeneratedSpaceCarrierObjTopCatCondensedSetToTopCat` 📖	mathematical	—	`UCompactlyGeneratedSpace` `TopCat.carrier` `CategoryTheory.Functor.obj` `CondensedSet` `instCategoryCondensed` `CategoryTheory.types` `TopCat` `TopCat.instCategory` `condensedSetToTopCat` `TopCat.str`	—	—
`instUCompactlyGeneratedSpaceCarrierToTopCat` 📖	mathematical	—	`UCompactlyGeneratedSpace` `TopCat.carrier` `toTopCat` `instTopologicalSpaceObjOppositeCompHausObjFunctorTypeIsSheafCoherentTopologyOpOfPUnit`	—	`uCompactlyGeneratedSpace_of_continuous_maps` `continuous_coinduced_dom` `continuous_sigma_iff` `continuous_coinducingCoprod`
`toTopCatMap_hom_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `CategoryTheory.Functor.obj` `Opposite` `CompHaus` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.coherentTopology` `Opposite.op` `CompHaus.of` `instTopologicalSpacePUnit` `instCompactSpace` `instIndiscreteTopologyPUnit` `instTopologicalSpaceObjOppositeCompHausObjFunctorTypeIsSheafCoherentTopologyOpOfPUnit` `ContinuousMap.instFunLike` `TopCat.Hom.hom` `toTopCat` `toTopCatMap` `CategoryTheory.NatTrans.app` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory`	—	`instCompactSpace` `instIndiscreteTopologyPUnit`
`topCatAdjunctionCounit_bijective` 📖	mathematical	—	`Function.Bijective` `TopCat.carrier` `toTopCat` `TopCat.toCondensedSet` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `topCatAdjunctionCounit`	—	`Equiv.bijective`
`topCatAdjunctionCounit_hom_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `TopCat.carrier` `instTopologicalSpacePUnit` `TopCat.str` `toTopCat` `TopCat.toCondensedSet` `ContinuousMap.instFunLike` `TopCat.Hom.hom` `topCatAdjunctionCounit`	—	—
`topCatAdjunctionUnit_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CompHaus` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.coherentTopology` `TopCat.toCondensedSet` `toTopCat` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `topCatAdjunctionUnit` `TopCat.carrier` `CategoryTheory.Functor.obj` `CompHausLike` `TopCat` `TopCat.instCategory` `CompHausLike.compHausLikeToTop` `Opposite.unop` `TopCat.str` `CategoryTheory.Functor.map` `Opposite.op` `CompHaus.of` `instTopologicalSpacePUnit` `instCompactSpace` `instIndiscreteTopologyPUnit` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.const`	—	—
`topCatAdjunctionUnit_hom_app_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `TopCat.carrier` `CategoryTheory.Functor.obj` `CompHausLike` `CompHausLike.category` `TopCat` `TopCat.instCategory` `CompHausLike.compHausLikeToTop` `Opposite.unop` `toTopCat` `TopCat.str` `ContinuousMap.instFunLike` `CategoryTheory.NatTrans.app` `Opposite` `CompHaus` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.coherentTopology` `TopCat.toCondensedSet` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `topCatAdjunctionUnit` `CategoryTheory.Functor.map` `Opposite.op` `CompHaus.of` `instTopologicalSpacePUnit` `instCompactSpace` `instIndiscreteTopologyPUnit` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.const`	—	`instCompactSpace` `instIndiscreteTopologyPUnit`

(root)

Definitions

Name	Category	Theorems
`condensedSetToTopCat` 📖	CompOp	4 math math: `condensedSetToTopCat_obj_carrier`, `CondensedSet.instEpiTopCatAppCounitTopCatAdjunction`, `CondensedSet.instUCompactlyGeneratedSpaceCarrierObjTopCatCondensedSetToTopCat`, `condensedSetToTopCat_map`
`instTopologicalSpaceObjOppositeCompHausObjFunctorTypeIsSheafCoherentTopologyOpOfPUnit` 📖	CompOp	3 math math: `CondensedSet.instUCompactlyGeneratedSpaceCarrierToTopCat`, `CondensedSet.continuous_coinducingCoprod`, `CondensedSet.toTopCatMap_hom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`condensedSetToTopCat_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CondensedSet` `instCategoryCondensed` `CategoryTheory.types` `TopCat` `TopCat.instCategory` `condensedSetToTopCat` `CondensedSet.toTopCatMap`	—	—
`condensedSetToTopCat_obj_carrier` 📖	mathematical	—	`TopCat.carrier` `CategoryTheory.Functor.obj` `CondensedSet` `instCategoryCondensed` `CategoryTheory.types` `TopCat` `TopCat.instCategory` `condensedSetToTopCat` `Opposite` `CompHaus` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.coherentTopology` `Opposite.op` `CompHaus.of` `instTopologicalSpacePUnit` `instCompactSpace` `instIndiscreteTopologyPUnit`	—	—

---

← Back to Index