instCoeFunHomForallCarrierToTopTotallyDisconnectedSpaceToProfinite

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

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

English

The identity morphism on ProfiniteGrp A acts as the identity function on A.

Русский

Идентичный морфизм на ProfiniteGrp A действует как тождественная функция на A.

LaTeX

$$id_apply (A : ProfiniteGrp) (a : A) : (𝟙 A : A ⟶ A) a = a$$

Lean4

@[to_additive]
instance {M N : ProfiniteGrp.{u}} : CoeFun (M ⟶ N) (fun _ ↦ M → N) where coe f := f.hom

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

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

Разделы

Аффилиация

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