colimitTypeRel_iff_orbitRel — Mathlib

English

Explicitly, the limit of J is equivalent to the fixed points under the induced group action on J(star G).

Русский

Явно: предел J эквивалентен фиксированным точкам под индуцированным действием группы на J(star G).

LaTeX

$$$\\text{limitEquivFixedPoints }(J) : \\; \\lim J \\cong \\operatorname{Fix}_G(J(\\mathrm{star} G))$$$

Lean4

/-- The relation used to construct colimits in types for `J : SingleObj G ⥤ Type u` is
equivalent to the `MulAction.orbitRel` equivalence relation on `J.obj (SingleObj.star G)`. -/
theorem colimitTypeRel_iff_orbitRel (x y : J.obj (SingleObj.star G)) :
    J.ColimitTypeRel ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔
      MulAction.orbitRel G (J.obj (SingleObj.star G)) x y :=
  by
  conv => rhs; rw [Setoid.comm']
  change (∃ g : G, y = g • x) ↔ (∃ g : G, g • x = y)
  grind

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