Lemmas about subgroups within the permutations (self-equivalences) of a type α #
This file provides extra lemmas about some Subgroups that exist within Equiv.Perm α.
GroupTheory.Subgroup depends on GroupTheory.Perm.Basic, so these need to be in a separate
file.
It also provides decidable instances on membership in these subgroups, since
MonoidHom.decidableMemRange cannot be inferred without the help of a lambda.
The presence of these instances induces a Fintype instance on the QuotientGroup.Quotient of
these subgroups.
instance
Equiv.Perm.sumCongrHom.decidableMemRange
{α : Type u_1}
{β : Type u_2}
[DecidableEq α]
[DecidableEq β]
[Fintype α]
[Fintype β]
:
DecidablePred fun (x : Equiv.Perm (α ⊕ β)) => x ∈ MonoidHom.range (Equiv.Perm.sumCongrHom α β)
Equations
- Equiv.Perm.sumCongrHom.decidableMemRange x = inferInstance
@[simp]
theorem
Equiv.Perm.sumCongrHom.card_range
{α : Type u_1}
{β : Type u_2}
[Fintype ↥(MonoidHom.range (Equiv.Perm.sumCongrHom α β))]
[Fintype (Equiv.Perm α × Equiv.Perm β)]
:
Fintype.card ↥(MonoidHom.range (Equiv.Perm.sumCongrHom α β)) = Fintype.card (Equiv.Perm α × Equiv.Perm β)
instance
Equiv.Perm.sigmaCongrRightHom.decidableMemRange
{α : Type u_1}
{β : α → Type u_2}
[DecidableEq α]
[(a : α) → DecidableEq (β a)]
[Fintype α]
[(a : α) → Fintype (β a)]
:
DecidablePred fun (x : Equiv.Perm ((a : α) × β a)) => x ∈ MonoidHom.range (Equiv.Perm.sigmaCongrRightHom β)
Equations
- Equiv.Perm.sigmaCongrRightHom.decidableMemRange x = inferInstance
@[simp]
theorem
Equiv.Perm.sigmaCongrRightHom.card_range
{α : Type u_1}
{β : α → Type u_2}
[Fintype ↥(MonoidHom.range (Equiv.Perm.sigmaCongrRightHom β))]
[Fintype ((a : α) → Equiv.Perm (β a))]
:
Fintype.card ↥(MonoidHom.range (Equiv.Perm.sigmaCongrRightHom β)) = Fintype.card ((a : α) → Equiv.Perm (β a))
instance
Equiv.Perm.subtypeCongrHom.decidableMemRange
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
[Fintype (Equiv.Perm { a : α // p a } × Equiv.Perm { a : α // ¬p a })]
[DecidableEq (Equiv.Perm α)]
:
DecidablePred fun (x : Equiv.Perm α) => x ∈ MonoidHom.range (Equiv.Perm.subtypeCongrHom p)
Equations
- Equiv.Perm.subtypeCongrHom.decidableMemRange p x = inferInstance
@[simp]
theorem
Equiv.Perm.subtypeCongrHom.card_range
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
[Fintype ↥(MonoidHom.range (Equiv.Perm.subtypeCongrHom p))]
[Fintype (Equiv.Perm { a : α // p a } × Equiv.Perm { a : α // ¬p a })]
:
Fintype.card ↥(MonoidHom.range (Equiv.Perm.subtypeCongrHom p)) = Fintype.card (Equiv.Perm { a : α // p a } × Equiv.Perm { a : α // ¬p a })
noncomputable def
Equiv.Perm.subgroupOfMulAction
(G : Type u_1)
(H : Type u_2)
[Group G]
[MulAction G H]
[FaithfulSMul G H]
:
G ≃* ↥(MonoidHom.range (MulAction.toPermHom G H))
Cayley's theorem: Every group G is isomorphic to a subgroup of the symmetric group acting on
G. Note that we generalize this to an arbitrary "faithful" group action by G. Setting H = G
recovers the usual statement of Cayley's theorem via RightCancelMonoid.faithfulSMul