toFiniteQuotientFunctor

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

URI: https://scilib.ai/kg/mathlib#ProfiniteGrp.toFiniteQuotientFunctor

Lean4

/-- The functor from `OpenNormalSubgroup P` to `FiniteGrp` sending `U` to `P ⧸ U`,
where `P : ProfiniteGrp`. -/
def toFiniteQuotientFunctor (P : ProfiniteGrp) : OpenNormalSubgroup P ⥤ FiniteGrp
    where
  obj := fun H => FiniteGrp.of (P ⧸ H.toSubgroup)
  map := fun fHK => FiniteGrp.ofHom (QuotientGroup.map _ _ (.id _) (leOfHom fHK))
  map_id _ := ConcreteCategory.ext <| QuotientGroup.map_id _
  map_comp f
    g := ConcreteCategory.ext <| (QuotientGroup.map_comp_map _ _ _ (.id _) (.id _) (leOfHom f) (leOfHom g)).symm

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru