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

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 α = (α → α)

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• instInhabitedEnd = { default := 1 }

Monoid endomorphisms

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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 := ⋯ } }

@[implicit_reducible]

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

Equations

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

@[simp]

theorem Equiv.Perm.default_eq {α : Type u_4} : default = 1

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.

@[simp]

theorem Equiv.Perm.equivUnitsEnd_symm_apply_apply {α : Type u_4} (u : (Function.End α)ˣ) : ⇑(equivUnitsEnd.symm u) = ↑u

@[simp]

theorem Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply {α : Type u_4} (u : (Function.End α)ˣ) : ⇑(Equiv.symm (equivUnitsEnd.symm u)) = ↑u⁻¹

@[simp]

theorem Equiv.Perm.val_equivUnitsEnd_apply {α : Type u_4} (e : Perm α) (a : α) : ↑(equivUnitsEnd e) a = e a

@[simp]

theorem Equiv.Perm.val_inv_equivUnitsEnd_apply {α : Type u_4} (e : Perm α) (a : α) : ↑(equivUnitsEnd e)⁻¹ a = (Equiv.symm e) a

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

@[simp]

theorem MonoidHom.toHomPerm_apply_symm_apply {α : Type u_4} {G : Type u_7} [Group G] (f : G →* Function.End α) (x : G) : ⇑(Equiv.symm (f.toHomPerm x)) = ↑(f.toHomUnits x)⁻¹

@[simp]

theorem MonoidHom.toHomPerm_apply_apply {α : Type u_4} {G : Type u_7} [Group G] (f : G →* Function.End α) (x : G) : ⇑(f.toHomPerm x) = f x

theorem Equiv.Perm.mul_apply {α : Type u_4} (f g : Perm α) (x : α) : (f * g) x = f (g x)

theorem Equiv.Perm.one_apply {α : Type u_4} (x : α) : 1 x = x

theorem Equiv.Perm.one_def {α : Type u_4} : 1 = Equiv.refl α

theorem Equiv.Perm.mul_def {α : Type u_4} (f g : Perm α) : f * g = Equiv.trans g f

theorem Equiv.Perm.inv_def {α : Type u_4} (f : Perm α) : f⁻¹ = Equiv.symm f

@[simp]

theorem Equiv.Perm.coe_inv {α : Type u_4} (f : Perm α) : ⇑f⁻¹ = ⇑(Equiv.symm f)

@[simp]

theorem Equiv.Perm.coe_one {α : Type u_4} : ⇑1 = id

@[simp]

theorem Equiv.Perm.coe_mul {α : Type u_4} (f g : Perm α) : ⇑(f * g) = ⇑f ∘ ⇑g

theorem Equiv.Perm.coe_pow {α : Type u_4} (f : Perm α) (n : ℕ) : ⇑(f ^ n) = (⇑f)^[n]

theorem Equiv.Perm.iterate_eq_pow {α : Type u_4} (f : Perm α) (n : ℕ) : (⇑f)^[n] = ⇑(f ^ n)

theorem Equiv.Perm.eq_inv_iff_eq {α : Type u_4} {f : Perm α} {x y : α} : x = f⁻¹ y ↔ f x = y

theorem Equiv.Perm.inv_eq_iff_eq {α : Type u_4} {f : Perm α} {x y : α} : f⁻¹ x = y ↔ x = f y

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.

@[deprecated "use `pull_end` simpset instead" (since := "2026-05-13")]

theorem Equiv.Perm.trans_one {α : Sort u_7} {β : Type u_8} (e : α ≃ β) : e.trans 1 = e

@[deprecated "use `pull_end` simpset instead" (since := "2026-05-13")]

theorem Equiv.Perm.mul_refl {α : Type u_4} (e : Perm α) : e * Equiv.refl α = e

@[deprecated "use `pull_end` simpset instead" (since := "2026-05-13")]

theorem Equiv.Perm.one_symm {α : Type u_4} : Equiv.symm 1 = 1

@[deprecated "use `pull_end` simpset instead" (since := "2026-05-13")]

theorem Equiv.Perm.refl_inv {α : Type u_4} : (Equiv.refl α)⁻¹ = 1

@[deprecated "use `pull_end` simpset instead" (since := "2026-05-13")]

theorem Equiv.Perm.one_trans {α : Type u_7} {β : Sort u_8} (e : α ≃ β) : Equiv.trans 1 e = e

