Documentation Verification Report

Continuous

📁 Source: Mathlib/CategoryTheory/Action/Continuous.lean

Statistics

Metric	Count
Definitions `IsContinuous`, `instHasForget₂HomSubtypeVTopCatContinuousMapCarrier`, `instMulActionCarrierObjTopCatForget₂ContinuousMap`, `mapContAction`, `mapContAction`, `mapContActionComp`, `mapContActionCongr`, `ContAction`, `IsDiscrete`, `instCoeAction`, `instHasForget₂HomSubtypeObjActionIsContinuousV`, `instHasForget₂HomSubtypeObjActionIsContinuousVTopCatContinuousMapCarrier`, `res`, `resComp`, `resCongr`, `resEquiv`, `DiscreteContAction`, `instCategory`, `instConcreteCategoryHomSubtypeObjActionIsContinuousContActionIsDiscreteV`, `instHasForget₂HomSubtypeObjActionIsContinuousContActionIsDiscreteV`, `instHasForget₂HomSubtypeObjActionIsContinuousContActionIsDiscreteVTopCatContinuousMapCarrier`	21
Theorems `isContinuous_def`, `mapContAction_functor`, `mapContAction_inverse`, `mapContActionComp_hom`, `mapContActionComp_inv`, `mapContActionCongr_hom`, `mapContActionCongr_inv`, `mapContAction_map`, `mapContAction_obj_obj`, `resComp_hom`, `resComp_inv`, `resCongr_hom`, `resCongr_inv`, `resEquiv_functor`, `resEquiv_inverse`, `res_map`, `res_obj_obj`, `instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap`	18
Total	39

Action

Definitions

Name	Category	Theorems
`IsContinuous` 📖	MathDef	17 math math: `DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap`, `CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `ContAction.resEquiv_inverse`, `CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `CategoryTheory.PreGaloisCategory.functorToContAction_map`, `CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `ContAction.resCongr_hom`, `ContAction.res_obj_obj`, `ContAction.resComp_hom`, `ContAction.resEquiv_functor`, `CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `ContAction.resCongr_inv`, `CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContActionOfFiberFunctor`, `CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj`, `isContinuous_def`, `ContAction.resComp_inv`, `ContAction.res_map`
`instHasForget₂HomSubtypeVTopCatContinuousMapCarrier` 📖	CompOp	1 math math: `isContinuous_def`
`instMulActionCarrierObjTopCatForget₂ContinuousMap` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isContinuous_def` 📖	mathematical	—	`IsContinuous` `Continuous` `TopCat.carrier` `CategoryTheory.Functor.obj` `Action` `instCategory` `TopCat` `TopCat.instCategory` `CategoryTheory.forget₂` `HomSubtype` `V` `instFunLikeHomSubtypeV` `instConcreteCategoryHomSubtypeV` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `instHasForget₂HomSubtypeVTopCatContinuousMapCarrier` `instTopologicalSpaceProd` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CategoryTheory.Functor.map` `MonoidHom` `CategoryTheory.End` `CategoryTheory.Category.toCategoryStruct` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.End.monoid` `MonoidHom.instFunLike` `ρ`	—	`ContinuousSMul.continuous_smul`

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
`mapContAction` 📖	CompOp	2 math math: `mapContAction_functor`, `mapContAction_inverse`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapContAction_functor` 📖	mathematical	`Action.IsContinuous` `CategoryTheory.Functor.obj` `Action` `Action.instCategory` `CategoryTheory.Functor.mapAction` `functor` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `inverse`	`ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `mapContAction` `CategoryTheory.Functor.mapContAction`	—	—
`mapContAction_inverse` 📖	mathematical	`Action.IsContinuous` `CategoryTheory.Functor.obj` `Action` `Action.instCategory` `CategoryTheory.Functor.mapAction` `functor` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `inverse`	`ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `mapContAction` `CategoryTheory.Functor.mapContAction`	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`mapContAction` 📖	CompOp	8 math math: `mapContActionCongr_inv`, `mapContActionComp_inv`, `mapContActionCongr_hom`, `CategoryTheory.Equivalence.mapContAction_functor`, `mapContAction_map`, `CategoryTheory.Equivalence.mapContAction_inverse`, `mapContActionComp_hom`, `mapContAction_obj_obj`
`mapContActionComp` 📖	CompOp	2 math math: `mapContActionComp_inv`, `mapContActionComp_hom`
`mapContActionCongr` 📖	CompOp	2 math math: `mapContActionCongr_inv`, `mapContActionCongr_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapContActionComp_hom` 📖	mathematical	`Action.IsContinuous` `obj` `Action` `Action.instCategory` `mapAction` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	`CategoryTheory.Iso.hom` `CategoryTheory.Functor` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `category` `mapContAction` `comp` `mapContActionComp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.refl`	—	—
`mapContActionComp_inv` 📖	mathematical	`Action.IsContinuous` `obj` `Action` `Action.instCategory` `mapAction` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	`CategoryTheory.Iso.inv` `CategoryTheory.Functor` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `category` `mapContAction` `comp` `mapContActionComp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Iso.refl`	—	—
`mapContActionCongr_hom` 📖	mathematical	`Action.IsContinuous` `obj` `Action` `Action.instCategory` `mapAction` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	`CategoryTheory.Iso.hom` `CategoryTheory.Functor` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `category` `mapContAction` `mapContActionCongr` `CategoryTheory.ObjectProperty.homMk` `Action.mkIso` `CategoryTheory.Iso.app` `Action.V` `CategoryTheory.ObjectProperty.isoMk`	—	—
`mapContActionCongr_inv` 📖	mathematical	`Action.IsContinuous` `obj` `Action` `Action.instCategory` `mapAction` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	`CategoryTheory.Iso.inv` `CategoryTheory.Functor` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `category` `mapContAction` `mapContActionCongr` `CategoryTheory.ObjectProperty.homMk` `Action.mkIso` `CategoryTheory.Iso.app` `Action.V` `CategoryTheory.ObjectProperty.isoMk`	—	—
`mapContAction_map` 📖	mathematical	`Action.IsContinuous` `obj` `Action` `Action.instCategory` `mapAction` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	`map` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `mapContAction` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory`	—	—
`mapContAction_obj_obj` 📖	mathematical	`Action.IsContinuous` `obj` `Action` `Action.instCategory` `mapAction` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	`ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `mapContAction`	—	—

