Basic

📁 Source: Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

Statistics

Metric	Count
Definitions ProfiniteAddGrp, hom, hom', addGroup, instAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite, instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteAddGrpCatAddMonoidHomCarrier, instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap, instHasForget₂FiniteAddGrpAddMonoidHomCarrierToAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite, limit, limitCone, limitConeIsLimit, limitConePtAux, of, ofClosedAddSubgroup, ofContinuousAddEquiv, ofFiniteAddGrp, ofFiniteAddGrpHom, ofHom, ofProfinite, pi, toProfinite, toProfiniteGrpIso, hom, hom', group, instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite, instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteGrpCatMonoidHomCarrier, instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap, instHasForget₂FiniteGrpMonoidHomCarrierToGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite, limit, limitCone, limitConeIsLimit, limitConePtAux, of, ofClosedSubgroup, ofContinuousMulEquiv, ofFiniteGrp, ofFiniteGrpHom, ofHom, ofProfinite, pi, toProfinite, instCategoryProfiniteAddGrp, instCategoryProfiniteGrp, instCoeSortProfiniteAddGrpType, instCoeSortProfiniteGrpType, instConcreteCategoryProfiniteAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite, instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite	50
Theorems ext, ext_iff, coe_comp, coe_id, coe_of, comp_apply, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_neg_apply, hom_ofHom, id_apply, instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux, instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, instHasLimit, instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, limit_add_val, limit_ext, limit_ext_iff, limit_zero_val, neg_hom_apply, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, topologicalAddGroup, ext, ext_iff, coe_comp, coe_id, coe_of, comp_apply, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_inv_apply, hom_ofHom, id_apply, instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux, instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, instHasLimit, instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite, instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, inv_hom_apply, limit_ext, limit_ext_iff, limit_mul_val, limit_one_val, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, topologicalGroup	58
Total	108

ProfiniteAddGrp

Definitions