@[deprecated "use `pull_end` simpset instead" (since := "2026-05-13")]

theorem Equiv.Perm.refl_mul {α : Type u_4} (e : Perm α) : Equiv.refl α * e = e

@[deprecated "use `pull_end` simpset instead" (since := "2026-05-13")]

theorem Equiv.Perm.inv_trans_self {α : Type u_4} (e : Perm α) : Equiv.trans e⁻¹ e = 1

@[deprecated "use `pull_end` simpset instead" (since := "2026-05-13")]

theorem Equiv.Perm.mul_symm {α : Type u_4} (e : Perm α) : e * Equiv.symm e = 1

@[deprecated "use `pull_end` simpset instead" (since := "2026-05-13")]

theorem Equiv.Perm.self_trans_inv {α : Type u_4} (e : Perm α) : Equiv.trans e e⁻¹ = 1

@[deprecated "use `pull_end` simpset instead" (since := "2026-05-13")]

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.

@[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)

@[simp]

theorem Equiv.Perm.sumCongr_inv {α : Type u_7} {β : Type u_8} (e : Perm α) (f : Perm β) : (e.sumCongr f)⁻¹ = e⁻¹.sumCongr f⁻¹

@[simp]

theorem Equiv.Perm.sumCongr_one {α : Type u_7} {β : Type u_8} : sumCongr 1 1 = 1

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' := ⋯ }

@[simp]

theorem Equiv.Perm.sumCongrHom_apply (α : Type u_7) (β : Type u_8) (a : Perm α × Perm β) : (sumCongrHom α β) a = a.1.sumCongr a.2

theorem Equiv.Perm.sumCongrHom_injective {α : Type u_7} {β : Type u_8} : Function.Injective ⇑(sumCongrHom α β)

@[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)