ContAction

Definitions

Name	Category	Theorems
`IsDiscrete` 📖	MathDef	1 math math: `DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap`
`instCoeAction` 📖	CompOp	—
`instHasForget₂HomSubtypeObjActionIsContinuousV` 📖	CompOp	—
`instHasForget₂HomSubtypeObjActionIsContinuousVTopCatContinuousMapCarrier` 📖	CompOp	—
`res` 📖	CompOp	8 math math: `resEquiv_inverse`, `resCongr_hom`, `res_obj_obj`, `resComp_hom`, `resEquiv_functor`, `resCongr_inv`, `resComp_inv`, `res_map`
`resComp` 📖	CompOp	2 math math: `resComp_hom`, `resComp_inv`
`resCongr` 📖	CompOp	2 math math: `resCongr_hom`, `resCongr_inv`
`resEquiv` 📖	CompOp	2 math math: `resEquiv_inverse`, `resEquiv_functor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`resComp_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `Action` `Action.instCategory` `Action.IsContinuous` `CategoryTheory.Functor.category` `res` `ContinuousMonoidHom.comp` `CategoryTheory.Functor.comp` `resComp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.refl`	—	—
`resComp_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `Action` `Action.instCategory` `Action.IsContinuous` `CategoryTheory.Functor.category` `res` `ContinuousMonoidHom.comp` `CategoryTheory.Functor.comp` `resComp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.refl`	—	—
`resCongr_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `Action` `Action.instCategory` `Action.IsContinuous` `CategoryTheory.Functor.category` `res` `resCongr` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.Functor.obj` `Action.res` `MonoidHomClass.toMonoidHom` `ContinuousMonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `ContinuousMonoidHom.instFunLike` `ContinuousMonoidHom.instMonoidHomClass` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `Action.mkIso` `CategoryTheory.Iso.refl` `Action.V` `CategoryTheory.ObjectProperty.isoMk`	—	—
`resCongr_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `Action` `Action.instCategory` `Action.IsContinuous` `CategoryTheory.Functor.category` `res` `resCongr` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.Functor.obj` `Action.res` `MonoidHomClass.toMonoidHom` `ContinuousMonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `ContinuousMonoidHom.instFunLike` `ContinuousMonoidHom.instMonoidHomClass` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `Action.mkIso` `CategoryTheory.Iso.refl` `Action.V` `CategoryTheory.ObjectProperty.isoMk`	—	—
`resEquiv_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `Action` `Action.instCategory` `Action.IsContinuous` `resEquiv` `res` `ContinuousMonoidHom.toContinuousMonoidHom` `ContinuousMulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `ContinuousMulEquiv.instEquivLike`	—	—
`resEquiv_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `Action` `Action.instCategory` `Action.IsContinuous` `resEquiv` `res` `ContinuousMonoidHom.toContinuousMonoidHom` `ContinuousMulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `EquivLike.toFunLike` `ContinuousMulEquiv.instEquivLike` `ContinuousMulEquiv.symm`	—	—
`res_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `Action` `Action.instCategory` `Action.IsContinuous` `res` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.Functor.obj` `Action.res` `MonoidHomClass.toMonoidHom` `ContinuousMonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `ContinuousMonoidHom.instFunLike` `ContinuousMonoidHom.instMonoidHomClass` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory`	—	`ContinuousMonoidHom.instMonoidHomClass`
`res_obj_obj` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `Action` `Action.instCategory` `Action.IsContinuous` `CategoryTheory.Functor.obj` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `res` `Action.res` `MonoidHomClass.toMonoidHom` `ContinuousMonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `ContinuousMonoidHom.instFunLike` `ContinuousMonoidHom.instMonoidHomClass`	—	—

