Documentation Verification Report

TopCatAdjunction

📁 Source: Mathlib/Condensed/Light/TopCatAdjunction.lean

Statistics

Metric	Count
Definitions `fullyFaithfulSequentialToLightCondSet`, `lightCondSetToSequential`, `sequentialAdjunction`, `sequentialAdjunctionCounitIso`, `sequentialAdjunctionHomeo`, `sequentialToLightCondSet`, `toTopCat`, `toTopCatMap`, `topCatAdjunction`, `topCatAdjunctionCounit`, `topCatAdjunctionCounitEquiv`, `topCatAdjunctionUnit`, `underlyingTopologicalSpace`, `lightCondSetToTopCat`	14
Theorems `continuous_coinducingCoprod`, `instEpiTopCatAppCounitTopCatAdjunction`, `instFaithfulTopCatTopCatToLightCondSet`, `instIsIsoFunctorSequentialCounitSequentialAdjunction`, `instSequentialSpaceCarrierObjTopCatLightCondSetToTopCat`, `instSequentialSpaceCarrierToTopCat`, `toTopCatMap_hom_apply`, `topCatAdjunctionCounit_bijective`, `topCatAdjunctionUnit_val_app`, `topCatAdjunctionUnit_val_app_apply`, `lightCondSetToTopCat_map`, `lightCondSetToTopCat_obj_carrier`	12
Total	26

LightCondSet

Definitions

