Documentation

Mathlib.Algebra.Group.Equiv.Basic

Multiplicative and additive equivs #

This file contains basic results on MulEquiv and AddEquiv.

Tags #

Equiv, MulEquiv, AddEquiv

theorem MulEquivClass.toMulEquiv_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [MulEquivClass F α β] :
theorem AddEquivClass.toAddEquiv_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] :
def MulEquiv.ofUnique {M : Type u_9} {N : Type u_10} [Unique M] [Unique N] [Mul M] [Mul N] :
M ≃* N

The MulEquiv between two monoids with a unique element.

Equations
def AddEquiv.ofUnique {M : Type u_9} {N : Type u_10} [Unique M] [Unique N] [Add M] [Add N] :
M ≃+ N

The AddEquiv between two AddMonoids with a unique element.

Equations
@[deprecated MulEquiv.ofUnique (since := "2024-12-25")]
def MulEquiv.mulEquivOfUnique {M : Type u_9} {N : Type u_10} [Unique M] [Unique N] [Mul M] [Mul N] :
M ≃* N

Alias of MulEquiv.ofUnique.


The MulEquiv between two monoids with a unique element.

Equations
@[deprecated MulEquiv.ofUnique (since := "2024-12-25")]
def AddEquiv.addEquivOfUnique {M : Type u_9} {N : Type u_10} [Unique M] [Unique N] [Add M] [Add N] :
M ≃+ N

Alias of AddEquiv.ofEquiv.

Equations
instance MulEquiv.instUnique {M : Type u_9} {N : Type u_10} [Unique M] [Unique N] [Mul M] [Mul N] :
Unique (M ≃* N)

There is a unique monoid homomorphism between two monoids with a unique element.

Equations
instance AddEquiv.instUnique {M : Type u_9} {N : Type u_10} [Unique M] [Unique N] [Add M] [Add N] :
Unique (M ≃+ N)

There is a unique additive monoid homomorphism between two additive monoids with a unique element.

Equations

Monoids #

