Equivalence

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

Statistics

Metric	Count
Definitions functorToContAction	1
Theorems functorToContAction_map, functorToContAction_obj_obj, instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContActionOfFiberFunctor, instFaithfulContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, instFullContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, instIsEquivalenceContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction	7
Total	8

CategoryTheory.PreGaloisCategory

Definitions

Name	Category	Theorems
functorToContAction 📖	CompOp	7 math math: instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContActionOfFiberFunctor, instFullContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, functorToContAction_map, functorToContAction_obj_obj, instIsEquivalenceContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, instFaithfulContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorToContAction_map 📖	mathematical	—	CategoryTheory.Functor.map ContAction FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Types.instFunLike FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomObjFiniteTopCatContinuousMapCarrier CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup instTopologicalSpaceAutFunctorFintypeCat 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 CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite 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 CategoryTheory.Types.instFunLike FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomObjFiniteTopCatContinuousMapCarrier instTopologicalSpaceAutFunctorFintypeCat CategoryTheory.Functor.obj ContAction functorToContAction functorToAction	—	—
instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction 📖	mathematical	—	CategoryTheory.Functor.EssSurj ContAction FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Types.instFunLike FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomObjFiniteTopCatContinuousMapCarrier CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup instTopologicalSpaceAutFunctorFintypeCat Action Action.instCategory Action.IsContinuous functorToContAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContActionOfFiberFunctor FiberFunctor.comp_right FintypeCat.instIsEquivalenceUSwitch Action.isContinuous_def Continuous.comp continuous_bot ContinuousSMul.continuous_smul CategoryTheory.ObjectProperty.FullSubcategory.property Continuous.prodMk Continuous.fst continuous_id' Continuous.comp' continuous_of_discreteTopology 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
instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContActionOfFiberFunctor 📖	mathematical	—	CategoryTheory.Functor.EssSurj ContAction FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Types.instFunLike FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomObjFiniteTopCatContinuousMapCarrier CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup instTopologicalSpaceAutFunctorFintypeCat Action Action.instCategory Action.IsContinuous functorToContAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory CategoryTheory.ObjectProperty.FullSubcategory.property exists_lift_of_continuous FintypeCatDiscrete.instDiscreteTopologyObjFinite
instFaithfulContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction 📖	mathematical	—	CategoryTheory.Functor.Faithful ContAction FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Types.instFunLike FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomObjFiniteTopCatContinuousMapCarrier CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup instTopologicalSpaceAutFunctorFintypeCat Action Action.instCategory Action.IsContinuous functorToContAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory
instFullContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction 📖	mathematical	—	CategoryTheory.Functor.Full ContAction FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Types.instFunLike FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomObjFiniteTopCatContinuousMapCarrier CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup instTopologicalSpaceAutFunctorFintypeCat Action Action.instCategory Action.IsContinuous functorToContAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory
instIsEquivalenceContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence ContAction FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Types.instFunLike FintypeCat.concreteCategoryFintype FintypeCatDiscrete.instHasForget₂FintypeCatHomObjFiniteTopCatContinuousMapCarrier CategoryTheory.Aut CategoryTheory.Functor CategoryTheory.Functor.category DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup instTopologicalSpaceAutFunctorFintypeCat Action Action.instCategory Action.IsContinuous functorToContAction	—	CategoryTheory.GaloisCategory.toPreGaloisCategory instFaithfulContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction instFullContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction

---

← Back to Index