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

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

Equations

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

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

Equations

• instInhabitedEnd = { default := 1 }

Monoid endomorphisms

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

Equations

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

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

Equations

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

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

Equations

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

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

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.val_equivUnitsEnd_apply {α : Type u_4} (e : Perm α) (a : α) : ↑(equivUnitsEnd e) a = e a

@[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_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_6} [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_apply {α : Type u_4} {G : Type u_6} [Group G] (f : G →* Function.End α) (a✝ : G) : ⇑(f.toHomPerm a✝) = f a✝

@[simp]

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

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

@[simp]

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

@[simp]

theorem Equiv.Perm.apply_inv_self {α : Type u_4} (f : Perm α) (x : α) : f (f⁻¹ 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_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]

@[simp]

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_6} (σ : 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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def Equiv.Perm.permCongrHom {α : Type u_4} {β : Type u_5} (e : α ≃ β) : Perm α ≃* Perm β

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

Equations

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

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

@[simp]

theorem Equiv.Perm.sumCongr_mul {α : Type u_6} {β : Type u_7} (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_6} {β : Type u_7} (e : Perm α) (f : Perm β) : (e.sumCongr f)⁻¹ = e⁻¹.sumCongr f⁻¹

@[simp]

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

def Equiv.Perm.sumCongrHom (α : Type u_6) (β : Type u_7) : 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_6) (β : Type u_7) (a : Perm α × Perm β) : (sumCongrHom α β) a = a.1.sumCongr a.2

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

@[simp]

theorem Equiv.Perm.sumCongr_swap_one {α : Type u_6} {β : Type u_7} [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_6} {β : Type u_7} [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_6} {β : α → Type u_7} (F G : (a : α) → Perm (β a)) : sigmaCongrRight F * sigmaCongrRight G = sigmaCongrRight (F * G)

@[simp]

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

@[simp]

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

def Equiv.Perm.sigmaCongrRightHom {α : Type u_6} (β : α → Type u_7) : ((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_6} (β : α → Type u_7) (F : (a : α) → Perm (β a)) : (sigmaCongrRightHom β) F = sigmaCongrRight F

theorem Equiv.Perm.sigmaCongrRightHom_injective {α : Type u_6} {β : α → Type u_7} : 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.Perm.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.

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_apply_coe {α : Type u_4} (p : α → Prop) [DecidablePred p] (f : Perm (Subtype p)) : ↑((Perm.subtypeEquivSubtypePerm p) f) = ofSubtype f

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

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.addLeft_zero {α : Type u_4} [AddGroup α] : Equiv.addLeft 0 = 1

@[simp]

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

@[simp]

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

@[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_addLeft {α : Type u_4} [AddGroup α] (a : α) : (Equiv.addLeft a)⁻¹ = Equiv.addLeft (-a)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Equiv.mulRight_one {α : Type u_4} [Group α] : Equiv.mulRight 1 = 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.mulRight_mul {α : Type u_4} [Group α] (a b : α) : Equiv.mulRight (a * b) = Equiv.mulRight b * Equiv.mulRight a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible]

def MulAut (M : Type u_6) [Mul M] : Type u_6

The group of multiplicative automorphisms.

Equations

• MulAut M = (M ≃* M)

@[reducible]

def AddAut (M : Type u_6) [Add M] : Type u_6

The group of additive automorphisms.

Equations

• AddAut M = (M ≃+ M)

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.

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

theorem MulAut.symm_inv (M : Type u_2) [Mul M] (e : MulAut M) : (MulEquiv.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 MulAut.mul_apply (M : Type u_2) [Mul M] (e₁ e₂ : MulAut 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

theorem MulAut.apply_inv_self (M : Type u_2) [Mul M] (e : MulAut 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

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.

@[simp]

theorem MulAut.conj_apply {G : Type u_3} [Group G] (g h : G) : (conj 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

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

def MulAut.congr {G : Type u_3} [Group G] {H : Type u_6} [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.

@[simp]

theorem MulAut.congr_symm_apply {G : Type u_3} [Group G] {H : Type u_6} [Group H] (ϕ : G ≃* H) (f : MulAut H) : (congr ϕ).symm f = ϕ.trans (MulEquiv.trans f ϕ.symm)

@[simp]

theorem MulAut.congr_apply {G : Type u_3} [Group G] {H : Type u_6} [Group H] (ϕ : G ≃* H) (f : MulAut G) : (congr ϕ) f = ϕ.symm.trans (MulEquiv.trans f ϕ)

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.

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.

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

Equations

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

@[simp]

theorem AddAut.coe_mul (A : Type u_1) [Add A] (e₁ e₂ : AddAut A) : ⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂

@[simp]

theorem AddAut.coe_one (A : Type u_1) [Add A] : ⇑1 = id

@[simp]

theorem AddAut.coe_inv (A : Type u_1) [Add A] (e : AddAut A) : ⇑e⁻¹ = ⇑(AddEquiv.symm e)

theorem AddAut.mul_def (A : Type u_1) [Add A] (e₁ e₂ : AddAut A) : e₁ * e₂ = AddEquiv.trans e₂ e₁

theorem AddAut.one_def (A : Type u_1) [Add A] : 1 = AddEquiv.refl A

theorem AddAut.inv_def (A : Type u_1) [Add A] (e₁ : AddAut A) : e₁⁻¹ = AddEquiv.symm e₁

@[simp]

theorem AddAut.mul_apply (A : Type u_1) [Add A] (e₁ e₂ : AddAut A) (a : A) : (e₁ * e₂) a = e₁ (e₂ a)

@[simp]

theorem AddAut.one_apply (A : Type u_1) [Add A] (a : A) : 1 a = a

@[simp]

theorem AddAut.inv_symm (A : Type u_1) [Add A] (e : AddAut A) : AddEquiv.symm e⁻¹ = e

@[simp]

theorem AddAut.symm_inv (A : Type u_1) [Add A] (e : AddAut A) : (AddEquiv.symm e)⁻¹ = e

@[simp]

theorem AddAut.inv_apply (A : Type u_1) [Add A] (e : AddAut A) (a : A) : e⁻¹ a = (AddEquiv.symm e) a

theorem AddAut.apply_inv_self (A : Type u_1) [Add A] (e : AddAut A) (a : A) : e⁻¹ (e a) = a

theorem AddAut.inv_apply_self (A : Type u_1) [Add A] (e : AddAut A) (a : A) : e (e⁻¹ a) = a

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

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.

@[simp]

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

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

theorem AddAut.conj_inv_apply {G : Type u_3} [AddGroup G] (g h : G) : (Additive.toMul (conj g))⁻¹ h = -g + h + g

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

def AddAut.congr {G : Type u_3} [AddGroup G] {H : Type u_6} [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.

@[simp]

theorem AddAut.congr_apply {G : Type u_3} [AddGroup G] {H : Type u_6} [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_6} [AddGroup H] (ϕ : G ≃+ H) (f : AddAut H) : (congr ϕ).symm f = ϕ.trans (AddEquiv.trans f ϕ.symm)

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

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

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

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

@[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_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_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_apply (G : Type u_3) [Group G] (a✝ : G ≃* G) (a : Additive G) : ((AddAutAdditive G).symm a✝) a = Additive.ofMul (a✝ (Additive.toMul a))