Name	Category	Theorems
addGroup 📖	CompOp	18 math math: ofHom_hom, ofHom_apply, instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, hom_neg_apply, hom_id, neg_hom_apply, limit_zero_val, comp_apply, instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, id_apply, coe_id, limit_add_val, limit_ext_iff, coe_comp, hom_comp, instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux, topologicalAddGroup
instAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap 📖	CompOp	1 math math: instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap
instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite 📖	CompOp	—
instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteAddGrpCatAddMonoidHomCarrier 📖	CompOp	—
instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap 📖	CompOp	3 math math: instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap
instHasForget₂FiniteAddGrpAddMonoidHomCarrierToAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite 📖	CompOp	—
limit 📖	CompOp	2 math math: limit_zero_val, limit_add_val
limitCone 📖	CompOp	—
limitConeIsLimit 📖	CompOp	—
limitConePtAux 📖	CompOp	4 math math: limit_zero_val, limit_add_val, limit_ext_iff, instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux
of 📖	CompOp	5 math math: ofHom_id, ofHom_apply, ofHom_comp, coe_of, hom_ofHom
ofClosedAddSubgroup 📖	CompOp	—
ofContinuousAddEquiv 📖	CompOp	—
ofFiniteAddGrp 📖	CompOp	—
ofFiniteAddGrpHom 📖	CompOp	—
ofHom 📖	CompOp	5 math math: ofHom_hom, ofHom_id, ofHom_apply, ofHom_comp, hom_ofHom
ofProfinite 📖	CompOp	—
pi 📖	CompOp	—
toProfinite 📖	CompOp	19 math math: ofHom_hom, ofHom_apply, instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, hom_neg_apply, hom_id, neg_hom_apply, limit_zero_val, coe_of, comp_apply, instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, id_apply, coe_id, limit_add_val, limit_ext_iff, coe_comp, hom_comp, instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux, topologicalAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe ContinuousAddMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addGroup ContinuousAddMonoidHom.instFunLike Hom.hom CategoryTheory.CategoryStruct.comp ProfiniteAddGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteAddGrp	—	—
coe_id 📖	mathematical	—	DFunLike.coe ContinuousAddMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addGroup ContinuousAddMonoidHom.instFunLike Hom.hom CategoryTheory.CategoryStruct.id ProfiniteAddGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteAddGrp	—	—
coe_of 📖	mathematical	—	TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe ContinuousAddMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addGroup ContinuousAddMonoidHom.instFunLike Hom.hom CategoryTheory.CategoryStruct.comp ProfiniteAddGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteAddGrp	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp ProfiniteAddGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteAddGrp ContinuousAddMonoidHom.comp TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addGroup	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id ProfiniteAddGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteAddGrp ContinuousAddMonoidHom.id TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addGroup	—	—
hom_neg_apply 📖	mathematical	—	DFunLike.coe ContinuousAddMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addGroup ContinuousAddMonoidHom.instFunLike Hom.hom CategoryTheory.Iso.hom ProfiniteAddGrp instCategoryProfiniteAddGrp CategoryTheory.Iso.inv	—	CategoryTheory.Iso.inv_hom_id_apply
hom_ofHom 📖	mathematical	—	Hom.hom of ofHom	—	—
id_apply 📖	mathematical	—	DFunLike.coe ContinuousAddMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addGroup ContinuousAddMonoidHom.instFunLike Hom.hom CategoryTheory.CategoryStruct.id ProfiniteAddGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteAddGrp	—	—
instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux 📖	mathematical	—	CompactSpace AddSubgroup Pi.addGroup TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite CategoryTheory.Functor.obj ProfiniteAddGrp instCategoryProfiniteAddGrp addGroup SetLike.instMembership AddSubgroup.instSetLike limitConePtAux instTopologicalSpaceSubtype Pi.topologicalSpace	—	CompHausLike.is_compact
instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap 📖	mathematical	—	CategoryTheory.Functor.Faithful ProfiniteAddGrp instCategoryProfiniteAddGrp Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.forget₂ ContinuousAddMonoidHom CompHausLike.toTop toProfinite SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addGroup ContinuousAddMonoidHom.instFunLike instConcreteCategoryProfiniteAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite ContinuousMap ContinuousMap.instFunLike CompHausLike.concreteCategory instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap	—	CategoryTheory.ConcreteCategory.hom_ext CategoryTheory.congr_fun
instHasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit ProfiniteAddGrp instCategoryProfiniteAddGrp	—	—
instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap 📖	mathematical	—	IsTopologicalAddGroup TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str CategoryTheory.Limits.Cone.pt Profinite CompHausLike.category CategoryTheory.Functor.comp ProfiniteAddGrp instCategoryProfiniteAddGrp CategoryTheory.forget₂ ContinuousAddMonoidHom toProfinite SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addGroup ContinuousAddMonoidHom.instFunLike instConcreteCategoryProfiniteAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite ContinuousMap ContinuousMap.instFunLike CompHausLike.concreteCategory instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap Profinite.limitCone instAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap	—	AddSubgroup.instIsTopologicalAddGroupSubtypeMem Pi.topologicalAddGroup topologicalAddGroup
instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits ProfiniteAddGrp instCategoryProfiniteAddGrp Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.forget₂ ContinuousAddMonoidHom CompHausLike.toTop toProfinite SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addGroup ContinuousAddMonoidHom.instFunLike instConcreteCategoryProfiniteAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite ContinuousMap ContinuousMap.instFunLike CompHausLike.concreteCategory instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
limit_add_val 📖	mathematical	—	AddSubgroup Pi.addGroup TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite CategoryTheory.Functor.obj ProfiniteAddGrp instCategoryProfiniteAddGrp addGroup SetLike.instMembership AddSubgroup.instSetLike limitConePtAux limit AddSubgroup.add AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—
limit_ext 📖	—	AddSubgroup Pi.addGroup TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite CategoryTheory.Functor.obj ProfiniteAddGrp instCategoryProfiniteAddGrp addGroup SetLike.instMembership AddSubgroup.instSetLike limitConePtAux	—	—	—
limit_ext_iff 📖	mathematical	—	AddSubgroup Pi.addGroup TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite CategoryTheory.Functor.obj ProfiniteAddGrp instCategoryProfiniteAddGrp addGroup SetLike.instMembership AddSubgroup.instSetLike limitConePtAux	—	limit_ext
limit_zero_val 📖	mathematical	—	AddSubgroup Pi.addGroup TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite CategoryTheory.Functor.obj ProfiniteAddGrp instCategoryProfiniteAddGrp addGroup SetLike.instMembership AddSubgroup.instSetLike limitConePtAux limit AddSubgroup.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—
neg_hom_apply 📖	mathematical	—	DFunLike.coe ContinuousAddMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addGroup ContinuousAddMonoidHom.instFunLike Hom.hom CategoryTheory.Iso.inv ProfiniteAddGrp instCategoryProfiniteAddGrp CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
ofHom_apply 📖	mathematical	—	DFunLike.coe ContinuousAddMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite of SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addGroup ContinuousAddMonoidHom.instFunLike Hom.hom ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom ContinuousAddMonoidHom.comp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid CategoryTheory.CategoryStruct.comp ProfiniteAddGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteAddGrp of	—	—
ofHom_hom 📖	mathematical	—	ofHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite addGroup topologicalAddGroup CompHausLike.is_compact Profinite.instTotallyDisconnectedSpaceCarrierToTop Hom.hom	—	topologicalAddGroup CompHausLike.is_compact Profinite.instTotallyDisconnectedSpaceCarrierToTop
ofHom_id 📖	mathematical	—	ofHom ContinuousAddMonoidHom.id SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid CategoryTheory.CategoryStruct.id ProfiniteAddGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteAddGrp of	—	—
topologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite addGroup	—	—

