Documentation Verification Report

Topology

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

Statistics

Metric	Count
Definitions `autEmbedding`, `autEquivAutWhiskerRight`, `instSMulAutFintypeCatObjCarrier`, `instTopologicalSpaceAutFintypeCatObj`, `instTopologicalSpaceAutFunctorFintypeCat`, `instTopologicalSpaceCarrierObjFintypeCat`	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`, `instContinuousSMulAutFintypeCatObjCarrier`, `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	—
`instSMulAutFintypeCatObjCarrier` 📖	CompOp	1 math math: `instContinuousSMulAutFintypeCatObjCarrier`
`instTopologicalSpaceAutFintypeCatObj` 📖	CompOp	4 math math: `aut_discreteTopology`, `instContinuousSMulAutFintypeCatObjCarrier`, `autEmbedding_isClosedEmbedding`, `autEmbedding_range_isClosed`
`instTopologicalSpaceAutFunctorFintypeCat` 📖	CompOp	23 math math: `instT2SpaceAutFunctorFintypeCat`, `instContinuousMulAutFunctorFintypeCat`, `toAutMulEquiv_isHomeomorph`, `instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `instTotallyDisconnectedSpaceAutFunctorFintypeCat`, `instFullContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `functorToContAction_map`, `continuous_mapAut_whiskeringRight`, `toAutHomeo_apply`, `instIsEquivalenceContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `toAut_isHomeomorph`, `instIsFundamentalGroupAutFunctorFintypeCat`, `continuousSMul_aut_fiber`, `nhds_one_has_basis_stabilizers`, `instFaithfulContActionFintypeCatHomCarrierAutFunctorFunctorToContAction`, `instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContActionOfFiberFunctor`, `functorToContAction_obj_obj`, `instIsTopologicalGroupAutFunctorFintypeCat`, `exists_lift_of_quotient_openSubgroup`, `instCompactSpaceAutFunctorFintypeCat`, `toAut_continuous`, `autEmbedding_isClosedEmbedding`, `instContinuousInvAutFunctorFintypeCat`
`instTopologicalSpaceCarrierObjFintypeCat` 📖	CompOp	4 math math: `obj_discreteTopology`, `continuousSMul_aut_fiber`, `IsFundamentalGroup.continuous_smul`, `instContinuousSMulAutFintypeCatObjCarrier`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`autEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `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` `FintypeCat.instCategory` `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` `FintypeCat.instCategory` `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` `FintypeCat.instCategory` `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` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map` `CategoryTheory.Comma.hom` `CategoryTheory.Iso.hom`	—	`Set.ext` `CategoryTheory.NatTrans.naturality`
`autEmbedding_range_isClosed` 📖	mathematical	—	`IsClosed` `Pi.topologicalSpace` `CategoryTheory.Aut` `FintypeCat` `FintypeCat.instCategory` `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` `FintypeCat.instCategory` `CategoryTheory.Functor.obj` `instTopologicalSpaceAutFintypeCatObj`	—	—
`continuousSMul_aut_fiber` 📖	mathematical	—	`ContinuousSMul` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `MulAction.toSemigroupAction` `instMulActionAutFunctorFintypeCatCarrierObj` `instTopologicalSpaceAutFunctorFintypeCat` `instTopologicalSpaceCarrierObjFintypeCat`	—	`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` `FintypeCat.instCategory` `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` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `CategoryTheory.Aut.instGroup` `IsOpen` `instTopologicalSpaceAutFunctorFintypeCat`	`IsConnected`	—	`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` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `instTopologicalSpaceAutFunctorFintypeCat`	—	`Topology.IsClosedEmbedding.compactSpace` `Pi.compactSpace` `Finite.compactSpace` `FintypeCat.instFiniteAut` `autEmbedding_isClosedEmbedding`
`instContinuousInvAutFunctorFintypeCat` 📖	mathematical	—	`ContinuousInv` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `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` `FintypeCat.instCategory` `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`
`instContinuousSMulAutFintypeCatObjCarrier` 📖	mathematical	—	`ContinuousSMul` `CategoryTheory.Aut` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.obj` `FintypeCat.carrier` `instSMulAutFintypeCatObjCarrier` `instTopologicalSpaceAutFintypeCatObj` `instTopologicalSpaceCarrierObjFintypeCat`	—	`continuous_of_discreteTopology` `instDiscreteTopologyProd` `aut_discreteTopology` `obj_discreteTopology`
`instIsTopologicalGroupAutFunctorFintypeCat` 📖	mathematical	—	`IsTopologicalGroup` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `instTopologicalSpaceAutFunctorFintypeCat` `CategoryTheory.Aut.instGroup`	—	`instContinuousMulAutFunctorFintypeCat` `instContinuousInvAutFunctorFintypeCat`
`instT2SpaceAutFunctorFintypeCat` 📖	mathematical	—	`T2Space` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `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` `FintypeCat.instCategory` `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` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `PointedGaloisObject` `nhds` `instTopologicalSpaceAutFunctorFintypeCat` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `CategoryTheory.Aut.instGroup` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `MulAction.stabilizer` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `PointedGaloisObject.obj` `instMulActionAutFunctorFintypeCatCarrierObj` `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` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `instTopologicalSpaceCarrierObjFintypeCat`	—	—

---

← Back to Index