# Monoids of endomorphisms, groups of automorphisms #

This file defines

- the endomorphism monoid structure on `Function.End α := α → α`
- the endomorphism monoid structure on `Monoid.End M := M →* M` and `AddMonoid.End M := M →+ M`
- the automorphism group structure on `Equiv.Perm α := α ≃ α`
- the automorphism group structure on `MulAut M := M ≃* M` and `AddAut M := M ≃+ M`.

## Implementation notes #

The definition of multiplication in the endomorphism monoids and automorphism groups agrees with function composition, and multiplication in `CategoryTheory.End`, but not with `CategoryTheory.comp`.

## Tags #

end monoid, aut group

### Type endomorphisms #

source
def Function.End (α : Type u_4) :
Type u_4

The monoid of endomorphisms.

Note that this is generalized by `CategoryTheory.End` to categories other than `Type u`.

Equations

- Function.End α = (α → α)

Instances For

source
instance instMonoidEnd {α : Type u_4} :
Monoid (Function.End α)
Equations

- One or more equations did not get rendered due to their size.

source
instance instInhabitedEnd {α : Type u_4} :
Inhabited (Function.End α)
Equations

- instInhabitedEnd = { default := 1 }

### Monoid endomorphisms #

source
instance Equiv.Perm.instOne {α : Type u_4} :
One (Perm α)
Equations

- Equiv.Perm.instOne = { one := Equiv.refl α }

source
instance Equiv.Perm.instMul {α : Type u_4} :
Mul (Perm α)
Equations

- Equiv.Perm.instMul = { mul := fun (f g : Equiv.Perm α) => Equiv.trans g f }

source
instance Equiv.Perm.instInv {α : Type u_4} :
Inv (Perm α)
Equations

- Equiv.Perm.instInv = { inv := Equiv.symm }

source
instance Equiv.Perm.instPowNat {α : Type u_4} :
Pow (Perm α) ℕ
Equations

- Equiv.Perm.instPowNat = { pow := fun (f : Equiv.Perm α) (n : ℕ) => { toFun := (⇑f)^[n], invFun := (⇑(Equiv.symm f))^[n], left_inv := ⋯, right_inv := ⋯ } }

source
instance Equiv.Perm.permGroup {α : Type u_4} :
Group (Perm α)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem Equiv.Perm.default_eq {α : Type u_4} :
default = 1
source
def Equiv.Perm.equivUnitsEnd {α : Type u_4} :
Perm α ≃* (Function.End α)ˣ

The permutation of a type is equivalent to the units group of the endomorphisms monoid of this type.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Equiv.Perm.equivUnitsEnd_symm_apply_apply {α : Type u_4} (u : (Function.End α)ˣ) :
⇑(equivUnitsEnd.symm u) = ↑u
source
@[simp]
theorem Equiv.Perm.val_equivUnitsEnd_apply {α : Type u_4} (e : Perm α) (a : α) :
↑(equivUnitsEnd e) a = e a
source
@[simp]
theorem Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply {α : Type u_4} (u : (Function.End α)ˣ) :
⇑(Equiv.symm (equivUnitsEnd.symm u)) = ↑u⁻¹
source
@[simp]
theorem Equiv.Perm.val_inv_equivUnitsEnd_apply {α : Type u_4} (e : Perm α) (a : α) :
↑(equivUnitsEnd e)⁻¹ a = (Equiv.symm e) a
source
def MonoidHom.toHomPerm {α : Type u_4} {G : Type u_7} [Group G] (f : G →* Function.End α) :
G →* Equiv.Perm α

Lift a monoid homomorphism `f : G →* Function.End α` to a monoid homomorphism `f : G →* Equiv.Perm α`.

Equations

- f.toHomPerm = Equiv.Perm.equivUnitsEnd.symm.toMonoidHom.comp f.toHomUnits

Instances For

source
@[simp]
theorem MonoidHom.toHomPerm_apply_apply {α : Type u_4} {G : Type u_7} [Group G] (f : G →* Function.End α) (a✝ : G) :
⇑(f.toHomPerm a✝) = f a✝
source
@[simp]
theorem MonoidHom.toHomPerm_apply_symm_apply {α : Type u_4} {G : Type u_7} [Group G] (f : G →* Function.End α) (a✝ : G) :
⇑(Equiv.symm (f.toHomPerm a✝)) = ↑(f.toHomUnits a✝)⁻¹
source
theorem Equiv.Perm.mul_apply {α : Type u_4} (f g : Perm α) (x : α) :
(f * g) x = f (g x)
source
theorem Equiv.Perm.one_apply {α : Type u_4} (x : α) :
1 x = x
source
@[simp]
theorem Equiv.Perm.inv_apply_self {α : Type u_4} (f : Perm α) (x : α) :
f⁻¹ (f x) = x
source
@[simp]
theorem Equiv.Perm.apply_inv_self {α : Type u_4} (f : Perm α) (x : α) :
f (f⁻¹ x) = x
source
theorem Equiv.Perm.one_def {α : Type u_4} :
1 = Equiv.refl α
source
theorem Equiv.Perm.mul_def {α : Type u_4} (f g : Perm α) :
f * g = Equiv.trans g f
source
theorem Equiv.Perm.inv_def {α : Type u_4} (f : Perm α) :
f⁻¹ = Equiv.symm f
source
@[simp]
theorem Equiv.Perm.coe_one {α : Type u_4} :
⇑1 = id
source
@[simp]
theorem Equiv.Perm.coe_mul {α : Type u_4} (f g : Perm α) :
⇑(f * g) = ⇑f ∘ ⇑g
source
theorem Equiv.Perm.coe_pow {α : Type u_4} (f : Perm α) (n : ℕ) :
⇑(f ^ n) = (⇑f)^[n]
source
@[simp]
theorem Equiv.Perm.iterate_eq_pow {α : Type u_4} (f : Perm α) (n : ℕ) :
(⇑f)^[n] = ⇑(f ^ n)
source
theorem Equiv.Perm.eq_inv_iff_eq {α : Type u_4} {f : Perm α} {x y : α} :
x = f⁻¹ y ↔ f x = y
source
theorem Equiv.Perm.inv_eq_iff_eq {α : Type u_4} {f : Perm α} {x y : α} :
f⁻¹ x = y ↔ x = f y
source
theorem Equiv.Perm.zpow_apply_comm {α : Type u_7} (σ : Perm α) (m n : ℤ) {x : α} :
(σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x)