@[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.

@[simp]

theorem Equiv.Perm.sigmaCongrRight_mul {α : Type u_7} {β : α → Type u_8} (F G : (a : α) → Perm (β a)) : sigmaCongrRight F * sigmaCongrRight G = sigmaCongrRight (F * G)

@[simp]

theorem Equiv.Perm.sigmaCongrRight_inv {α : Type u_7} {β : α → Type u_8} (F : (a : α) → Perm (β a)) : (sigmaCongrRight F)⁻¹ = sigmaCongrRight fun (a : α) => (F a)⁻¹

@[simp]

theorem Equiv.Perm.sigmaCongrRight_one {α : Type u_7} {β : α → Type u_8} : sigmaCongrRight 1 = 1

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' := ⋯ }

@[simp]

theorem Equiv.Perm.sigmaCongrRightHom_apply {α : Type u_7} (β : α → Type u_8) (F : (a : α) → Perm (β a)) : (sigmaCongrRightHom β) F = sigmaCongrRight F

theorem Equiv.Perm.sigmaCongrRightHom_injective {α : Type u_7} {β : α → Type u_8} : Function.Injective ⇑(sigmaCongrRightHom β)

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' := ⋯ }

@[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

theorem Equiv.Perm.subtypeCongrHom_injective {α : Type u_4} (p : α → Prop) [DecidablePred p] : Function.Injective ⇑(subtypeCongrHom p)

@[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.

@[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

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' := ⋯ }

@[simp]

theorem Equiv.permCongrHom_symm {α : Type u_4} {β : Type u_5} (e : α ≃ β) : e.permCongrHom.symm = e.symm.permCongrHom

@[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

@[simp]

theorem Equiv.permCongrHom_coe_equiv {α : Type u_4} {β : Type u_5} (e : α ≃ β) : ↑e.permCongrHom = e.permCongr

@[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.

@[simp]

theorem Equiv.Perm.extendDomain_one {α : Type u_4} {β : Type u_5} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) : extendDomain 1 f = 1

@[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

@[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

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' := ⋯ }

@[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

theorem Equiv.Perm.extendDomainHom_injective {α : Type u_4} {β : Type u_5} {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) : Function.Injective ⇑(extendDomainHom f)

@[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

@[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

@[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

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 := ⋯ }

@[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, ⋯⟩

@[simp]

theorem Equiv.Perm.subtypePerm_one {α : Type u_4} (p : α → Prop) (h : ∀ (x : α), p (1 x) ↔ p (1 x) := ⋯) : subtypePerm 1 h = 1

@[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 ⋯

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.

@[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.

@[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 ⋯

@[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 ⋯

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' := ⋯ }

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

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⟩)

@[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)

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

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

theorem Equiv.Perm.ofSubtype_injective {α : Type u_4} {p : α → Prop} [DecidablePred p] : Function.Injective ⇑ofSubtype

@[simp]

theorem Equiv.Perm.subtypePerm_ofSubtype {α : Type u_4} {p : α → Prop} [DecidablePred p] (f : Perm (Subtype p)) : (ofSubtype f).subtypePerm ⋯ = f

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

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

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.

@[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 ⋯

@[simp]

theorem Equiv.Perm.subtypeEquivSubtypePerm_apply_coe {α : Type u_4} (p : α → Prop) [DecidablePred p] (f : Perm (Subtype p)) : ↑((Perm.subtypeEquivSubtypePerm p) f) = ofSubtype f

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⟩)

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

@[simp]

theorem Equiv.swap_inv {α : Type u_4} [DecidableEq α] (x y : α) : (swap x y)⁻¹ = swap x y

@[simp]

theorem Equiv.swap_mul_self {α : Type u_4} [DecidableEq α] (i j : α) : swap i j * swap i j = 1

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)

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

theorem Equiv.swap_apply_apply {α : Type u_4} [DecidableEq α] (f : Perm α) (x y : α) : swap (f x) (f y) = f * swap x y * f⁻¹

@[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.

@[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.

@[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

@[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

@[simp]

theorem Equiv.swap_eq_one_iff {α : Type u_4} [DecidableEq α] {i j : α} : swap i j = 1 ↔ i = j

theorem Equiv.swap_mul_eq_iff {α : Type u_4} [DecidableEq α] {i j : α} {σ : Perm α} : swap i j * σ = σ ↔ i = j

theorem Equiv.mul_swap_eq_iff {α : Type u_4} [DecidableEq α] {i j : α} {σ : Perm α} : σ * swap i j = σ ↔ i = j

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

@[simp]

theorem Equiv.mulLeft_one {α : Type u_4} [Group α] : Equiv.mulLeft 1 = 1

@[simp]

theorem Equiv.addLeft_zero {α : Type u_4} [AddGroup α] : Equiv.addLeft 0 = 1

@[simp]

theorem Equiv.mulRight_one {α : Type u_4} [Group α] : Equiv.mulRight 1 = 1

@[simp]

theorem Equiv.addRight_zero {α : Type u_4} [AddGroup α] : Equiv.addRight 0 = 1

@[simp]

theorem Equiv.mulLeft_mul {α : Type u_4} [Group α] (a b : α) : Equiv.mulLeft (a * b) = Equiv.mulLeft a * Equiv.mulLeft b

@[simp]

theorem Equiv.addLeft_add {α : Type u_4} [AddGroup α] (a b : α) : Equiv.addLeft (a + b) = Equiv.addLeft a * Equiv.addLeft b

@[simp]

theorem Equiv.mulRight_mul {α : Type u_4} [Group α] (a b : α) : Equiv.mulRight (a * b) = Equiv.mulRight b * Equiv.mulRight a

@[simp]

theorem Equiv.addRight_add {α : Type u_4} [AddGroup α] (a b : α) : Equiv.addRight (a + b) = Equiv.addRight b * Equiv.addRight a

@[simp]

theorem Equiv.inv_mulLeft {α : Type u_4} [Group α] (a : α) : (Equiv.mulLeft a)⁻¹ = Equiv.mulLeft a⁻¹

@[simp]

theorem Equiv.neg_addLeft {α : Type u_4} [AddGroup α] (a : α) : (Equiv.addLeft a)⁻¹ = Equiv.addLeft (-a)

@[simp]

theorem Equiv.inv_mulRight {α : Type u_4} [Group α] (a : α) : (Equiv.mulRight a)⁻¹ = Equiv.mulRight a⁻¹

@[simp]

theorem Equiv.neg_addRight {α : Type u_4} [AddGroup α] (a : α) : (Equiv.addRight a)⁻¹ = Equiv.addRight (-a)

@[simp]

theorem Equiv.pow_mulLeft {α : Type u_4} [Group α] (a : α) (n : ℕ) : Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)

@[simp]

theorem Equiv.nsmul_addLeft {α : Type u_4} [AddGroup α] (a : α) (n : ℕ) : Equiv.addLeft a ^ n = Equiv.addLeft (n • a)

@[simp]

theorem Equiv.pow_mulRight {α : Type u_4} [Group α] (a : α) (n : ℕ) : Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)

@[simp]

theorem Equiv.nsmul_addRight {α : Type u_4} [AddGroup α] (a : α) (n : ℕ) : Equiv.addRight a ^ n = Equiv.addRight (n • a)

@[simp]

theorem Equiv.zpow_mulLeft {α : Type u_4} [Group α] (a : α) (n : ℤ) : Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)

@[simp]

theorem Equiv.zsmul_addLeft {α : Type u_4} [AddGroup α] (a : α) (n : ℤ) : Equiv.addLeft a ^ n = Equiv.addLeft (n • a)

@[simp]

theorem Equiv.zpow_mulRight {α : Type u_4} [Group α] (a : α) (n : ℤ) : Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)

@[simp]

theorem Equiv.zsmul_addRight {α : Type u_4} [AddGroup α] (a : α) (n : ℤ) : Equiv.addRight a ^ n = Equiv.addRight (n • a)

@[reducible, inline]

abbrev MulAut (M : Type u_7) [Mul M] : Type u_7

The group of multiplicative automorphisms.

Equations

• MulAut M = (M ≃* M)

@[reducible, inline]

abbrev AddAut (M : Type u_7) [Add M] : Type u_7

The group of additive automorphisms.

Equations

• AddAut M = (M ≃+ M)

@[implicit_reducible]

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

If M is a type with multiplicative, then multiplicative automorphisms of M have the structure of a group.

Equations

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

@[implicit_reducible]

instance AddAut.instAddGroup (M : Type u_2) [Add M] : AddGroup (AddAut M)

If M is a type with addition, then additive automorphisms of M have the structure of a group.

We give AddAut M the structure of an additive group rather than a multiplicative group to help with to_additive translation. Without this, any proof in group theory making use of the conjugation action G →* MulAut G would be impossible to to_additive-ize because a correct additivization would require inserting Additive around AddAut G and dealing with these extra Additives in the proof, but to_additive is unable to do this automatically.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance AddAut.instInhabited (M : Type u_2) [Add M] : Inhabited (AddAut M)

Equations

• AddAut.instInhabited M = { default := 0 }

@[simp]

theorem MulAut.coe_mul (M : Type u_2) [Mul M] (e₁ e₂ : MulAut M) : ⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂

@[simp]

theorem AddAut.coe_add (M : Type u_2) [Add M] (e₁ e₂ : AddAut M) : ⇑(e₁ + e₂) = ⇑e₁ ∘ ⇑e₂

@[simp]

theorem MulAut.coe_one (M : Type u_2) [Mul M] : ⇑1 = id

@[simp]

theorem AddAut.coe_zero (M : Type u_2) [Add M] : ⇑0 = id

@[simp]

theorem MulAut.coe_inv (M : Type u_2) [Mul M] (e : MulAut M) : ⇑e⁻¹ = ⇑(MulEquiv.symm e)

@[simp]

theorem AddAut.coe_neg (M : Type u_2) [Add M] (e : AddAut M) : ⇑(-e) = ⇑(AddEquiv.symm e)

theorem MulAut.mul_def (M : Type u_2) [Mul M] (e₁ e₂ : MulAut M) : e₁ * e₂ = MulEquiv.trans e₂ e₁

theorem AddAut.add_def (M : Type u_2) [Add M] (e₁ e₂ : AddAut M) : e₁ + e₂ = AddEquiv.trans e₂ e₁

theorem MulAut.one_def (M : Type u_2) [Mul M] : 1 = MulEquiv.refl M

theorem AddAut.zero_def (M : Type u_2) [Add M] : 0 = AddEquiv.refl M

theorem MulAut.inv_def (M : Type u_2) [Mul M] (e₁ : MulAut M) : e₁⁻¹ = MulEquiv.symm e₁

theorem AddAut.neg_def (M : Type u_2) [Add M] (e₁ : AddAut M) : -e₁ = AddEquiv.symm e₁

@[simp]

theorem MulAut.inv_symm (M : Type u_2) [Mul M] (e : MulAut M) : MulEquiv.symm e⁻¹ = e

@[simp]

theorem AddAut.neg_symm (M : Type u_2) [Add M] (e : AddAut M) : AddEquiv.symm (-e) = e

@[simp]

theorem MulAut.symm_inv (M : Type u_2) [Mul M] (e : MulAut M) : (MulEquiv.symm e)⁻¹ = e

@[simp]

theorem AddAut.symm_neg (M : Type u_2) [Add M] (e : AddAut M) : -AddEquiv.symm e = e

@[simp]

theorem MulAut.inv_apply (M : Type u_2) [Mul M] (e : MulAut M) (m : M) : e⁻¹ m = (MulEquiv.symm e) m

@[simp]

theorem AddAut.neg_apply (M : Type u_2) [Add M] (e : AddAut M) (m : M) : (-e) m = (AddEquiv.symm e) m

@[simp]

theorem MulAut.mul_apply (M : Type u_2) [Mul M] (e₁ e₂ : MulAut M) (m : M) : (e₁ * e₂) m = e₁ (e₂ m)

@[simp]

theorem AddAut.add_apply (M : Type u_2) [Add M] (e₁ e₂ : AddAut M) (m : M) : (e₁ + e₂) m = e₁ (e₂ m)

@[simp]

theorem MulAut.one_apply (M : Type u_2) [Mul M] (m : M) : 1 m = m

@[simp]

theorem AddAut.zero_apply (M : Type u_2) [Add M] (m : M) : 0 m = m

theorem MulAut.apply_inv_self (M : Type u_2) [Mul M] (e : MulAut M) (m : M) : e (e⁻¹ m) = m

theorem AddAut.apply_neg_self (M : Type u_2) [Add M] (e : AddAut M) (m : M) : e ((-e) m) = m

theorem MulAut.inv_apply_self (M : Type u_2) [Mul M] (e : MulAut M) (m : M) : e⁻¹ (e m) = m

theorem AddAut.neg_apply_self (M : Type u_2) [Add M] (e : AddAut M) (m : M) : (-e) (e m) = m

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' := ⋯ }

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.

def AddAut.addConj {G : Type u_3} [AddGroup G] : G →+ AddAut G

Group conjugation, AddAut.addConj g h = g + h + -g, as an additive homomorphism mapping addition in G into addition in the additive automorphism group AddAut G.

Equations

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

@[simp]

theorem MulAut.conj_apply {G : Type u_3} [Group G] (g h : G) : (conj g) h = g * h * g⁻¹

@[simp]

theorem AddAut.addConj_apply {G : Type u_3} [AddGroup G] (g h : G) : (addConj g) h = g + h + -g

@[simp]

theorem MulAut.conj_symm_apply {G : Type u_3} [Group G] (g h : G) : (MulEquiv.symm (conj g)) h = g⁻¹ * h * g

@[simp]

theorem AddAut.addConj_symm_apply {G : Type u_3} [AddGroup G] (g h : G) : (AddEquiv.symm (addConj g)) h = -g + h + g

theorem MulAut.conj_inv_apply {G : Type u_3} [Group G] (g h : G) : (conj g)⁻¹ h = g⁻¹ * h * g

theorem AddAut.addConj_neg_apply {G : Type u_3} [AddGroup G] (g h : G) : (-addConj g) h = -g + h + g

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.

def AddAut.congr {G : Type u_3} [AddGroup G] {H : Type u_7} [AddGroup H] (ϕ : G ≃+ H) : AddAut G ≃+ AddAut H

Isomorphic groups have isomorphic automorphism groups.

Equations

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

@[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 ϕ)

@[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)

@[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 ϕ)

@[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)

@[deprecated AddAut.coe_add (since := "2026-05-26")]

theorem AddAut.coe_mul (M : Type u_2) [Add M] (e₁ e₂ : AddAut M) : ⇑(e₁ + e₂) = ⇑e₁ ∘ ⇑e₂

Alias of AddAut.coe_add.

@[deprecated AddAut.coe_zero (since := "2026-05-26")]

theorem AddAut.coe_one (M : Type u_2) [Add M] : ⇑0 = id

Alias of AddAut.coe_zero.

@[deprecated AddAut.coe_neg (since := "2026-05-26")]

theorem AddAut.coe_inv (M : Type u_2) [Add M] (e : AddAut M) : ⇑(-e) = ⇑(AddEquiv.symm e)

Alias of AddAut.coe_neg.

@[deprecated AddAut.add_def (since := "2026-05-26")]

theorem AddAut.mul_def (M : Type u_2) [Add M] (e₁ e₂ : AddAut M) : e₁ + e₂ = AddEquiv.trans e₂ e₁

Alias of AddAut.add_def.

@[deprecated AddAut.zero_def (since := "2026-05-26")]

theorem AddAut.one_def (M : Type u_2) [Add M] : 0 = AddEquiv.refl M

Alias of AddAut.zero_def.

@[deprecated AddAut.neg_def (since := "2026-05-26")]

theorem AddAut.inv_def (M : Type u_2) [Add M] (e₁ : AddAut M) : -e₁ = AddEquiv.symm e₁

Alias of AddAut.neg_def.

@[deprecated AddAut.add_apply (since := "2026-05-26")]

theorem AddAut.mul_apply (M : Type u_2) [Add M] (e₁ e₂ : AddAut M) (m : M) : (e₁ + e₂) m = e₁ (e₂ m)

Alias of AddAut.add_apply.

@[deprecated AddAut.zero_apply (since := "2026-05-26")]

theorem AddAut.one_apply (M : Type u_2) [Add M] (m : M) : 0 m = m

Alias of AddAut.zero_apply.

@[deprecated AddAut.neg_symm (since := "2026-05-26")]

theorem AddAut.inv_symm (M : Type u_2) [Add M] (e : AddAut M) : AddEquiv.symm (-e) = e

Alias of AddAut.neg_symm.

@[deprecated AddAut.symm_neg (since := "2026-05-26")]

theorem AddAut.symm_inv (M : Type u_2) [Add M] (e : AddAut M) : -AddEquiv.symm e = e

Alias of AddAut.symm_neg.

@[deprecated AddAut.neg_apply (since := "2026-05-26")]

theorem AddAut.inv_apply (M : Type u_2) [Add M] (e : AddAut M) (m : M) : (-e) m = (AddEquiv.symm e) m

Alias of AddAut.neg_apply.

@[deprecated AddAut.neg_apply_self (since := "2026-05-26")]

theorem AddAut.inv_apply_self (M : Type u_2) [Add M] (e : AddAut M) (m : M) : (-e) (e m) = m

Alias of AddAut.neg_apply_self.

@[deprecated AddAut.apply_neg_self (since := "2026-05-26")]

theorem AddAut.apply_inv_self (M : Type u_2) [Add M] (e : AddAut M) (m : M) : e ((-e) m) = m

Alias of AddAut.apply_neg_self.

def AddAut.toPerm (A : Type u_1) [Add A] : AddAut A →+ Additive (Equiv.Perm A)

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

Equations

• AddAut.toPerm A = { toFun := AddEquiv.toEquiv, map_zero' := ⋯, map_add' := ⋯ }

@[deprecated AddAut.addConj (since := "2026-05-26")]

def AddAut.conj {G : Type u_3} [AddGroup G] : G →+ AddAut G

Alias of AddAut.addConj.

---

Group conjugation, AddAut.addConj g h = g + h + -g, as an additive homomorphism mapping addition in G into addition in the additive automorphism group AddAut G.

Equations

• @AddAut.conj = @AddAut.addConj

@[deprecated AddAut.addConj_apply (since := "2026-05-26")]

theorem AddAut.conj_apply {G : Type u_3} [AddGroup G] (g h : G) : (addConj g) h = g + h + -g

Alias of AddAut.addConj_apply.

@[deprecated AddAut.addConj_symm_apply (since := "2026-05-26")]

theorem AddAut.conj_symm_apply {G : Type u_3} [AddGroup G] (g h : G) : (AddEquiv.symm (addConj g)) h = -g + h + g

Alias of AddAut.addConj_symm_apply.

@[deprecated AddAut.addConj_neg_apply (since := "2026-05-26")]

theorem AddAut.conj_inv_apply {G : Type u_3} [AddGroup G] (g h : G) : (-addConj g) h = -g + h + g

Alias of AddAut.addConj_neg_apply.

@[deprecated "use `addConj_neg_apply` instead" (since := "2026-05-26")]

theorem AddAut.neg_conj_apply {G : Type u_3} [AddGroup G] (g h : G) : (-addConj g) h = -g + h + g

def MulAutMultiplicative (G : Type u_3) [AddGroup G] : MulAut (Multiplicative G) ≃* Multiplicative (AddAut G)

Multiplicative G and G have isomorphic automorphism groups.

Equations

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

@[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))

@[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))

@[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))

@[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))

def AddAutAdditive (G : Type u_3) [Group G] : AddAut (Additive G) ≃+ Additive (MulAut G)

Additive G and G have isomorphic automorphism groups.

Equations

• AddAutAdditive G = { toEquiv := MulEquiv.toAdditive.symm, map_add' := ⋯ }

@[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))

@[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))

@[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))

@[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))