ProfiniteAddGrp.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	12 math math: ProfiniteAddGrp.ofHom_hom, ProfiniteAddGrp.ofHom_apply, ProfiniteAddGrp.hom_neg_apply, ProfiniteAddGrp.hom_id, ProfiniteAddGrp.neg_hom_apply, ProfiniteAddGrp.comp_apply, ProfiniteAddGrp.id_apply, ProfiniteAddGrp.coe_id, ProfiniteAddGrp.coe_comp, ProfiniteAddGrp.hom_ext_iff, ProfiniteAddGrp.hom_ofHom, ProfiniteAddGrp.hom_comp
hom' 📖	CompOp	1 math math: ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom'	—	—	—
ext_iff 📖	mathematical	—	hom'	—	ext

ProfiniteGrp

Definitions

Name	Category	Theorems
group 📖	CompOp	42 math math: instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, limit_one_val, ProfiniteCompletion.lift_eta, coe_id, ProfiniteCompletion.lift_eta_assoc, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, toLimit_surjective, hom_id, denseRange_toLimit, comp_apply, ofHom_hom, topologicalGroup, hom_comp, InfiniteGalois.mulEquivToLimit_symm_continuous, inv_hom_apply, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, cone_pt, InfiniteGalois.proj_adjoin_singleton_val, limit_mul_val, profiniteCompletion_map, hom_inv_apply, cone_π_app, InfiniteGalois.toAlgEquivAux_eq_liftNormal, toLimit_injective, ofHom_apply, instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, coe_comp, InfiniteGalois.mk_toAlgEquivAux, InfiniteGalois.proj_of_le, toLimitFun_continuous, diagram_map, InfiniteGalois.algEquivToLimit_continuous, id_apply, isIso_toLimit, InfiniteGalois.limitToAlgEquiv_symm_apply, instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, limit_ext_iff, instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, diagram_obj, instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite
instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite 📖	CompOp	—
instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap 📖	CompOp	1 math math: instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap
instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteGrpCatMonoidHomCarrier 📖	CompOp	2 math math: ProfiniteCompletion.lift_eta, ProfiniteCompletion.lift_eta_assoc
instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap 📖	CompOp	4 math math: instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap
instHasForget₂FiniteGrpMonoidHomCarrierToGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite 📖	CompOp	2 math math: diagram_map, diagram_obj
limit 📖	CompOp	17 math math: limit_one_val, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, toLimit_surjective, denseRange_toLimit, InfiniteGalois.mulEquivToLimit_symm_continuous, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, InfiniteGalois.proj_adjoin_singleton_val, limit_mul_val, InfiniteGalois.toAlgEquivAux_eq_liftNormal, toLimit_injective, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, InfiniteGalois.mk_toAlgEquivAux, InfiniteGalois.proj_of_le, toLimitFun_continuous, InfiniteGalois.algEquivToLimit_continuous, isIso_toLimit, InfiniteGalois.limitToAlgEquiv_symm_apply
limitCone 📖	CompOp	—
limitConeIsLimit 📖	CompOp	—
limitConePtAux 📖	CompOp	16 math math: limit_one_val, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, denseRange_toLimit, InfiniteGalois.mulEquivToLimit_symm_continuous, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, InfiniteGalois.proj_adjoin_singleton_val, limit_mul_val, InfiniteGalois.toAlgEquivAux_eq_liftNormal, instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, InfiniteGalois.mk_toAlgEquivAux, InfiniteGalois.proj_of_le, toLimitFun_continuous, InfiniteGalois.algEquivToLimit_continuous, InfiniteGalois.limitToAlgEquiv_symm_apply, limit_ext_iff
of 📖	CompOp	5 math math: coe_of, ofHom_comp, ofHom_apply, ofHom_id, hom_ofHom
ofClosedSubgroup 📖	CompOp	—
ofContinuousMulEquiv 📖	CompOp	—
ofFiniteGrp 📖	CompOp	—
ofFiniteGrpHom 📖	CompOp	—
ofHom 📖	CompOp	5 math math: ofHom_comp, ofHom_hom, ofHom_apply, ofHom_id, hom_ofHom
ofProfinite 📖	CompOp	—
pi 📖	CompOp	—
toProfinite 📖	CompOp	44 math math: coe_of, instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, limit_one_val, ProfiniteCompletion.lift_eta, coe_id, ProfiniteCompletion.lift_eta_assoc, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, toLimit_surjective, hom_id, denseRange_toLimit, comp_apply, ofHom_hom, topologicalGroup, hom_comp, InfiniteGalois.mulEquivToLimit_symm_continuous, inv_hom_apply, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, cone_pt, InfiniteGalois.proj_adjoin_singleton_val, limit_mul_val, ProfiniteCompletion.denseRange, profiniteCompletion_map, hom_inv_apply, cone_π_app, InfiniteGalois.toAlgEquivAux_eq_liftNormal, toLimit_injective, ofHom_apply, instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, coe_comp, InfiniteGalois.mk_toAlgEquivAux, InfiniteGalois.proj_of_le, toLimitFun_continuous, diagram_map, InfiniteGalois.algEquivToLimit_continuous, id_apply, isIso_toLimit, InfiniteGalois.limitToAlgEquiv_symm_apply, instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, limit_ext_iff, instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, diagram_obj, instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe ContinuousMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite DivInvMonoid.toMonoid Group.toDivInvMonoid group ContinuousMonoidHom.instFunLike Hom.hom CategoryTheory.CategoryStruct.comp ProfiniteGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteGrp	—	—
coe_id 📖	mathematical	—	DFunLike.coe ContinuousMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite DivInvMonoid.toMonoid Group.toDivInvMonoid group ContinuousMonoidHom.instFunLike Hom.hom CategoryTheory.CategoryStruct.id ProfiniteGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteGrp	—	—
coe_of 📖	mathematical	—	TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe ContinuousMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite DivInvMonoid.toMonoid Group.toDivInvMonoid group ContinuousMonoidHom.instFunLike Hom.hom CategoryTheory.CategoryStruct.comp ProfiniteGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteGrp	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp ProfiniteGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteGrp ContinuousMonoidHom.comp TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite DivInvMonoid.toMonoid Group.toDivInvMonoid group	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id ProfiniteGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteGrp ContinuousMonoidHom.id TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite DivInvMonoid.toMonoid Group.toDivInvMonoid group	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe ContinuousMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite DivInvMonoid.toMonoid Group.toDivInvMonoid group ContinuousMonoidHom.instFunLike Hom.hom CategoryTheory.Iso.hom ProfiniteGrp instCategoryProfiniteGrp CategoryTheory.Iso.inv	—	CategoryTheory.Iso.inv_hom_id_apply
hom_ofHom 📖	mathematical	—	Hom.hom of ofHom	—	—
id_apply 📖	mathematical	—	DFunLike.coe ContinuousMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite DivInvMonoid.toMonoid Group.toDivInvMonoid group ContinuousMonoidHom.instFunLike Hom.hom CategoryTheory.CategoryStruct.id ProfiniteGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteGrp	—	—
instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux 📖	mathematical	—	CompactSpace Subgroup Pi.group TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp group SetLike.instMembership Subgroup.instSetLike limitConePtAux instTopologicalSpaceSubtype Pi.topologicalSpace	—	CompHausLike.is_compact
instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap 📖	mathematical	—	CategoryTheory.Functor.Faithful ProfiniteGrp instCategoryProfiniteGrp Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.forget₂ ContinuousMonoidHom CompHausLike.toTop toProfinite DivInvMonoid.toMonoid Group.toDivInvMonoid group ContinuousMonoidHom.instFunLike instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite ContinuousMap ContinuousMap.instFunLike CompHausLike.concreteCategory instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap	—	CategoryTheory.ConcreteCategory.hom_ext CategoryTheory.congr_fun
instHasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit ProfiniteGrp instCategoryProfiniteGrp	—	—
instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap 📖	mathematical	—	IsTopologicalGroup TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str CategoryTheory.Limits.Cone.pt Profinite CompHausLike.category CategoryTheory.Functor.comp ProfiniteGrp instCategoryProfiniteGrp CategoryTheory.forget₂ ContinuousMonoidHom toProfinite DivInvMonoid.toMonoid Group.toDivInvMonoid group ContinuousMonoidHom.instFunLike instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite ContinuousMap ContinuousMap.instFunLike CompHausLike.concreteCategory instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap Profinite.limitCone instGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap	—	Subgroup.instIsTopologicalGroupSubtypeMem Pi.topologicalGroup topologicalGroup
instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits ProfiniteGrp instCategoryProfiniteGrp Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.forget₂ ContinuousMonoidHom CompHausLike.toTop toProfinite DivInvMonoid.toMonoid Group.toDivInvMonoid group ContinuousMonoidHom.instFunLike instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite ContinuousMap ContinuousMap.instFunLike CompHausLike.concreteCategory instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms ProfiniteGrp instCategoryProfiniteGrp CategoryTheory.types CategoryTheory.forget ContinuousMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite DivInvMonoid.toMonoid Group.toDivInvMonoid group ContinuousMonoidHom.instFunLike instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite	—	CategoryTheory.reflectsIsomorphisms_comp instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap CompHausLike.forget_reflectsIsomorphisms
instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms ProfiniteGrp instCategoryProfiniteGrp Profinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str CategoryTheory.forget₂ ContinuousMonoidHom CompHausLike.toTop toProfinite DivInvMonoid.toMonoid Group.toDivInvMonoid group ContinuousMonoidHom.instFunLike instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite ContinuousMap ContinuousMap.instFunLike CompHausLike.concreteCategory instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap	—	map_mul MonoidHomClass.toMulHomClass ContinuousMonoidHom.instMonoidHomClass Homeomorph.continuous_toFun Homeomorph.continuous_invFun CategoryTheory.Iso.isIso_hom
inv_hom_apply 📖	mathematical	—	DFunLike.coe ContinuousMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite DivInvMonoid.toMonoid Group.toDivInvMonoid group ContinuousMonoidHom.instFunLike Hom.hom CategoryTheory.Iso.inv ProfiniteGrp instCategoryProfiniteGrp CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
limit_ext 📖	—	Subgroup Pi.group TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp group SetLike.instMembership Subgroup.instSetLike limitConePtAux	—	—	—
limit_ext_iff 📖	mathematical	—	Subgroup Pi.group TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp group SetLike.instMembership Subgroup.instSetLike limitConePtAux	—	limit_ext
limit_mul_val 📖	mathematical	—	Subgroup Pi.group TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp group SetLike.instMembership Subgroup.instSetLike limitConePtAux limit Subgroup.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
limit_one_val 📖	mathematical	—	Subgroup Pi.group TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite CategoryTheory.Functor.obj ProfiniteGrp instCategoryProfiniteGrp group SetLike.instMembership Subgroup.instSetLike limitConePtAux limit Subgroup.one InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
ofHom_apply 📖	mathematical	—	DFunLike.coe ContinuousMonoidHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite of DivInvMonoid.toMonoid Group.toDivInvMonoid group ContinuousMonoidHom.instFunLike Hom.hom ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom ContinuousMonoidHom.comp DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.comp ProfiniteGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteGrp of	—	—
ofHom_hom 📖	mathematical	—	ofHom TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite group topologicalGroup CompHausLike.is_compact Profinite.instTotallyDisconnectedSpaceCarrierToTop Hom.hom	—	topologicalGroup CompHausLike.is_compact Profinite.instTotallyDisconnectedSpaceCarrierToTop
ofHom_id 📖	mathematical	—	ofHom ContinuousMonoidHom.id DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.CategoryStruct.id ProfiniteGrp CategoryTheory.Category.toCategoryStruct instCategoryProfiniteGrp of	—	—
topologicalGroup 📖	mathematical	—	IsTopologicalGroup TopCat.carrier CompHausLike.toTop TotallyDisconnectedSpace TopCat.str toProfinite group	—	—

ProfiniteGrp.ContinuousMulEquiv

Definitions

Name	Category	Theorems
toProfiniteGrpIso 📖	CompOp	—

ProfiniteGrp.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	15 math math: ProfiniteGrp.coe_id, ProfiniteGrp.toLimit_surjective, ProfiniteGrp.hom_id, ProfiniteGrp.denseRange_toLimit, ProfiniteGrp.comp_apply, ProfiniteGrp.ofHom_hom, ProfiniteGrp.hom_comp, ProfiniteGrp.inv_hom_apply, ProfiniteGrp.hom_inv_apply, ProfiniteGrp.toLimit_injective, ProfiniteGrp.ofHom_apply, ProfiniteGrp.coe_comp, ProfiniteGrp.hom_ext_iff, ProfiniteGrp.id_apply, ProfiniteGrp.hom_ofHom
hom' 📖	CompOp	1 math math: ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom'	—	—	—
ext_iff 📖	mathematical	—	hom'	—	ext

(root)

Definitions

Name	Category	Theorems
ProfiniteAddGrp 📖	CompData	18 math math: ProfiniteAddGrp.ofHom_id, ProfiniteAddGrp.instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteAddGrp.hom_neg_apply, ProfiniteAddGrp.hom_id, ProfiniteAddGrp.ofHom_comp, ProfiniteAddGrp.neg_hom_apply, ProfiniteAddGrp.limit_zero_val, ProfiniteAddGrp.comp_apply, ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, ProfiniteAddGrp.id_apply, ProfiniteAddGrp.coe_id, ProfiniteAddGrp.limit_add_val, ProfiniteAddGrp.limit_ext_iff, ProfiniteAddGrp.coe_comp, ProfiniteAddGrp.hom_comp, ProfiniteAddGrp.instHasLimit, ProfiniteAddGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux
instCategoryProfiniteAddGrp 📖	CompOp	18 math math: ProfiniteAddGrp.ofHom_id, ProfiniteAddGrp.instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteAddGrp.hom_neg_apply, ProfiniteAddGrp.hom_id, ProfiniteAddGrp.ofHom_comp, ProfiniteAddGrp.neg_hom_apply, ProfiniteAddGrp.limit_zero_val, ProfiniteAddGrp.comp_apply, ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, ProfiniteAddGrp.id_apply, ProfiniteAddGrp.coe_id, ProfiniteAddGrp.limit_add_val, ProfiniteAddGrp.limit_ext_iff, ProfiniteAddGrp.coe_comp, ProfiniteAddGrp.hom_comp, ProfiniteAddGrp.instHasLimit, ProfiniteAddGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux
instCategoryProfiniteGrp 📖	CompOp	41 math math: ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteGrp.ofHom_comp, ProfiniteGrp.limit_one_val, ProfiniteGrp.ProfiniteCompletion.lift_eta, ProfiniteGrp.coe_id, ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, ProfiniteGrp.instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteGrp.hom_id, ProfiniteGrp.denseRange_toLimit, ProfiniteGrp.instHasLimit, ProfiniteGrp.comp_apply, ProfiniteGrp.hom_comp, InfiniteGalois.mulEquivToLimit_symm_continuous, ProfiniteGrp.inv_hom_apply, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, ProfiniteGrp.cone_pt, InfiniteGalois.proj_adjoin_singleton_val, ProfiniteGrp.limit_mul_val, ProfiniteGrp.profiniteCompletion_map, ProfiniteGrp.hom_inv_apply, ProfiniteGrp.cone_π_app, InfiniteGalois.toAlgEquivAux_eq_liftNormal, ProfiniteGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, ProfiniteGrp.ofHom_id, ProfiniteGrp.coe_comp, InfiniteGalois.mk_toAlgEquivAux, InfiniteGalois.proj_of_le, ProfiniteGrp.toLimitFun_continuous, ProfiniteGrp.diagram_map, InfiniteGalois.algEquivToLimit_continuous, ProfiniteGrp.id_apply, ProfiniteGrp.isIso_toLimit, InfiniteGalois.limitToAlgEquiv_symm_apply, ProfiniteGrp.profiniteCompletion_obj, ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteGrp.limit_ext_iff, ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, ProfiniteGrp.diagram_obj, ProfiniteGrp.instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite
instCoeSortProfiniteAddGrpType 📖	CompOp	—
instCoeSortProfiniteGrpType 📖	CompOp	—
instConcreteCategoryProfiniteAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite 📖	CompOp	3 math math: ProfiniteAddGrp.instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap
instConcreteCategoryProfiniteGrpContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite 📖	CompOp	9 math math: ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteGrp.ProfiniteCompletion.lift_eta, ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc, ProfiniteGrp.instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteGrp.diagram_map, ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, ProfiniteGrp.diagram_obj, ProfiniteGrp.instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite

---

← Back to Index