Lean4
/-- `ProfiniteGrp.limitCone` is a limit cone. -/
def limitConeIsLimit : Limits.IsLimit (limitCone F)
where
lift
cone :=
ofHom
{
((Profinite.limitConeIsLimit (F ⋙ (forget₂ ProfiniteGrp Profinite))).lift
((forget₂ ProfiniteGrp Profinite).mapCone
cone)).hom with
map_one' :=
Subtype.ext
(funext fun j ↦ map_one (cone.π.app j).hom)
-- TODO: investigate whether it's possible to set up `ext` lemmas for the `TopCat`-related
-- categories so that `by ext j; exact map_one (cone.π.app j)` works here, similarly below.
map_mul' := fun _ _ ↦ Subtype.ext (funext fun j ↦ map_mul (cone.π.app j).hom _ _) }
uniq cone m
h := by
apply (forget₂ ProfiniteGrp Profinite).map_injective
simpa using
(Profinite.limitConeIsLimit (F ⋙ (forget₂ ProfiniteGrp Profinite))).uniq
((forget₂ ProfiniteGrp Profinite).mapCone cone) ((forget₂ ProfiniteGrp Profinite).map m)
(fun j ↦ congrArg (forget₂ ProfiniteGrp Profinite).map (h j))
