limitConePtAux

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

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

Lean4

/-- Auxiliary construction to obtain the group structure on the limit of profinite groups. -/
@[to_additive /-- Auxiliary construction to obtain the additive group structure on the limit of
    profinite additive groups. -/
    ]
def limitConePtAux : Subgroup (Π j : J, F.obj j)
    where
  carrier := {x | ∀ ⦃i j : J⦄ (π : i ⟶ j), F.map π (x i) = x j}
  mul_mem' hx hy _ _ π := by simp only [Pi.mul_apply, map_mul, hx π, hy π]
  one_mem' := by simp only [Set.mem_setOf_eq, Pi.one_apply, map_one, implies_true]
  inv_mem' h _ _ π := by simp only [Pi.inv_apply, map_inv, h π]

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

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

Разделы

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

Аффилиация

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