Theorems · Theorem · Lie groups

ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc

∀ {G : GrpCat} {P : ProfiniteGrp.{u}} (f : G ⟶ GrpCat.of ↑P.toProfinite.toTop) {Z : GrpCat}
  (h : (CategoryTheory.forget₂ ProfiniteGrp.{u} GrpCat).obj P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ProfiniteGrp.ProfiniteCompletion.eta G)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.forget₂ ProfiniteGrp.{u} GrpCat).map (ProfiniteGrp.ProfiniteCompletion.lift f)) h) =
    CategoryTheory.CategoryStruct.comp f h

Defined in

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Cited by

0 results in Mathlib

Foundations

Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound