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

Instances For

source

instance instMonoidEnd {α : Type u_4} :

Monoid (Function.End α)

Equations

source

instance instInhabitedEnd {α : Type u_4} :

Inhabited (Function.End α)

Equations

Monoid endomorphisms #

source

instance Equiv.Perm.instOne {α : Type u_4} :

One (Perm α)

Equations

source

instance Equiv.Perm.instMul {α : Type u_4} :

Mul (Perm α)

Equations

source

instance Equiv.Perm.instInv {α : Type u_4} :

Inv (Perm α)

Equations

source

instance Equiv.Perm.instPowNat {α : Type u_4} :

Pow (Perm α) ℕ

Equations

source

instance Equiv.Perm.permGroup {α : Type u_4} :

Group (Perm α)

Equations

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

Instances For

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_apply {α : Type u_4} (u : (Function.End α)ˣ) :

⇑(equivUnitsEnd.symm u) = ↑u

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_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

Instances For

source

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

source

@[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✝)⁻¹

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_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.

source

@[simp]

theorem Equiv.Perm.trans_one {α : Sort u_6} {β : Type u_7} (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_6} {β : Sort u_7} (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

source

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

Perm α ≃* Perm β

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

Equations

Instances For

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

source

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

source

@[simp]

theorem Equiv.Perm.sumCongr_inv {α : Type u_6} {β : Type u_7} (e : Perm α) (f : Perm β) :

(e.sumCongr f)⁻¹ = e⁻¹.sumCongr f⁻¹

source

@[simp]

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

sumCongr 1 1 = 1

source

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

Instances For

source

@[simp]

theorem Equiv.Perm.sumCongrHom_apply (α : Type u_6) (β : Type u_7) (a : Perm α × Perm β) :

(sumCongrHom α β) a = a.1.sumCongr a.2

source

theorem Equiv.Perm.sumCongrHom_injective {α : Type u_6} {β : Type u_7} :

Function.Injective ⇑(sumCongrHom α β)

source

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

source

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

source

@[simp]

theorem Equiv.Perm.sigmaCongrRight_mul {α : Type u_6} {β : α → Type u_7} (F G : (a : α) → Perm (β a)) :

sigmaCongrRight F * sigmaCongrRight G = sigmaCongrRight (F * G)

source

@[simp]

theorem Equiv.Perm.sigmaCongrRight_inv {α : Type u_6} {β : α → Type u_7} (F : (a : α) → Perm (β a)) :

(sigmaCongrRight F)⁻¹ = sigmaCongrRight fun (a : α) => (F a)⁻¹

source

@[simp]

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

sigmaCongrRight 1 = 1

source

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

Instances For

source

@[simp]

theorem Equiv.Perm.sigmaCongrRightHom_apply {α : Type u_6} (β : α → Type u_7) (F : (a : α) → Perm (β a)) :

(sigmaCongrRightHom β) F = sigmaCongrRight F

source

theorem Equiv.Perm.sigmaCongrRightHom_injective {α : Type u_6} {β : α → Type u_7} :

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

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

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

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

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

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

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_6) [Mul M] :

Type u_6

The group of multiplicative automorphisms.

Equations

Instances For

source

@[reducible]

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

Type u_6

The group of additive automorphisms.

Equations

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

source

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

Inhabited (MulAut M)

Equations

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

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

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_6} [Group H] (ϕ : G ≃* H) :

MulAut G ≃* MulAut H

Isomorphic groups have isomorphic automorphism groups.

Equations

Instances For

source

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

source

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

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

source

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

AddGroup (AddAut M)

Equations

source

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

Inhabited (AddAut A)

Equations

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

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

Instances For

source

@[simp]