Documentation Verification Report

IsFundamentalgroup

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

Statistics

Metric	Count
Definitions `IsFundamentalGroup`, `IsNaturalSMul`, `toAut`, `toAutHomeo`, `toAutMulEquiv`	5
Theorems `continuous_smul`, `non_trivial`, `non_trivial'`, `toIsNaturalSMul`, `transitive_of_isGalois`, `naturality`, `action_ext_of_isGalois`, `instIsFundamentalGroupAutFunctorFintypeCat`, `instIsPretransitiveCarrierObjFintypeCatOfIsConnected`, `isPretransitive_of_surjective`, `toAutHomeo_apply`, `toAutMulEquiv_apply`, `toAutMulEquiv_isHomeomorph`, `toAut_bijective`, `toAut_continuous`, `toAut_hom_app_apply`, `toAut_injective_of_non_trivial`, `toAut_isHomeomorph`, `toAut_surjective_isGalois`, `toAut_surjective_isGalois_finite_family`, `toAut_surjective_of_isPretransitive`	21
Total	26

CategoryTheory.PreGaloisCategory

Definitions

Name	Category	Theorems
`IsFundamentalGroup` 📖	CompData	1 math math: `instIsFundamentalGroupAutFunctorFintypeCat`
`IsNaturalSMul` 📖	CompData	1 math math: `IsFundamentalGroup.toIsNaturalSMul`
`toAut` 📖	CompOp	8 math math: `toAut_hom_app_apply`, `toAutHomeo_apply`, `toAutMulEquiv_apply`, `toAut_isHomeomorph`, `toAut_surjective_of_isPretransitive`, `toAut_bijective`, `toAut_injective_of_non_trivial`, `toAut_continuous`
`toAutHomeo` 📖	CompOp	1 math math: `toAutHomeo_apply`
`toAutMulEquiv` 📖	CompOp	2 math math: `toAutMulEquiv_isHomeomorph`, `toAutMulEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`action_ext_of_isGalois` 📖	—	`FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `DFunLike.coe` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.NatTrans.app`	—	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `MulAction.exists_smul_eq` `isPretransitive_of_isGalois` `CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback` `CategoryTheory.Functor.map_mono` `CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape` `FiberFunctor.preservesPullbacks` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits` `CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForgetHomCarrier` `IsNaturalSMul.naturality` `FunctorToFintypeCat.naturality`
`instIsFundamentalGroupAutFunctorFintypeCat` 📖	mathematical	—	`IsFundamentalGroup` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `CategoryTheory.Aut.instGroup` `instMulActionAutFunctorFintypeCatCarrierObj` `instTopologicalSpaceAutFunctorFintypeCat` `instIsTopologicalGroupAutFunctorFintypeCat` `instCompactSpaceAutFunctorFintypeCat`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `instIsTopologicalGroupAutFunctorFintypeCat` `instCompactSpaceAutFunctorFintypeCat` `FunctorToFintypeCat.naturality` `FiberFunctor.isPretransitive_of_isConnected` `IsGalois.toIsConnected` `continuousSMul_aut_fiber` `CategoryTheory.Aut.ext` `CategoryTheory.NatTrans.ext'` `FintypeCat.hom_ext`
`instIsPretransitiveCarrierObjFintypeCatOfIsConnected` 📖	mathematical	—	`MulAction.IsPretransitive` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `isPretransitive_of_surjective` `IsFundamentalGroup.toIsNaturalSMul` `Function.Bijective.surjective` `toAut_bijective`
`isPretransitive_of_surjective` 📖	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` `MonoidHom.instFunLike` `toAut`	`MulAction.IsPretransitive` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `MulAction.exists_smul_eq` `FiberFunctor.isPretransitive_of_isConnected`
`toAutHomeo_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `instTopologicalSpaceAutFunctorFintypeCat` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `toAutHomeo` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `toAut` `IsFundamentalGroup.toIsNaturalSMul`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory`
`toAutMulEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toAutMulEquiv` `MonoidHom` `MonoidHom.instFunLike` `toAut` `IsFundamentalGroup.toIsNaturalSMul`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory`
`toAutMulEquiv_isHomeomorph` 📖	mathematical	—	`IsHomeomorph` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `instTopologicalSpaceAutFunctorFintypeCat` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toAutMulEquiv`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `toAut_isHomeomorph`
`toAut_bijective` 📖	mathematical	—	`Function.Bijective` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `toAut` `IsFundamentalGroup.toIsNaturalSMul`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `IsFundamentalGroup.toIsNaturalSMul` `toAut_injective_of_non_trivial` `IsFundamentalGroup.non_trivial'` `toAut_surjective_of_isPretransitive` `IsFundamentalGroup.continuous_smul` `IsFundamentalGroup.transitive_of_isGalois`
`toAut_continuous` 📖	mathematical	`ContinuousSMul` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instTopologicalSpaceCarrierObjFintypeCat`	`Continuous` `CategoryTheory.Aut` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `instTopologicalSpaceAutFunctorFintypeCat` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `toAut`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `continuous_of_continuousAt_one` `instContinuousMulAutFunctorFintypeCat` `MonoidHom.instMonoidHomClass` `continuousAt_def` `map_one` `MonoidHomClass.toOneHomClass` `Filter.HasBasis.mem_iff'` `nhds_one_has_basis_stabilizers` `mem_nhds_iff` `Set.preimage_mono` `stabilizer_isOpen` `obj_discreteTopology` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass`
`toAut_hom_app_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `MonoidHom` `CategoryTheory.Aut` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `toAut` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	—
`toAut_injective_of_non_trivial` 📖	mathematical	`InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `toAut`	—	`MonoidHom.ker_eq_bot_iff` `eq_bot_iff` `toAut_hom_app_apply` `FintypeCat.id_apply`
`toAut_isHomeomorph` 📖	mathematical	—	`IsHomeomorph` `CategoryTheory.Aut` `CategoryTheory.Functor` `FintypeCat` `FintypeCat.instCategory` `CategoryTheory.Functor.category` `instTopologicalSpaceAutFunctorFintypeCat` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `toAut` `IsFundamentalGroup.toIsNaturalSMul`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `IsFundamentalGroup.toIsNaturalSMul` `isHomeomorph_iff_continuous_bijective` `instT2SpaceAutFunctorFintypeCat` `toAut_continuous` `IsFundamentalGroup.continuous_smul` `toAut_bijective`
`toAut_surjective_isGalois` 📖	mathematical	—	`FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `DFunLike.coe` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `nonempty_fiber_of_isConnected` `IsGalois.toIsConnected` `MulAction.exists_smul_eq` `action_ext_of_isGalois`
`toAut_surjective_isGalois_finite_family` 📖	mathematical	`IsGalois` `MulAction.IsPretransitive` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`DFunLike.coe` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `nonempty_fiber_of_isConnected` `IsGalois.toIsConnected` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits` `instHasFiniteLimits` `CategoryTheory.Limits.FintypeCat.hasFiniteLimits` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts` `CategoryTheory.Limits.instPreservesFiniteProductsOfPreservesFiniteLimits` `FiberFunctor.instPreservesFiniteLimitsFintypeCat` `FintypeCat.inv_hom_id_apply` `CategoryTheory.Limits.FintypeCat.productEquiv_symm_comp_π_apply` `exists_hom_from_galois_of_fiber` `toAut_surjective_isGalois` `action_ext_of_isGalois` `IsNaturalSMul.naturality` `FunctorToFintypeCat.naturality`
`toAut_surjective_of_isPretransitive` 📖	mathematical	`ContinuousSMul` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instTopologicalSpaceCarrierObjFintypeCat` `MulAction.IsPretransitive`	`CategoryTheory.Aut` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.Aut.instGroup` `MonoidHom.instFunLike` `toAut`	—	`CategoryTheory.GaloisCategory.toPreGaloisCategory` `Set.univ_inter` `IsCompact.inter_iInter_nonempty` `CompactSpace.isCompact_univ` `IsClosed.leftCoset` `IsTopologicalGroup.toContinuousMul` `Subgroup.isClosed_of_isOpen` `stabilizer_isOpen` `obj_discreteTopology` `toAut_surjective_isGalois_finite_family` `Finite.of_fintype` `PointedGaloisObject.isGalois` `mem_leftCoset_iff` `SetLike.mem_coe` `MulAction.mem_stabilizer_iff` `SemigroupAction.mul_smul` `inv_smul_smul` `CategoryTheory.Iso.ext` `natTrans_ext_of_isGalois` `FintypeCat.hom_ext` `smul_eq_mul` `toAut_surjective_isGalois`

CategoryTheory.PreGaloisCategory.IsFundamentalGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_smul` 📖	mathematical	—	`ContinuousSMul` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `CategoryTheory.PreGaloisCategory.instTopologicalSpaceCarrierObjFintypeCat`	—	—
`non_trivial` 📖	mathematical	`FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`non_trivial'`
`non_trivial'` 📖	mathematical	`FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`toIsNaturalSMul` 📖	mathematical	—	`CategoryTheory.PreGaloisCategory.IsNaturalSMul`	—	—
`transitive_of_isGalois` 📖	mathematical	—	`MulAction.IsPretransitive` `FintypeCat.carrier` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—

CategoryTheory.PreGaloisCategory.IsNaturalSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`naturality` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `FintypeCat.carrier` `FintypeCat.instFunLikeHomCarrier` `CategoryTheory.ConcreteCategory.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FintypeCat.concreteCategoryFintype` `CategoryTheory.Functor.map` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—

---

← Back to Index