Lemmas about mixing `Perm` with `Equiv`. Because we have multiple ways to express `Equiv.refl`, `Equiv.symm`, and `Equiv.trans`, we want simp lemmas for every combination. The assumption made here is that if you're using the group structure, you want to preserve it after simp.

source
@[simp]
theorem Equiv.Perm.trans_one {α : Sort u_7} {β : Type u_8} (e : α ≃ β) :
e.trans 1 = e
source
@[simp]
theorem Equiv.Perm.mul_refl {α : Type u_4} (e : Perm α) :
e * Equiv.refl α = e
source
@[simp]
theorem Equiv.Perm.one_symm {α : Type u_4} :
Equiv.symm 1 = 1
source
@[simp]
theorem Equiv.Perm.refl_inv {α : Type u_4} :
(Equiv.refl α)⁻¹ = 1
source
@[simp]
theorem Equiv.Perm.one_trans {α : Type u_7} {β : Sort u_8} (e : α ≃ β) :
Equiv.trans 1 e = e
source
@[simp]
theorem Equiv.Perm.refl_mul {α : Type u_4} (e : Perm α) :
Equiv.refl α * e = e
source
@[simp]
theorem Equiv.Perm.inv_trans_self {α : Type u_4} (e : Perm α) :
Equiv.trans e⁻¹ e = 1
source
@[simp]
theorem Equiv.Perm.mul_symm {α : Type u_4} (e : Perm α) :
e * Equiv.symm e = 1
source
@[simp]
theorem Equiv.Perm.self_trans_inv {α : Type u_4} (e : Perm α) :
Equiv.trans e e⁻¹ = 1
source
@[simp]
theorem Equiv.Perm.symm_mul {α : Type u_4} (e : Perm α) :
Equiv.symm e * e = 1

Lemmas about `Equiv.Perm.sumCongr` re-expressed via the group structure.

source
@[simp]
theorem Equiv.Perm.sumCongr_mul {α : Type u_7} {β : Type u_8} (e : Perm α) (f : Perm β) (g : Perm α) (h : Perm β) :
e.sumCongr f * g.sumCongr h = (e * g).sumCongr (f * h)
source
@[simp]
theorem Equiv.Perm.sumCongr_inv {α : Type u_7} {β : Type u_8} (e : Perm α) (f : Perm β) :
(e.sumCongr f)⁻¹ = e⁻¹.sumCongr f⁻¹
source
@[simp]
theorem Equiv.Perm.sumCongr_one {α : Type u_7} {β : Type u_8} :
sumCongr 1 1 = 1
source
def Equiv.Perm.sumCongrHom (α : Type u_7) (β : Type u_8) :
Perm α × Perm β →* Perm (α ⊕ β)

`Equiv.Perm.sumCongr` as a `MonoidHom`, with its two arguments bundled into a single `Prod`.

This is particularly useful for its `MonoidHom.range` projection, which is the subgroup of permutations which do not exchange elements between `α` and `β`.

Equations

