Group actions on quotients and equivariant homs #
def
MulAction.homEquivProdFixedPoints
{G : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[Group G]
[MulAction G X]
[MulAction G Y]
(σ : X → G)
(hσ : ∀ (a b : X), (orbitRel G X) a b → σ a • a = σ b • b)
:
Given a representative for each orbit of X under G, and for each x : X a choice of σ
that sends x to the representative, we obtain a bijection between G-equivariant homs from X
and the product of Stab(x)-fixed points over each orbit representative x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
MulAction.homEquivProdFixedPoints_symm_apply_apply
{G : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[Group G]
[MulAction G X]
[MulAction G Y]
(σ : X → G)
(hσ : ∀ (a b : X), (orbitRel G X) a b → σ a • a = σ b • b)
(v : (i : ↑(Set.range fun (i : X) => σ i • i)) → ↑(fixedPoints (↥(stabilizer G ↑i)) Y))
(x : X)
:
def
MulAction.sigmaRangeQuotientStabilizer
{G : Type u_1}
{X : Type u_2}
[Group G]
[MulAction G X]
(σ : X → G)
(hσ : ∀ (a b : X), (orbitRel G X) a b → σ a • a = σ b • b)
:
Given a representative for each orbit of X under G, and for each x : X a choice of σ
that sends x to the representative, we obtain a bijection between X and ∐ G/stab(x) where
the disjoint union runs through the representatives.
Equations
- One or more equations did not get rendered due to their size.