Name	Category	Theorems
`fullyFaithfulSequentialToLightCondSet` 📖	CompOp	—
`lightCondSetToSequential` 📖	CompOp	1 math math: `instIsIsoFunctorSequentialCounitSequentialAdjunction`
`sequentialAdjunction` 📖	CompOp	1 math math: `instIsIsoFunctorSequentialCounitSequentialAdjunction`
`sequentialAdjunctionCounitIso` 📖	CompOp	—
`sequentialAdjunctionHomeo` 📖	CompOp	—
`sequentialToLightCondSet` 📖	CompOp	1 math math: `instIsIsoFunctorSequentialCounitSequentialAdjunction`
`toTopCat` 📖	CompOp	5 math math: `topCatAdjunctionUnit_val_app_apply`, `topCatAdjunctionCounit_bijective`, `instSequentialSpaceCarrierToTopCat`, `topCatAdjunctionUnit_val_app`, `toTopCatMap_hom_apply`
`toTopCatMap` 📖	CompOp	2 math math: `lightCondSetToTopCat_map`, `toTopCatMap_hom_apply`
`topCatAdjunction` 📖	CompOp	1 math math: `instEpiTopCatAppCounitTopCatAdjunction`
`topCatAdjunctionCounit` 📖	CompOp	1 math math: `topCatAdjunctionCounit_bijective`
`topCatAdjunctionCounitEquiv` 📖	CompOp	—
`topCatAdjunctionUnit` 📖	CompOp	2 math math: `topCatAdjunctionUnit_val_app_apply`, `topCatAdjunctionUnit_val_app`
`underlyingTopologicalSpace` 📖	CompOp	3 math math: `continuous_coinducingCoprod`, `instSequentialSpaceCarrierToTopCat`, `toTopCatMap_hom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_coinducingCoprod` 📖	mathematical	—	`Continuous` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `SecondCountableTopology` `LightProfinite` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CompHausLike.category` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `Opposite.op` `LightProfinite.of` `instTopologicalSpacePUnit` `Finite.compactSpace` `Finite.of_fintype` `PUnit.fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `instMetricSpacePUnit` `TotallySeparatedSpace.totallyDisconnectedSpace` `TotallySeparatedSpace.of_discrete` `instDiscreteTopologyPUnit` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountablePUnit` `PseudoEMetricSpace.pseudoMetrizableSpace` `EMetricSpace.toPseudoEMetricSpace` `underlyingTopologicalSpace`	—	`Finite.compactSpace` `Finite.of_fintype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `TotallySeparatedSpace.totallyDisconnectedSpace` `TotallySeparatedSpace.of_discrete` `instDiscreteTopologyPUnit` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountablePUnit` `PseudoEMetricSpace.pseudoMetrizableSpace` `continuous_sigma_iff` `continuous_coinduced_rng`
`instEpiTopCatAppCounitTopCatAdjunction` 📖	mathematical	—	`CategoryTheory.Epi` `TopCat` `TopCat.instCategory` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `LightCondSet` `instCategoryLightCondensed` `CategoryTheory.types` `topCatToLightCondSet` `lightCondSetToTopCat` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.counit` `topCatAdjunction`	—	`TopCat.epi_iff_surjective` `topCatAdjunctionCounit_bijective`
`instFaithfulTopCatTopCatToLightCondSet` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `TopCat` `TopCat.instCategory` `LightCondSet` `instCategoryLightCondensed` `CategoryTheory.types` `topCatToLightCondSet`	—	`CategoryTheory.Adjunction.faithful_R_of_epi_counit_app` `instEpiTopCatAppCounitTopCatAdjunction`
`instIsIsoFunctorSequentialCounitSequentialAdjunction` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `Sequential` `Sequential.instCategory` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `LightCondSet` `instCategoryLightCondensed` `CategoryTheory.types` `sequentialToLightCondSet` `lightCondSetToSequential` `CategoryTheory.Functor.id` `CategoryTheory.Adjunction.counit` `sequentialAdjunction`	—	`CategoryTheory.NatTrans.isIso_iff_isIso_app` `CategoryTheory.Iso.isIso_hom`
`instSequentialSpaceCarrierObjTopCatLightCondSetToTopCat` 📖	mathematical	—	`SequentialSpace` `TopCat.carrier` `CategoryTheory.Functor.obj` `LightCondSet` `instCategoryLightCondensed` `CategoryTheory.types` `TopCat` `TopCat.instCategory` `lightCondSetToTopCat` `TopCat.str`	—	`instSequentialSpaceCarrierToTopCat`
`instSequentialSpaceCarrierToTopCat` 📖	mathematical	—	`SequentialSpace` `TopCat.carrier` `toTopCat` `underlyingTopologicalSpace`	—	`SequentialSpace.coinduced` `Sigma.instSequentialSpace` `FrechetUrysohnSpace.to_sequentialSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.SecondCountableTopology.to_firstCountableTopology` `LightProfinite.instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace`
`toTopCatMap_hom_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `CategoryTheory.Functor.obj` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `Opposite.op` `LightProfinite.of` `instTopologicalSpacePUnit` `underlyingTopologicalSpace` `ContinuousMap.instFunLike` `TopCat.Hom.hom` `toTopCat` `toTopCatMap` `CategoryTheory.NatTrans.app` `CategoryTheory.Sheaf.Hom.val`	—	—
`topCatAdjunctionCounit_bijective` 📖	mathematical	—	`Function.Bijective` `TopCat.carrier` `toTopCat` `TopCat.toLightCondSet` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `topCatAdjunctionCounit`	—	`Equiv.bijective`
`topCatAdjunctionUnit_val_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `TopCat.toLightCondSet` `toTopCat` `CategoryTheory.Sheaf.Hom.val` `topCatAdjunctionUnit` `CategoryTheory.Functor.obj` `CompHausLike` `TopCat` `TopCat.instCategory` `CompHausLike.compHausLikeToTop` `Opposite.unop` `CategoryTheory.Functor.map` `Opposite.op` `LightProfinite.of` `instTopologicalSpacePUnit` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.const`	—	—
`topCatAdjunctionUnit_val_app_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `TopCat.carrier` `CategoryTheory.Functor.obj` `CompHausLike` `TotallyDisconnectedSpace` `TopCat.str` `SecondCountableTopology` `CompHausLike.category` `TopCat` `TopCat.instCategory` `CompHausLike.compHausLikeToTop` `Opposite.unop` `toTopCat` `ContinuousMap.instFunLike` `CategoryTheory.NatTrans.app` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `TopCat.toLightCondSet` `CategoryTheory.Sheaf.Hom.val` `topCatAdjunctionUnit` `CategoryTheory.Functor.map` `Opposite.op` `LightProfinite.of` `instTopologicalSpacePUnit` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.const`	—	—

(root)

Definitions

Name	Category	Theorems
`lightCondSetToTopCat` 📖	CompOp	4 math math: `LightCondSet.instEpiTopCatAppCounitTopCatAdjunction`, `LightCondSet.instSequentialSpaceCarrierObjTopCatLightCondSetToTopCat`, `lightCondSetToTopCat_obj_carrier`, `lightCondSetToTopCat_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lightCondSetToTopCat_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `LightCondSet` `instCategoryLightCondensed` `CategoryTheory.types` `TopCat` `TopCat.instCategory` `lightCondSetToTopCat` `LightCondSet.toTopCatMap`	—	—
`lightCondSetToTopCat_obj_carrier` 📖	mathematical	—	`TopCat.carrier` `CategoryTheory.Functor.obj` `LightCondSet` `instCategoryLightCondensed` `CategoryTheory.types` `TopCat` `TopCat.instCategory` `lightCondSetToTopCat` `Opposite` `LightProfinite` `CategoryTheory.Category.opposite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.str` `SecondCountableTopology` `CategoryTheory.Sheaf.val` `CategoryTheory.coherentTopology` `Opposite.op` `LightProfinite.of` `instTopologicalSpacePUnit`	—	—

---

← Back to Index