- Equiv.Perm.sumCongrHom α β = { toFun := fun (a : Equiv.Perm α × Equiv.Perm β) => a.1.sumCongr a.2, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem Equiv.Perm.sumCongrHom_apply (α : Type u_7) (β : Type u_8) (a : Perm α × Perm β) :
(sumCongrHom α β) a = a.1.sumCongr a.2
source
theorem Equiv.Perm.sumCongrHom_injective {α : Type u_7} {β : Type u_8} :
Function.Injective ⇑(sumCongrHom α β)
source
@[simp]
theorem Equiv.Perm.sumCongr_swap_one {α : Type u_7} {β : Type u_8} [DecidableEq α] [DecidableEq β] (i j : α) :
(swap i j).sumCongr 1 = swap (Sum.inl i) (Sum.inl j)
source
@[simp]
theorem Equiv.Perm.sumCongr_one_swap {α : Type u_7} {β : Type u_8} [DecidableEq α] [DecidableEq β] (i j : β) :
sumCongr 1 (swap i j) = swap (Sum.inr i) (Sum.inr j)

Lemmas about `Equiv.Perm.sigmaCongrRight` re-expressed via the group structure.

source
@[simp]
theorem Equiv.Perm.sigmaCongrRight_mul {α : Type u_7} {β : α → Type u_8} (F G : (a : α) → Perm (β a)) :
sigmaCongrRight F * sigmaCongrRight G = sigmaCongrRight (F * G)
source
@[simp]
theorem Equiv.Perm.sigmaCongrRight_inv {α : Type u_7} {β : α → Type u_8} (F : (a : α) → Perm (β a)) :
(sigmaCongrRight F)⁻¹ = sigmaCongrRight fun (a : α) => (F a)⁻¹
source
@[simp]
theorem Equiv.Perm.sigmaCongrRight_one {α : Type u_7} {β : α → Type u_8} :
sigmaCongrRight 1 = 1
source
def Equiv.Perm.sigmaCongrRightHom {α : Type u_7} (β : α → Type u_8) :
((a : α) → Perm (β a)) →* Perm ((a : α) × β a)

`Equiv.Perm.sigmaCongrRight` as a `MonoidHom`.

This is particularly useful for its `MonoidHom.range` projection, which is the subgroup of permutations which do not exchange elements between fibers.

Equations

- Equiv.Perm.sigmaCongrRightHom β = { toFun := Equiv.Perm.sigmaCongrRight, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem Equiv.Perm.sigmaCongrRightHom_apply {α : Type u_7} (β : α → Type u_8) (F : (a : α) → Perm (β a)) :
(sigmaCongrRightHom β) F = sigmaCongrRight F
source
theorem Equiv.Perm.sigmaCongrRightHom_injective {α : Type u_7} {β : α → Type u_8} :
Function.Injective ⇑(sigmaCongrRightHom β)
source
def Equiv.Perm.subtypeCongrHom {α : Type u_4} (p : α → Prop) [DecidablePred p] :
Perm { a : α // p a } × Perm { a : α // ¬p a } →* Perm α

`Equiv.Perm.subtypeCongr` as a `MonoidHom`.

Equations

- Equiv.Perm.subtypeCongrHom p = { toFun := fun (pair : Equiv.Perm { a : α // p a } × Equiv.Perm { a : α // ¬p a }) => pair.1.subtypeCongr pair.2, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem Equiv.Perm.subtypeCongrHom_apply {α : Type u_4} (p : α → Prop) [DecidablePred p] (pair : Perm { a : α // p a } × Perm { a : α // ¬p a }) :
(subtypeCongrHom p) pair = pair.1.subtypeCongr pair.2
source
theorem Equiv.Perm.subtypeCongrHom_injective {α : Type u_4} (p : α → Prop) [DecidablePred p] :
Function.Injective ⇑(subtypeCongrHom p)
source
@[simp]
theorem Equiv.permCongr_eq_mul {α : Type u_4} (e p : Perm α) :
(permCongr e) p = e * p * e⁻¹

If `e` is also a permutation, we can write `permCongr` completely in terms of the group structure.

source
@[deprecated Equiv.permCongr_eq_mul (since := "2025-08-29")]
theorem Equiv.Perm.permCongr_eq_mul {α : Type u_4} (e p : Perm α) :
(permCongr e) p = e * p * e⁻¹

Alias of `Equiv.permCongr_eq_mul`.

If `e` is also a permutation, we can write `permCongr` completely in terms of the group structure.

source
@[simp]
theorem Equiv.permCongr_mul {α : Type u_4} {β : Type u_5} (e : α ≃ β) (p q : Perm α) :
e.permCongr (p * q) = e.permCongr p * e.permCongr q
source
def Equiv.permCongrHom {α : Type u_4} {β : Type u_5} (e : α ≃ β) :
Perm α ≃* Perm β

If `α` is equivalent to `β`, then `Perm α` is equivalent to `Perm β`.

Equations

- e.permCongrHom = { toEquiv := e.permCongr, map_mul' := ⋯ }

Instances For

source
@[deprecated Equiv.permCongrHom (since := "2025-08-23")]
def Equiv.Perm.permCongrHom {α : Type u_4} {β : Type u_5} (e : α ≃ β) :
Perm α ≃* Perm β

Alias of `Equiv.permCongrHom`.

If `α` is equivalent to `β`, then `Perm α` is equivalent to `Perm β`.

Equations

- @Equiv.Perm.permCongrHom = @Equiv.permCongrHom

Instances For

source
@[simp]
theorem Equiv.permCongrHom_symm {α : Type u_4} {β : Type u_5} (e : α ≃ β) :
e.permCongrHom.symm = e.symm.permCongrHom
source
@[simp]
theorem Equiv.permCongrHom_trans {α : Type u_4} {β : Type u_5} {γ : Type u_6} (e : α ≃ β) (e' : β ≃ γ) :
e.permCongrHom.trans e'.permCongrHom = (e.trans e').permCongrHom
source
@[simp]
theorem Equiv.permCongrHom_coe_equiv {α : Type u_4} {β : Type u_5} (e : α ≃ β) :
↑e.permCongrHom = e.permCongr
source
@[simp]
theorem Equiv.permCongrHom_coe {α : Type u_4} {β : Type u_5} (e : α ≃ β) :
⇑e.permCongrHom = ⇑e.permCongr

Lemmas about `Equiv.Perm.extendDomain` re-expressed via the group structure.

source
@[simp]
theorem Equiv.Perm.extendDomain_one {α : Type u_4} {β : Type u_5} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) :
extendDomain 1 f = 1
source
@[simp]
theorem Equiv.Perm.extendDomain_inv {α : Type u_4} {β : Type u_5} (e : Perm α) {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) :
(e.extendDomain f)⁻¹ = e⁻¹.extendDomain f
source
@[simp]
theorem Equiv.Perm.extendDomain_mul {α : Type u_4} {β : Type u_5} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) (e e' : Perm α) :
e.extendDomain f * e'.extendDomain f = (e * e').extendDomain f
source
def Equiv.Perm.extendDomainHom {α : Type u_4} {β : Type u_5} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) :
Perm α →* Perm β

`extendDomain` as a group homomorphism

Equations

- Equiv.Perm.extendDomainHom f = { toFun := fun (e : Equiv.Perm α) => e.extendDomain f, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem Equiv.Perm.extendDomainHom_apply {α : Type u_4} {β : Type u_5} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) (e : Perm α) :
(extendDomainHom f) e = e.extendDomain f
source
theorem Equiv.Perm.extendDomainHom_injective {α : Type u_4} {β : Type u_5} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) :
Function.Injective ⇑(extendDomainHom f)
source
@[simp]
theorem Equiv.Perm.extendDomain_eq_one_iff {α : Type u_4} {β : Type u_5} {p : β → Prop} [DecidablePred p] {e : Perm α} {f : α ≃ Subtype p} :
e.extendDomain f = 1 ↔ e = 1
source
@[simp]
theorem Equiv.Perm.extendDomain_pow {α : Type u_4} {β : Type u_5} (e : Perm α) {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) (n : ℕ) :
(e ^ n).extendDomain f = e.extendDomain f ^ n
source
@[simp]
theorem Equiv.Perm.extendDomain_zpow {α : Type u_4} {β : Type u_5} (e : Perm α) {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) (n : ℤ) :
(e ^ n).extendDomain f = e.extendDomain f ^ n
source
def Equiv.Perm.subtypePerm {α : Type u_4} {p : α → Prop} (f : Perm α) (h : ∀ (x : α), p (f x) ↔ p x) :
Perm { x : α // p x }

If the permutation `f` fixes the subtype `{x // p x}`, then this returns the permutation on `{x // p x}` induced by `f`.

Equations

- f.subtypePerm h = { toFun := fun (x : { x : α // p x }) => ⟨f ↑x, ⋯⟩, invFun := fun (x : { x : α // p x }) => ⟨f⁻¹ ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Equiv.Perm.subtypePerm_apply {α : Type u_4} {p : α → Prop} (f : Perm α) (h : ∀ (x : α), p (f x) ↔ p x) (x : { x : α // p x }) :
(f.subtypePerm h) x = ⟨f ↑x, ⋯⟩
source
@[simp]
theorem Equiv.Perm.subtypePerm_one {α : Type u_4} (p : α → Prop) (h : ∀ (x : α), p (1 x) ↔ p (1 x) := ⋯) :
subtypePerm 1 h = 1
source
@[simp]
theorem Equiv.Perm.subtypePerm_mul {α : Type u_4} {p : α → Prop} (f g : Perm α) (hf : ∀ (x : α), p (f x) ↔ p x) (hg : ∀ (x : α), p (g x) ↔ p x) :
f.subtypePerm hf * g.subtypePerm hg = (f * g).subtypePerm ⋯
source
theorem Equiv.Perm.subtypePerm_inv {α : Type u_4} {p : α → Prop} (f : Perm α) (hf : ∀ (x : α), p (f⁻¹ x) ↔ p x) :
f⁻¹.subtypePerm hf = (f.subtypePerm ⋯)⁻¹

See `Equiv.Perm.inv_subtypePerm`.

source
@[simp]
theorem Equiv.Perm.inv_subtypePerm {α : Type u_4} {p : α → Prop} (f : Perm α) (hf : ∀ (x : α), p (f x) ↔ p x) :
(f.subtypePerm hf)⁻¹ = f⁻¹.subtypePerm ⋯

See `Equiv.Perm.subtypePerm_inv`.

source
@[simp]
theorem Equiv.Perm.subtypePerm_pow {α : Type u_4} {p : α → Prop} (f : Perm α) (n : ℕ) (hf : ∀ (x : α), p (f x) ↔ p x) :
f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
source
@[simp]
theorem Equiv.Perm.subtypePerm_zpow {α : Type u_4} {p : α → Prop} (f : Perm α) (n : ℤ) (hf : ∀ (x : α), p (f x) ↔ p x) :
f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
source
def Equiv.Perm.ofSubtype {α : Type u_4} {p : α → Prop} [DecidablePred p] :
Perm (Subtype p) →* Perm α

The inclusion map of permutations on a subtype of `α` into permutations of `α`, fixing the other points.

Equations

- Equiv.Perm.ofSubtype = { toFun := fun (f : Equiv.Perm (Subtype p)) => f.extendDomain (Equiv.refl (Subtype p)), map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
theorem Equiv.Perm.ofSubtype_subtypePerm {α : Type u_4} {p : α → Prop} [DecidablePred p] {f : Perm α} (h₁ : ∀ (x : α), p (f x) ↔ p x) (h₂ : ∀ (x : α), f x ≠ x → p x) :
ofSubtype (f.subtypePerm h₁) = f
source
theorem Equiv.Perm.ofSubtype_apply_of_mem {α : Type u_4} {p : α → Prop} [DecidablePred p] {a : α} (f : Perm (Subtype p)) (ha : p a) :
(ofSubtype f) a = ↑(f ⟨a, ha⟩)
source
@[simp]
theorem Equiv.Perm.ofSubtype_apply_coe {α : Type u_4} {p : α → Prop} [DecidablePred p] (f : Perm (Subtype p)) (x : Subtype p) :
(ofSubtype f) ↑x = ↑(f x)
source
theorem Equiv.Perm.ofSubtype_apply_of_not_mem {α : Type u_4} {p : α → Prop} [DecidablePred p] {a : α} (f : Perm (Subtype p)) (ha : ¬p a) :
(ofSubtype f) a = a
source
theorem Equiv.Perm.ofSubtype_apply_mem_iff_mem {α : Type u_4} {p : α → Prop} [DecidablePred p] (f : Perm (Subtype p)) (x : α) :
p ((ofSubtype f) x) ↔ p x
source
theorem Equiv.Perm.ofSubtype_injective {α : Type u_4} {p : α → Prop} [DecidablePred p] :
Function.Injective ⇑ofSubtype
source
@[simp]
theorem Equiv.Perm.subtypePerm_ofSubtype {α : Type u_4} {p : α → Prop} [DecidablePred p] (f : Perm (Subtype p)) :
(ofSubtype f).subtypePerm ⋯ = f
source
theorem Equiv.Perm.ofSubtype_subtypePerm_of_mem {α : Type u_4} {p : α → Prop} [DecidablePred p] {g : Perm α} (hg : ∀ (x : α), p (g x) ↔ p x) {a : α} (ha : p a) :
(ofSubtype (g.subtypePerm hg)) a = g a
source
theorem Equiv.Perm.ofSubtype_subtypePerm_of_not_mem {α : Type u_4} {p : α → Prop} [DecidablePred p] {g : Perm α} (hg : ∀ (x : α), p (g x) ↔ p x) {a : α} (ha : ¬p a) :
(ofSubtype (g.subtypePerm hg)) a = a
source
def Equiv.Perm.subtypeEquivSubtypePerm {α : Type u_4} (p : α → Prop) [DecidablePred p] :
Perm (Subtype p) ≃ { f : Perm α // ∀ (a : α), ¬p a → f a = a }

Permutations on a subtype are equivalent to permutations on the original type that fix pointwise the rest.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Equiv.Perm.subtypeEquivSubtypePerm_apply_coe {α : Type u_4} (p : α → Prop) [DecidablePred p] (f : Perm (Subtype p)) :
↑((Perm.subtypeEquivSubtypePerm p) f) = ofSubtype f
source
@[simp]
theorem Equiv.Perm.subtypeEquivSubtypePerm_symm_apply {α : Type u_4} (p : α → Prop) [DecidablePred p] (f : { f : Perm α // ∀ (a : α), ¬p a → f a = a }) :
(Perm.subtypeEquivSubtypePerm p).symm f = (↑f).subtypePerm ⋯
source
theorem Equiv.Perm.subtypeEquivSubtypePerm_apply_of_mem {α : Type u_4} {p : α → Prop} [DecidablePred p] {a : α} (f : Perm (Subtype p)) (h : p a) :
↑((Perm.subtypeEquivSubtypePerm p) f) a = ↑(f ⟨a, h⟩)
source
theorem Equiv.Perm.subtypeEquivSubtypePerm_apply_of_not_mem {α : Type u_4} {p : α → Prop} [DecidablePred p] {a : α} (f : Perm (Subtype p)) (h : ¬p a) :
↑((Perm.subtypeEquivSubtypePerm p) f) a = a
source
@[simp]
theorem Equiv.swap_inv {α : Type u_4} [DecidableEq α] (x y : α) :
(swap x y)⁻¹ = swap x y
source
@[simp]
theorem Equiv.swap_mul_self {α : Type u_4} [DecidableEq α] (i j : α) :
swap i j * swap i j = 1
source
theorem Equiv.swap_mul_eq_mul_swap {α : Type u_4} [DecidableEq α] (f : Perm α) (x y : α) :
swap x y * f = f * swap (f⁻¹ x) (f⁻¹ y)
source
theorem Equiv.mul_swap_eq_swap_mul {α : Type u_4} [DecidableEq α] (f : Perm α) (x y : α) :
f * swap x y = swap (f x) (f y) * f
source
theorem Equiv.swap_apply_apply {α : Type u_4} [DecidableEq α] (f : Perm α) (x y : α) :
swap (f x) (f y) = f * swap x y * f⁻¹
source
@[simp]
theorem Equiv.swap_mul_self_mul {α : Type u_4} [DecidableEq α] (i j : α) (σ : Perm α) :
swap i j * (swap i j * σ) = σ

Left-multiplying a permutation with `swap i j` twice gives the original permutation.

This specialization of `swap_mul_self` is useful when using cosets of permutations.

source
@[simp]
theorem Equiv.mul_swap_mul_self {α : Type u_4} [DecidableEq α] (i j : α) (σ : Perm α) :
σ * swap i j * swap i j = σ

Right-multiplying a permutation with `swap i j` twice gives the original permutation.

This specialization of `swap_mul_self` is useful when using cosets of permutations.

source
@[simp]
theorem Equiv.swap_mul_involutive {α : Type u_4} [DecidableEq α] (i j : α) :
Function.Involutive fun (x : Perm α) => swap i j * x

A stronger version of `mul_right_injective`

source
@[simp]
theorem Equiv.mul_swap_involutive {α : Type u_4} [DecidableEq α] (i j : α) :
Function.Involutive fun (x : Perm α) => x * swap i j

A stronger version of `mul_left_injective`

source
@[simp]
theorem Equiv.swap_eq_one_iff {α : Type u_4} [DecidableEq α] {i j : α} :
swap i j = 1 ↔ i = j
source
theorem Equiv.swap_mul_eq_iff {α : Type u_4} [DecidableEq α] {i j : α} {σ : Perm α} :
swap i j * σ = σ ↔ i = j
source
theorem Equiv.mul_swap_eq_iff {α : Type u_4} [DecidableEq α] {i j : α} {σ : Perm α} :
σ * swap i j = σ ↔ i = j
source
theorem Equiv.swap_mul_swap_mul_swap {α : Type u_4} [DecidableEq α] {x y z : α} (hxy : x ≠ y) (hxz : x ≠ z) :
swap y z * swap x y * swap y z = swap z x
source
@[simp]
theorem Equiv.addLeft_zero {α : Type u_4} [AddGroup α] :
Equiv.addLeft 0 = 1
source
@[simp]
theorem Equiv.addRight_zero {α : Type u_4} [AddGroup α] :
Equiv.addRight 0 = 1
source
@[simp]
theorem Equiv.addLeft_add {α : Type u_4} [AddGroup α] (a b : α) :
Equiv.addLeft (a + b) = Equiv.addLeft a * Equiv.addLeft b
source
@[simp]
theorem Equiv.addRight_add {α : Type u_4} [AddGroup α] (a b : α) :
Equiv.addRight (a + b) = Equiv.addRight b * Equiv.addRight a
source
@[simp]
theorem Equiv.inv_addLeft {α : Type u_4} [AddGroup α] (a : α) :
(Equiv.addLeft a)⁻¹ = Equiv.addLeft (-a)
source
@[simp]
theorem Equiv.inv_addRight {α : Type u_4} [AddGroup α] (a : α) :
(Equiv.addRight a)⁻¹ = Equiv.addRight (-a)
source
@[simp]
theorem Equiv.pow_addLeft {α : Type u_4} [AddGroup α] (a : α) (n : ℕ) :
Equiv.addLeft a ^ n = Equiv.addLeft (n • a)
source
@[simp]
theorem Equiv.pow_addRight {α : Type u_4} [AddGroup α] (a : α) (n : ℕ) :
Equiv.addRight a ^ n = Equiv.addRight (n • a)
source
@[simp]
theorem Equiv.zpow_addLeft {α : Type u_4} [AddGroup α] (a : α) (n : ℤ) :
Equiv.addLeft a ^ n = Equiv.addLeft (n • a)
source
@[simp]
theorem Equiv.zpow_addRight {α : Type u_4} [AddGroup α] (a : α) (n : ℤ) :
Equiv.addRight a ^ n = Equiv.addRight (n • a)
source
@[simp]
theorem Equiv.mulLeft_one {α : Type u_4} [Group α] :
Equiv.mulLeft 1 = 1
source
@[simp]
theorem Equiv.mulRight_one {α : Type u_4} [Group α] :
Equiv.mulRight 1 = 1
source
@[simp]
theorem Equiv.mulLeft_mul {α : Type u_4} [Group α] (a b : α) :
Equiv.mulLeft (a * b) = Equiv.mulLeft a * Equiv.mulLeft b
source
@[simp]
theorem Equiv.mulRight_mul {α : Type u_4} [Group α] (a b : α) :
Equiv.mulRight (a * b) = Equiv.mulRight b * Equiv.mulRight a
source
@[simp]
theorem Equiv.inv_mulLeft {α : Type u_4} [Group α] (a : α) :
(Equiv.mulLeft a)⁻¹ = Equiv.mulLeft a⁻¹
source
@[simp]
theorem Equiv.inv_mulRight {α : Type u_4} [Group α] (a : α) :
(Equiv.mulRight a)⁻¹ = Equiv.mulRight a⁻¹
source
@[simp]
theorem Equiv.pow_mulLeft {α : Type u_4} [Group α] (a : α) (n : ℕ) :
Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)
source
@[simp]
theorem Equiv.pow_mulRight {α : Type u_4} [Group α] (a : α) (n : ℕ) :
Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)
source
@[simp]
theorem Equiv.zpow_mulLeft {α : Type u_4} [Group α] (a : α) (n : ℤ) :
Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)
source
@[simp]
theorem Equiv.zpow_mulRight {α : Type u_4} [Group α] (a : α) (n : ℤ) :
Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)
source
@[reducible]
def MulAut (M : Type u_7) [Mul M] :
Type u_7

The group of multiplicative automorphisms.

Equations

- MulAut M = (M ≃* M)

Instances For

source
@[reducible]
def AddAut (M : Type u_7) [Add M] :
Type u_7

The group of additive automorphisms.

Equations

- AddAut M = (M ≃+ M)

Instances For

source
instance MulAut.instGroup (M : Type u_2) [Mul M] :
Group (MulAut M)

The group operation on multiplicative automorphisms is defined by `g h => MulEquiv.trans h g`. This means that multiplication agrees with composition, `(g*h)(x) = g (h x)`.

Equations

- One or more equations did not get rendered due to their size.

source
instance MulAut.instInhabited (M : Type u_2) [Mul M] :
Inhabited (MulAut M)
Equations

- MulAut.instInhabited M = { default := 1 }

source
@[simp]
theorem MulAut.coe_mul (M : Type u_2) [Mul M] (e₁ e₂ : MulAut M) :
⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂
source
@[simp]
theorem MulAut.coe_one (M : Type u_2) [Mul M] :
⇑1 = id
source
@[simp]
theorem MulAut.coe_inv (M : Type u_2) [Mul M] (e : MulAut M) :
⇑e⁻¹ = ⇑(MulEquiv.symm e)
source
theorem MulAut.mul_def (M : Type u_2) [Mul M] (e₁ e₂ : MulAut M) :
e₁ * e₂ = MulEquiv.trans e₂ e₁
source
theorem MulAut.one_def (M : Type u_2) [Mul M] :
1 = MulEquiv.refl M
source
theorem MulAut.inv_def (M : Type u_2) [Mul M] (e₁ : MulAut M) :
e₁⁻¹ = MulEquiv.symm e₁
source
@[simp]
theorem MulAut.inv_symm (M : Type u_2) [Mul M] (e : MulAut M) :
MulEquiv.symm e⁻¹ = e
source
@[simp]
theorem MulAut.symm_inv (M : Type u_2) [Mul M] (e : MulAut M) :
(MulEquiv.symm e)⁻¹ = e
source
@[simp]
theorem MulAut.inv_apply (M : Type u_2) [Mul M] (e : MulAut M) (m : M) :
e⁻¹ m = (MulEquiv.symm e) m
source
@[simp]
theorem MulAut.mul_apply (M : Type u_2) [Mul M] (e₁ e₂ : MulAut M) (m : M) :
(e₁ * e₂) m = e₁ (e₂ m)
source
@[simp]
theorem MulAut.one_apply (M : Type u_2) [Mul M] (m : M) :
1 m = m
source
theorem MulAut.apply_inv_self (M : Type u_2) [Mul M] (e : MulAut M) (m : M) :
e (e⁻¹ m) = m
source
theorem MulAut.inv_apply_self (M : Type u_2) [Mul M] (e : MulAut M) (m : M) :
e⁻¹ (e m) = m
source
def MulAut.toPerm (M : Type u_2) [Mul M] :
MulAut M →* Equiv.Perm M

Monoid hom from the group of multiplicative automorphisms to the group of permutations.

Equations

- MulAut.toPerm M = { toFun := MulEquiv.toEquiv, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
def MulAut.conj {G : Type u_3} [Group G] :
G →* MulAut G

Group conjugation, `MulAut.conj g h = g * h * g⁻¹`, as a monoid homomorphism mapping multiplication in `G` into multiplication in the automorphism group `MulAut G`. See also the type `ConjAct G` for any group `G`, which has a `MulAction (ConjAct G) G` instance where `conj G` acts on `G` by conjugation.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem MulAut.conj_apply {G : Type u_3} [Group G] (g h : G) :
(conj g) h = g * h * g⁻¹
source
@[simp]
theorem MulAut.conj_symm_apply {G : Type u_3} [Group G] (g h : G) :
(MulEquiv.symm (conj g)) h = g⁻¹ * h * g
source
theorem MulAut.conj_inv_apply {G : Type u_3} [Group G] (g h : G) :
(conj g)⁻¹ h = g⁻¹ * h * g
source
def MulAut.congr {G : Type u_3} [Group G] {H : Type u_7} [Group H] (ϕ : G ≃* H) :
MulAut G ≃* MulAut H

Isomorphic groups have isomorphic automorphism groups.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem MulAut.congr_apply {G : Type u_3} [Group G] {H : Type u_7} [Group H] (ϕ : G ≃* H) (f : MulAut G) :
(congr ϕ) f = ϕ.symm.trans (MulEquiv.trans f ϕ)
source
@[simp]
theorem MulAut.congr_symm_apply {G : Type u_3} [Group G] {H : Type u_7} [Group H] (ϕ : G ≃* H) (f : MulAut H) :
(congr ϕ).symm f = ϕ.trans (MulEquiv.trans f ϕ.symm)
source
instance AddAut.group (A : Type u_1) [Add A] :
Group (AddAut A)

The group operation on additive automorphisms is defined by `g h => AddEquiv.trans h g`. This means that multiplication agrees with composition, `(g*h)(x) = g (h x)`.

Equations

- One or more equations did not get rendered due to their size.

source
instance AddAut.instGroup (M : Type u_2) [Add M] :
AddGroup (AddAut M)
Equations

- One or more equations did not get rendered due to their size.

source
instance AddAut.instInhabited (A : Type u_1) [Add A] :
Inhabited (AddAut A)
Equations

- AddAut.instInhabited A = { default := 1 }

source
@[simp]
theorem AddAut.coe_mul (A : Type u_1) [Add A] (e₁ e₂ : AddAut A) :
⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂
source
@[simp]
theorem AddAut.coe_one (A : Type u_1) [Add A] :
⇑1 = id
source
@[simp]
theorem AddAut.coe_inv (A : Type u_1) [Add A] (e : AddAut A) :
⇑e⁻¹ = ⇑(AddEquiv.symm e)
source
theorem AddAut.mul_def (A : Type u_1) [Add A] (e₁ e₂ : AddAut A) :
e₁ * e₂ = AddEquiv.trans e₂ e₁
source
theorem AddAut.one_def (A : Type u_1) [Add A] :
1 = AddEquiv.refl A
source
theorem AddAut.inv_def (A : Type u_1) [Add A] (e₁ : AddAut A) :
e₁⁻¹ = AddEquiv.symm e₁
source
@[simp]
theorem AddAut.mul_apply (A : Type u_1) [Add A] (e₁ e₂ : AddAut A) (a : A) :
(e₁ * e₂) a = e₁ (e₂ a)
source
@[simp]
theorem AddAut.one_apply (A : Type u_1) [Add A] (a : A) :
1 a = a
source
@[simp]
theorem AddAut.inv_symm (A : Type u_1) [Add A] (e : AddAut A) :
AddEquiv.symm e⁻¹ = e
source
@[simp]
theorem AddAut.symm_inv (A : Type u_1) [Add A] (e : AddAut A) :
(AddEquiv.symm e)⁻¹ = e
source
@[simp]
theorem AddAut.inv_apply (A : Type u_1) [Add A] (e : AddAut A) (a : A) :
e⁻¹ a = (AddEquiv.symm e) a
source
theorem AddAut.apply_inv_self (A : Type u_1) [Add A] (e : AddAut A) (a : A) :
e⁻¹ (e a) = a
source
theorem AddAut.inv_apply_self (A : Type u_1) [Add A] (e : AddAut A) (a : A) :
e (e⁻¹ a) = a
source
def AddAut.toPerm (A : Type u_1) [Add A] :
AddAut A →* Equiv.Perm A

Monoid hom from the group of multiplicative automorphisms to the group of permutations.

Equations

- AddAut.toPerm A = { toFun := AddEquiv.toEquiv, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
def AddAut.conj {G : Type u_3} [AddGroup G] :
G →+ Additive (AddAut G)

Additive group conjugation, `AddAut.conj g h = g + h - g`, as an additive monoid homomorphism mapping addition in `G` into multiplication in the automorphism group `AddAut G` (written additively in order to define the map).

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem AddAut.conj_apply {G : Type u_3} [AddGroup G] (g h : G) :
(Additive.toMul (conj g)) h = g + h + -g
source
@[simp]
theorem AddAut.conj_symm_apply {G : Type u_3} [AddGroup G] (g h : G) :
(AddEquiv.symm (Additive.toMul (conj g))) h = -g + h + g
source
theorem AddAut.conj_inv_apply {G : Type u_3} [AddGroup G] (g h : G) :
(Additive.toMul (conj g))⁻¹ h = -g + h + g
source
theorem AddAut.neg_conj_apply {G : Type u_3} [AddGroup G] (g h : G) :
(Additive.toMul (-conj g)) h = -g + h + g
source
def AddAut.congr {G : Type u_3} [AddGroup G] {H : Type u_7} [AddGroup H] (ϕ : G ≃+ H) :
AddAut G ≃* AddAut H

Isomorphic additive groups have isomorphic automorphism groups.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem AddAut.congr_apply {G : Type u_3} [AddGroup G] {H : Type u_7} [AddGroup H] (ϕ : G ≃+ H) (f : AddAut G) :
(congr ϕ) f = ϕ.symm.trans (AddEquiv.trans f ϕ)
source
@[simp]
theorem AddAut.congr_symm_apply {G : Type u_3} [AddGroup G] {H : Type u_7} [AddGroup H] (ϕ : G ≃+ H) (f : AddAut H) :
(congr ϕ).symm f = ϕ.trans (AddEquiv.trans f ϕ.symm)
source
def MulAutMultiplicative (G : Type u_3) [AddGroup G] :
MulAut (Multiplicative G) ≃* AddAut G

`Multiplicative G` and `G` have isomorphic automorphism groups.

Equations

- MulAutMultiplicative G = { toEquiv := AddEquiv.toMultiplicative.symm, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem MulAutMultiplicative_apply_symm_apply (G : Type u_3) [AddGroup G] (a✝ : Multiplicative G ≃* Multiplicative G) (a : G) :
(AddEquiv.symm ((MulAutMultiplicative G) a✝)) a = Multiplicative.toAdd (a✝.symm (Multiplicative.ofAdd a))
source
@[simp]
theorem MulAutMultiplicative_symm_apply_apply (G : Type u_3) [AddGroup G] (a✝ : G ≃+ G) (a : Multiplicative G) :
((MulAutMultiplicative G).symm a✝) a = Multiplicative.ofAdd (a✝ (Multiplicative.toAdd a))
source
@[simp]
theorem MulAutMultiplicative_symm_apply_symm_apply (G : Type u_3) [AddGroup G] (a✝ : G ≃+ G) (a : Multiplicative G) :
(MulEquiv.symm ((MulAutMultiplicative G).symm a✝)) a = Multiplicative.ofAdd (a✝.symm (Multiplicative.toAdd a))
source
@[simp]
theorem MulAutMultiplicative_apply_apply (G : Type u_3) [AddGroup G] (a✝ : Multiplicative G ≃* Multiplicative G) (a : G) :
((MulAutMultiplicative G) a✝) a = Multiplicative.toAdd (a✝ (Multiplicative.ofAdd a))
source
def AddAutAdditive (G : Type u_3) [Group G] :
AddAut (Additive G) ≃* MulAut G

`Additive G` and `G` have isomorphic automorphism groups.

Equations

- AddAutAdditive G = { toEquiv := MulEquiv.toAdditive.symm, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem AddAutAdditive_symm_apply_symm_apply (G : Type u_3) [Group G] (a✝ : G ≃* G) (a : Additive G) :
(AddEquiv.symm ((AddAutAdditive G).symm a✝)) a = Additive.ofMul (a✝.symm (Additive.toMul a))
source
@[simp]
theorem AddAutAdditive_apply_apply (G : Type u_3) [Group G] (a✝ : Additive G ≃+ Additive G) (a : G) :
((AddAutAdditive G) a✝) a = Additive.toMul (a✝ (Additive.ofMul a))
source
@[simp]
theorem AddAutAdditive_symm_apply_apply (G : Type u_3) [Group G] (a✝ : G ≃* G) (a : Additive G) :
((AddAutAdditive G).symm a✝) a = Additive.ofMul (a✝ (Additive.toMul a))
source
@[simp]
theorem AddAutAdditive_apply_symm_apply (G : Type u_3) [Group G] (a✝ : Additive G ≃+ Additive G) (a : G) :
(MulEquiv.symm ((AddAutAdditive G) a✝)) a = Additive.toMul (a✝.symm (Additive.ofMul a))