Equivalence

📁 Source: Mathlib/CategoryTheory/Galois/Equivalence.lean

Statistics

Metric	Count
Definitions functorToContAction	1
Theorems functorToContAction_map, functorToContAction_obj_obj, instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContActionOfFiberFunctor, instFaithfulContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, instFullContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, instIsEquivalenceContActionFintypeCatHomCarrierAutFunctorFunctorToContAction	7
Total	8

CategoryTheory.PreGaloisCategory

Definitions

Name	Category	Theorems
functorToContAction 📖	CompOp	7 math math: instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, instFullContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, functorToContAction_map, instIsEquivalenceContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, instFaithfulContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContActionOfFiberFunctor, functorToContAction_obj_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorToContAction_map 📖	mathematical	—	CategoryTheory.Functor.map ContAction FintypeCat FintypeCat.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.carrier FintypeCat.instFunLikeHomCarrier FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomCarrierTopCatContinuousMapCarrier CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup instTopologicalSpaceAutFunctorFintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category Action Action.instCategory Action.IsContinuous functorToContAction CategoryTheory.ObjectProperty.homMk CategoryTheory.Functor.obj functorToAction	—	continuousSMul_aut_fiber
functorToContAction_obj_obj 📖	mathematical	—	CategoryTheory.ObjectProperty.FullSubcategory.obj Action FintypeCat FintypeCat.instCategory CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Action.instCategory Action.IsContinuous Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.carrier FintypeCat.instFunLikeHomCarrier FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomCarrierTopCatContinuousMapCarrier instTopologicalSpaceAutFunctorFintypeCat CategoryTheory.Functor.obj ContAction CategoryTheory.ObjectProperty.FullSubcategory.category functorToContAction functorToAction	—	—
instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContAction 📖	mathematical	—	CategoryTheory.Functor.EssSurj ContAction FintypeCat FintypeCat.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.carrier FintypeCat.instFunLikeHomCarrier FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomCarrierTopCatContinuousMapCarrier CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup instTopologicalSpaceAutFunctorFintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category Action Action.instCategory Action.IsContinuous functorToContAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContActionOfFiberFunctor FiberFunctor.comp_right FintypeCat.instIsEquivalenceUSwitch Action.isContinuous_def Continuous.comp continuous_of_discreteTopology FintypeCatDiscrete.instDiscreteTopologyCarrier ContinuousSMul.continuous_smul CategoryTheory.ObjectProperty.FullSubcategory.property Continuous.prodMk Continuous.fst continuous_id' Continuous.comp' obj_discreteTopology Continuous.snd CategoryTheory.NatTrans.naturality CategoryTheory.ObjectProperty.hom_ext Action.hom_ext CategoryTheory.Functor.essSurj_of_iso CategoryTheory.Functor.essSurj_comp CategoryTheory.Equivalence.essSurj_functor
instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContActionOfFiberFunctor 📖	mathematical	—	CategoryTheory.Functor.EssSurj ContAction FintypeCat FintypeCat.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.carrier FintypeCat.instFunLikeHomCarrier FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomCarrierTopCatContinuousMapCarrier CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup instTopologicalSpaceAutFunctorFintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category Action Action.instCategory Action.IsContinuous functorToContAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.ObjectProperty.FullSubcategory.property exists_lift_of_continuous FintypeCatDiscrete.instDiscreteTopologyCarrier
instFaithfulContActionFintypeCatHomCarrierAutFunctorFunctorToContAction 📖	mathematical	—	CategoryTheory.Functor.Faithful ContAction FintypeCat FintypeCat.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.carrier FintypeCat.instFunLikeHomCarrier FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomCarrierTopCatContinuousMapCarrier CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup instTopologicalSpaceAutFunctorFintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category Action Action.instCategory Action.IsContinuous functorToContAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory continuousSMul_aut_fiber CategoryTheory.ObjectProperty.instFaithfulFullSubcategoryLift instFaithfulActionFintypeCatAutFunctorFunctorToAction
instFullContActionFintypeCatHomCarrierAutFunctorFunctorToContAction 📖	mathematical	—	CategoryTheory.Functor.Full ContAction FintypeCat FintypeCat.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.carrier FintypeCat.instFunLikeHomCarrier FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomCarrierTopCatContinuousMapCarrier CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup instTopologicalSpaceAutFunctorFintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category Action Action.instCategory Action.IsContinuous functorToContAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory continuousSMul_aut_fiber CategoryTheory.ObjectProperty.instFullFullSubcategoryLift functorToAction_full
instIsEquivalenceContActionFintypeCatHomCarrierAutFunctorFunctorToContAction 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence ContAction FintypeCat FintypeCat.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct FintypeCat.carrier FintypeCat.instFunLikeHomCarrier FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomCarrierTopCatContinuousMapCarrier CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup instTopologicalSpaceAutFunctorFintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category Action Action.instCategory Action.IsContinuous functorToContAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory instFaithfulContActionFintypeCatHomCarrierAutFunctorFunctorToContAction instFullContActionFintypeCatHomCarrierAutFunctorFunctorToContAction instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContAction

---

← Back to Index