DiscreteContAction

Definitions

Name	Category	Theorems
`instCategory` 📖	CompOp	1 math math: `instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap`
`instConcreteCategoryHomSubtypeObjActionIsContinuousContActionIsDiscreteV` 📖	CompOp	1 math math: `instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap`
`instHasForget₂HomSubtypeObjActionIsContinuousContActionIsDiscreteV` 📖	CompOp	—
`instHasForget₂HomSubtypeObjActionIsContinuousContActionIsDiscreteVTopCatContinuousMapCarrier` 📖	CompOp	1 math math: `instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap` 📖	mathematical	—	`DiscreteTopology` `TopCat.carrier` `CategoryTheory.Functor.obj` `DiscreteContAction` `instCategory` `TopCat` `TopCat.instCategory` `CategoryTheory.forget₂` `Action.HomSubtype` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `Action` `Action.instCategory` `Action.IsContinuous` `ContAction` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ContAction.IsDiscrete` `Action.V` `Action.instFunLikeHomSubtypeV` `instConcreteCategoryHomSubtypeObjActionIsContinuousContActionIsDiscreteV` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `instHasForget₂HomSubtypeObjActionIsContinuousContActionIsDiscreteVTopCatContinuousMapCarrier`	—	`CategoryTheory.ObjectProperty.FullSubcategory.property`

(root)

Definitions

Name	Category	Theorems
`ContAction` 📖	CompOp	24 math math: `DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap`, `CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `CategoryTheory.Functor.mapContActionCongr_inv`, `CategoryTheory.Functor.mapContActionComp_inv`, `CategoryTheory.Functor.mapContActionCongr_hom`, `ContAction.resEquiv_inverse`, `CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `CategoryTheory.PreGaloisCategory.functorToContAction_map`, `CategoryTheory.Equivalence.mapContAction_functor`, `CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `CategoryTheory.Functor.mapContAction_map`, `ContAction.resCongr_hom`, `ContAction.res_obj_obj`, `ContAction.resComp_hom`, `ContAction.resEquiv_functor`, `CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `ContAction.resCongr_inv`, `CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContActionOfFiberFunctor`, `CategoryTheory.Equivalence.mapContAction_inverse`, `CategoryTheory.Functor.mapContActionComp_hom`, `CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj`, `CategoryTheory.Functor.mapContAction_obj_obj`, `ContAction.resComp_inv`, `ContAction.res_map`
`DiscreteContAction` 📖	CompOp	1 math math: `DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap`

---

← Back to Index