def MulEquiv.arrowCongr {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [Mul P] [Mul Q] (f : M N) (g : P ≃* Q) :
(MP) ≃* (NQ)

A multiplicative analogue of Equiv.arrowCongr, where the equivalence between the targets is multiplicative.

Equations
  • MulEquiv.arrowCongr f g = { toFun := fun (h : MP) (n : N) => g (h (f.symm n)), invFun := fun (k : NQ) (m : M) => g.symm (k (f m)), left_inv := , right_inv := , map_mul' := }
def AddEquiv.arrowCongr {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [Add P] [Add Q] (f : M N) (g : P ≃+ Q) :
(MP) ≃+ (NQ)

An additive analogue of Equiv.arrowCongr, where the equivalence between the targets is additive.

Equations
  • AddEquiv.arrowCongr f g = { toFun := fun (h : MP) (n : N) => g (h (f.symm n)), invFun := fun (k : NQ) (m : M) => g.symm (k (f m)), left_inv := , right_inv := , map_add' := }
@[simp]
theorem AddEquiv.arrowCongr_apply {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [Add P] [Add Q] (f : M N) (g : P ≃+ Q) (h : MP) (n : N) :
(arrowCongr f g) h n = g (h (f.symm n))
@[simp]
theorem MulEquiv.arrowCongr_apply {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [Mul P] [Mul Q] (f : M N) (g : P ≃* Q) (h : MP) (n : N) :
(arrowCongr f g) h n = g (h (f.symm n))
def MulEquiv.monoidHomCongr {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) :
(M →* P) ≃* (N →* Q)

A multiplicative analogue of Equiv.arrowCongr, for multiplicative maps from a monoid to a commutative monoid.

Equations
  • One or more equations did not get rendered due to their size.
def AddEquiv.addMonoidHomCongr {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) :
(M →+ P) ≃+ (N →+ Q)

An additive analogue of Equiv.arrowCongr, for additive maps from an additive monoid to a commutative additive monoid.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem MulEquiv.monoidHomCongr_apply {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) (h : M →* P) :
(f.monoidHomCongr g) h = g.toMonoidHom.comp (h.comp f.symm.toMonoidHom)
@[simp]
theorem AddEquiv.addMonoidHomCongr_apply {M : Type u_9} {N : Type u_10} {P : Type u_11} {Q : Type u_12} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) :
(f.addMonoidHomCongr g) h = g.toAddMonoidHom.comp (h.comp f.symm.toAddMonoidHom)
def MulEquiv.piCongrRight {η : Type u_9} {Ms : ηType u_10} {Ns : ηType u_11} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) :
((j : η) → Ms j) ≃* ((j : η) → Ns j)

A family of multiplicative equivalences Π j, (Ms j ≃* Ns j) generates a multiplicative equivalence between Π j, Ms j and Π j, Ns j.

This is the MulEquiv version of Equiv.piCongrRight, and the dependent version of MulEquiv.arrowCongr.

Equations
  • One or more equations did not get rendered due to their size.
def AddEquiv.piCongrRight {η : Type u_9} {Ms : ηType u_10} {Ns : ηType u_11} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
((j : η) → Ms j) ≃+ ((j : η) → Ns j)

A family of additive equivalences Π j, (Ms j ≃+ Ns j) generates an additive equivalence between Π j, Ms j and Π j, Ns j.

This is the AddEquiv version of Equiv.piCongrRight, and the dependent version of AddEquiv.arrowCongr.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddEquiv.piCongrRight_apply {η : Type u_9} {Ms : ηType u_10} {Ns : ηType u_11} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) (x : (j : η) → Ms j) (j : η) :
(piCongrRight es) x j = (es j) (x j)
@[simp]
theorem MulEquiv.piCongrRight_apply {η : Type u_9} {Ms : ηType u_10} {Ns : ηType u_11} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) (x : (j : η) → Ms j) (j : η) :
(piCongrRight es) x j = (es j) (x j)
@[simp]
theorem MulEquiv.piCongrRight_refl {η : Type u_9} {Ms : ηType u_10} [(j : η) → Mul (Ms j)] :
(piCongrRight fun (j : η) => refl (Ms j)) = refl ((j : η) → Ms j)
@[simp]
theorem AddEquiv.piCongrRight_refl {η : Type u_9} {Ms : ηType u_10} [(j : η) → Add (Ms j)] :
(piCongrRight fun (j : η) => refl (Ms j)) = refl ((j : η) → Ms j)
@[simp]
theorem MulEquiv.piCongrRight_symm {η : Type u_9} {Ms : ηType u_10} {Ns : ηType u_11} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) :
(piCongrRight es).symm = piCongrRight fun (i : η) => (es i).symm
@[simp]
theorem AddEquiv.piCongrRight_symm {η : Type u_9} {Ms : ηType u_10} {Ns : ηType u_11} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
(piCongrRight es).symm = piCongrRight fun (i : η) => (es i).symm
@[simp]
theorem MulEquiv.piCongrRight_trans {η : Type u_9} {Ms : ηType u_10} {Ns : ηType u_11} {Ps : ηType u_12} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] [(j : η) → Mul (Ps j)] (es : (j : η) → Ms j ≃* Ns j) (fs : (j : η) → Ns j ≃* Ps j) :
(piCongrRight es).trans (piCongrRight fs) = piCongrRight fun (i : η) => (es i).trans (fs i)
@[simp]
theorem AddEquiv.piCongrRight_trans {η : Type u_9} {Ms : ηType u_10} {Ns : ηType u_11} {Ps : ηType u_12} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] [(j : η) → Add (Ps j)] (es : (j : η) → Ms j ≃+ Ns j) (fs : (j : η) → Ns j ≃+ Ps j) :
(piCongrRight es).trans (piCongrRight fs) = piCongrRight fun (i : η) => (es i).trans (fs i)
def MulEquiv.piUnique {ι : Type u_9} (M : ιType u_10) [(j : ι) → Mul (M j)] [Unique ι] :
((j : ι) → M j) ≃* M default

A family indexed by a type with a unique element is MulEquiv to the element at the single index.

Equations
def AddEquiv.piUnique {ι : Type u_9} (M : ιType u_10) [(j : ι) → Add (M j)] [Unique ι] :
((j : ι) → M j) ≃+ M default

A family indexed by a type with a unique element is AddEquiv to the element at the single index.

Equations
@[simp]
theorem AddEquiv.piUnique_symm_apply {ι : Type u_9} (M : ιType u_10) [(j : ι) → Add (M j)] [Unique ι] (x : M default) (i : ι) :
(piUnique M).symm x i = uniqueElim x i
@[simp]
theorem MulEquiv.piUnique_symm_apply {ι : Type u_9} (M : ιType u_10) [(j : ι) → Mul (M j)] [Unique ι] (x : M default) (i : ι) :
(piUnique M).symm x i = uniqueElim x i
@[simp]
theorem MulEquiv.piUnique_apply {ι : Type u_9} (M : ιType u_10) [(j : ι) → Mul (M j)] [Unique ι] (f : (i : ι) → M i) :
@[simp]
theorem AddEquiv.piUnique_apply {ι : Type u_9} (M : ιType u_10) [(j : ι) → Add (M j)] [Unique ι] (f : (i : ι) → M i) :
def MonoidHom.precompEquiv {α : Type u_9} {β : Type u_10} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_11) [Monoid γ] :
(β →* γ) (α →* γ)

The equivalence (β →* γ) ≃ (α →* γ) obtained by precomposition with a multiplicative equivalence e : α ≃* β.

Equations
  • MonoidHom.precompEquiv e γ = { toFun := fun (f : β →* γ) => f.comp e, invFun := fun (g : α →* γ) => g.comp e.symm, left_inv := , right_inv := }
def AddMonoidHom.precompEquiv {α : Type u_9} {β : Type u_10} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_11) [AddMonoid γ] :
(β →+ γ) (α →+ γ)

The equivalence (β →+ γ) ≃ (α →+ γ) obtained by precomposition with an additive equivalence e : α ≃+ β.

Equations
@[simp]
theorem MonoidHom.precompEquiv_apply {α : Type u_9} {β : Type u_10} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_11) [Monoid γ] (f : β →* γ) :
(precompEquiv e γ) f = f.comp e
@[simp]
theorem MonoidHom.precompEquiv_symm_apply {α : Type u_9} {β : Type u_10} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_11) [Monoid γ] (g : α →* γ) :
(precompEquiv e γ).symm g = g.comp e.symm
@[simp]
theorem AddMonoidHom.precompEquiv_apply {α : Type u_9} {β : Type u_10} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_11) [AddMonoid γ] (f : β →+ γ) :
(precompEquiv e γ) f = f.comp e
@[simp]
theorem AddMonoidHom.precompEquiv_symm_apply {α : Type u_9} {β : Type u_10} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_11) [AddMonoid γ] (g : α →+ γ) :
(precompEquiv e γ).symm g = g.comp e.symm
def MonoidHom.postcompEquiv {α : Type u_9} {β : Type u_10} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_11) [Monoid γ] :
(γ →* α) (γ →* β)

The equivalence (γ →* α) ≃ (γ →* β) obtained by postcomposition with a multiplicative equivalence e : α ≃* β.

Equations
  • MonoidHom.postcompEquiv e γ = { toFun := fun (f : γ →* α) => e.toMonoidHom.comp f, invFun := fun (g : γ →* β) => e.symm.toMonoidHom.comp g, left_inv := , right_inv := }
def AddMonoidHom.postcompEquiv {α : Type u_9} {β : Type u_10} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_11) [AddMonoid γ] :
(γ →+ α) (γ →+ β)

The equivalence (γ →+ α) ≃ (γ →+ β) obtained by postcomposition with an additive equivalence e : α ≃+ β.

Equations
  • AddMonoidHom.postcompEquiv e γ = { toFun := fun (f : γ →+ α) => e.toAddMonoidHom.comp f, invFun := fun (g : γ →+ β) => e.symm.toAddMonoidHom.comp g, left_inv := , right_inv := }
@[simp]
theorem MonoidHom.postcompEquiv_apply {α : Type u_9} {β : Type u_10} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_11) [Monoid γ] (f : γ →* α) :
(postcompEquiv e γ) f = e.toMonoidHom.comp f
@[simp]
theorem AddMonoidHom.postcompEquiv_symm_apply {α : Type u_9} {β : Type u_10} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_11) [AddMonoid γ] (g : γ →+ β) :
(postcompEquiv e γ).symm g = e.symm.toAddMonoidHom.comp g
@[simp]
theorem MonoidHom.postcompEquiv_symm_apply {α : Type u_9} {β : Type u_10} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_11) [Monoid γ] (g : γ →* β) :
(postcompEquiv e γ).symm g = e.symm.toMonoidHom.comp g
@[simp]
theorem AddMonoidHom.postcompEquiv_apply {α : Type u_9} {β : Type u_10} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_11) [AddMonoid γ] (f : γ →+ α) :
(postcompEquiv e γ) f = e.toAddMonoidHom.comp f
def Equiv.inv (G : Type u_7) [InvolutiveInv G] :

Inversion on a Group or GroupWithZero is a permutation of the underlying type.

Equations
def Equiv.neg (G : Type u_7) [InvolutiveNeg G] :

Negation on an AddGroup is a permutation of the underlying type.

Equations
@[simp]
theorem Equiv.inv_apply (G : Type u_7) [InvolutiveInv G] :
@[simp]
theorem Equiv.neg_apply (G : Type u_7) [InvolutiveNeg G] :