Topology

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

Statistics

Metric	Count
Definitions autEmbedding, autEquivAutWhiskerRight, instSMulAutFintypeCatObjObjFinite, instTopologicalSpaceAutFintypeCatObj, instTopologicalSpaceAutFunctorFintypeCat, instTopologicalSpaceObjFiniteObjFintypeCat	6
Theorems autEmbedding_apply, autEmbedding_injective, autEmbedding_isClosedEmbedding, autEmbedding_range, autEmbedding_range_isClosed, aut_discreteTopology, continuousSMul_aut_fiber, continuous_mapAut_whiskeringRight, exists_set_ker_evaluation_subset_of_isOpen, instCompactSpaceAutFunctorFintypeCat, instContinuousInvAutFunctorFintypeCat, instContinuousMulAutFunctorFintypeCat, instContinuousSMulAutFintypeCatObjObjFinite, instIsTopologicalGroupAutFunctorFintypeCat, instT2SpaceAutFunctorFintypeCat, instTotallyDisconnectedSpaceAutFunctorFintypeCat, nhds_one_has_basis_stabilizers, obj_discreteTopology	18
Total	24

CategoryTheory.PreGaloisCategory

Definitions

Name	Category	Theorems
autEmbedding 📖	CompOp	5 math math: autEmbedding_injective, autEmbedding_apply, autEmbedding_range, autEmbedding_isClosedEmbedding, autEmbedding_range_isClosed
autEquivAutWhiskerRight 📖	CompOp	—
instSMulAutFintypeCatObjObjFinite 📖	CompOp	1 math math: instContinuousSMulAutFintypeCatObjObjFinite
instTopologicalSpaceAutFintypeCatObj 📖	CompOp	4 math math: instContinuousSMulAutFintypeCatObjObjFinite, aut_discreteTopology, autEmbedding_isClosedEmbedding, autEmbedding_range_isClosed
instTopologicalSpaceAutFunctorFintypeCat 📖	CompOp	23 math math: instT2SpaceAutFunctorFintypeCat, instContinuousMulAutFunctorFintypeCat, toAutMulEquiv_isHomeomorph, instTotallyDisconnectedSpaceAutFunctorFintypeCat, instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContActionOfFiberFunctor, instFullContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, functorToContAction_map, continuous_mapAut_whiskeringRight, toAutHomeo_apply, toAut_isHomeomorph, instIsFundamentalGroupAutFunctorFintypeCat, continuousSMul_aut_fiber, nhds_one_has_basis_stabilizers, functorToContAction_obj_obj, instIsEquivalenceContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, instIsTopologicalGroupAutFunctorFintypeCat, exists_lift_of_quotient_openSubgroup, instFaithfulContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, instCompactSpaceAutFunctorFintypeCat, toAut_continuous, autEmbedding_isClosedEmbedding, instContinuousInvAutFunctorFintypeCat
instTopologicalSpaceObjFiniteObjFintypeCat 📖	CompOp	4 math math: instContinuousSMulAutFintypeCatObjObjFinite, obj_discreteTopology, continuousSMul_aut_fiber, IsFundamentalGroup.continuous_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
autEmbedding_apply 📖	mathematical	—	DFunLike.coe MonoidHom CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Pi.mulOneClass CategoryTheory.Functor.obj MonoidHom.instFunLike autEmbedding CategoryTheory.Iso.app	—	—
autEmbedding_injective 📖	mathematical	—	CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Pi.mulOneClass CategoryTheory.Functor.obj MonoidHom.instFunLike autEmbedding	—	CategoryTheory.Aut.ext CategoryTheory.NatTrans.ext' FintypeCat.hom_ext CategoryTheory.Iso.app_hom
autEmbedding_isClosedEmbedding 📖	mathematical	—	Topology.IsClosedEmbedding CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category instTopologicalSpaceAutFunctorFintypeCat Pi.topologicalSpace CategoryTheory.Functor.obj instTopologicalSpaceAutFintypeCatObj DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Pi.mulOneClass MonoidHom.instFunLike autEmbedding	—	autEmbedding_injective autEmbedding_range_isClosed
autEmbedding_range 📖	mathematical	—	Set.range CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Pi.mulOneClass CategoryTheory.Functor.obj MonoidHom.instFunLike autEmbedding Set.iInter CategoryTheory.Arrow setOf CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.ConcreteCategory.hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike FintypeCat.concreteCategoryFintype CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.Comma.hom CategoryTheory.Iso.hom	—	Set.ext CategoryTheory.NatTrans.naturality FintypeCat.hom_ext CategoryTheory.comp_apply CategoryTheory.ConcreteCategory.congr_hom
autEmbedding_range_isClosed 📖	mathematical	—	IsClosed Pi.topologicalSpace CategoryTheory.Aut FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.obj instTopologicalSpaceAutFintypeCatObj Set.range CategoryTheory.Functor CategoryTheory.Functor.category DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup Pi.mulOneClass MonoidHom.instFunLike autEmbedding	—	autEmbedding_range isClosed_iInter isClosed_eq Pi.t2Space DiscreteTopology.toT2Space obj_discreteTopology continuous_pi Continuous.comp' continuous_induced_dom continuous_of_discreteTopology aut_discreteTopology continuous_apply
aut_discreteTopology 📖	mathematical	—	DiscreteTopology CategoryTheory.Aut FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.obj instTopologicalSpaceAutFintypeCatObj	—	—
continuousSMul_aut_fiber 📖	mathematical	—	ContinuousSMul CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.obj SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup MulAction.toSemigroupAction instMulActionAutFunctorFintypeCatObjFiniteObj instTopologicalSpaceAutFunctorFintypeCat instTopologicalSpaceObjFiniteObjFintypeCat	—	Continuous.comp' continuous_induced_dom continuous_of_discreteTopology instDiscreteTopologyProd aut_discreteTopology obj_discreteTopology Continuous.prodMk continuous_apply Continuous.fst continuous_id' Continuous.snd
continuous_mapAut_whiskeringRight 📖	mathematical	—	Continuous CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight instTopologicalSpaceAutFunctorFintypeCat DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup MonoidHom.instFunLike CategoryTheory.Functor.mapAut	—	Topology.IsInducing.continuous_iff Topology.IsClosedEmbedding.isInducing autEmbedding_isClosedEmbedding continuous_pi_iff Continuous.comp' continuous_of_discreteTopology aut_discreteTopology continuous_apply continuous_induced_dom
exists_set_ker_evaluation_subset_of_isOpen 📖	mathematical	CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category Set Set.instMembership InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Aut.instGroup IsOpen instTopologicalSpaceAutFunctorFintypeCat	Set Fintype Set.Elem IsConnected CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category Set.instMembership	—	CategoryTheory.GaloisCategory.toPreGaloisCategory isOpen_induced_iff isOpen_pi_iff Finite.Set.finite_iUnion Finite.of_fintype Finite.Set.finite_range FintypeCat.hom_ext CategoryTheory.Limits.FintypeCat.jointly_surjective CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts FiberFunctor.preservesFiniteCoproducts FintypeCat.id_apply FunctorToFintypeCat.naturality CategoryTheory.id_apply CategoryTheory.Iso.ext has_decomp_connected_components
instCompactSpaceAutFunctorFintypeCat 📖	mathematical	—	CompactSpace CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category instTopologicalSpaceAutFunctorFintypeCat	—	Topology.IsClosedEmbedding.compactSpace Pi.compactSpace Finite.compactSpace FintypeCat.instFiniteAut autEmbedding_isClosedEmbedding
instContinuousInvAutFunctorFintypeCat 📖	mathematical	—	ContinuousInv CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category instTopologicalSpaceAutFunctorFintypeCat InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Aut.instGroup	—	Topology.IsInducing.continuousInv Pi.continuousInv IsTopologicalGroup.toContinuousInv topologicalGroup_of_discreteTopology aut_discreteTopology Topology.IsClosedEmbedding.isInducing autEmbedding_isClosedEmbedding
instContinuousMulAutFunctorFintypeCat 📖	mathematical	—	ContinuousMul CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category instTopologicalSpaceAutFunctorFintypeCat MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup	—	Topology.IsInducing.continuousMul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass Pi.continuousMul IsTopologicalGroup.toContinuousMul topologicalGroup_of_discreteTopology aut_discreteTopology Topology.IsClosedEmbedding.isInducing autEmbedding_isClosedEmbedding
instContinuousSMulAutFintypeCatObjObjFinite 📖	mathematical	—	ContinuousSMul CategoryTheory.Aut FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.obj CategoryTheory.ObjectProperty.FullSubcategory.obj instSMulAutFintypeCatObjObjFinite instTopologicalSpaceAutFintypeCatObj instTopologicalSpaceObjFiniteObjFintypeCat	—	continuous_of_discreteTopology instDiscreteTopologyProd aut_discreteTopology obj_discreteTopology
instIsTopologicalGroupAutFunctorFintypeCat 📖	mathematical	—	IsTopologicalGroup CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category instTopologicalSpaceAutFunctorFintypeCat CategoryTheory.Aut.instGroup	—	instContinuousMulAutFunctorFintypeCat instContinuousInvAutFunctorFintypeCat
instT2SpaceAutFunctorFintypeCat 📖	mathematical	—	T2Space CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category instTopologicalSpaceAutFunctorFintypeCat	—	T2Space.of_injective_continuous Pi.t2Space DiscreteTopology.toT2Space aut_discreteTopology autEmbedding_injective continuous_induced_dom
instTotallyDisconnectedSpaceAutFunctorFintypeCat 📖	mathematical	—	TotallyDisconnectedSpace CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category instTopologicalSpaceAutFunctorFintypeCat	—	Topology.IsEmbedding.isTotallyDisconnected_range Topology.IsClosedEmbedding.isEmbedding autEmbedding_isClosedEmbedding isTotallyDisconnected_of_totallyDisconnectedSpace Pi.totallyDisconnectedSpace TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete aut_discreteTopology
nhds_one_has_basis_stabilizers 📖	mathematical	—	Filter.HasBasis CategoryTheory.Aut CategoryTheory.Functor FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.types Finite CategoryTheory.Functor.category PointedGaloisObject nhds instTopologicalSpaceAutFunctorFintypeCat InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Aut.instGroup SetLike.coe Subgroup Subgroup.instSetLike MulAction.stabilizer CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.obj PointedGaloisObject.obj instMulActionAutFunctorFintypeCatObjFiniteObj PointedGaloisObject.pt	—	CategoryTheory.GaloisCategory.toPreGaloisCategory mem_nhds_iff exists_set_ker_evaluation_subset_of_isOpen CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits instHasFiniteLimits Finite.of_fintype exists_galois_representative FintypeCat.hom_ext surjective_of_nonempty_fiber_of_isConnected nonempty_fiber_pi_of_nonempty_of_finite nonempty_fiber_of_isConnected Function.Bijective.surjective FunctorToFintypeCat.naturality stabilizer_isOpen continuousSMul_aut_fiber obj_discreteTopology Subgroup.one_mem
obj_discreteTopology 📖	mathematical	—	DiscreteTopology CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.types Finite CategoryTheory.Functor.obj FintypeCat CategoryTheory.ObjectProperty.FullSubcategory.category instTopologicalSpaceObjFiniteObjFintypeCat	—	—

---

← Back to Index