theorem
ClosedPoint.orbitRel_map_of_equivariant
{G : Type u_1}
[Group G]
{C₁ : Type u_2}
{C₂ : Type u_3}
[MulAction G C₁]
[MulAction G C₂]
(φ : C₁ → C₂)
(hφ : ∀ (g : G) (P : C₁), φ (g • P) = g • φ P)
⦃a b : C₁⦄
(hab : (MulAction.orbitRel G C₁) a b)
:
(MulAction.orbitRel G C₂) (φ a) (φ b)
A $G$-equivariant map $\varphi : C_1 \to C_2$ takes points in the same $G$-orbit to points in the same $G$-orbit.
def
ClosedPoint.map
{G : Type u_1}
[Group G]
{C₁ : Type u_2}
{C₂ : Type u_3}
[MulAction G C₁]
[MulAction G C₂]
(φ : C₁ → C₂)
(hφ : ∀ (g : G) (P : C₁), φ (g • P) = g • φ P)
:
ClosedPoint G C₁ → ClosedPoint G C₂
Functoriality of closed points (Galois orbits) under a $G$-equivariant map of underlying sets.