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 α β] : Function.Injective MulEquivClass.toMulEquiv

theorem AddEquivClass.toAddEquiv_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] : Function.Injective AddEquivClass.toAddEquiv

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

• MulEquiv.ofUnique = { toEquiv := Equiv.ofUnique M N, map_mul' := ⋯ }

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

• AddEquiv.ofUnique = { toEquiv := Equiv.ofUnique M N, map_add' := ⋯ }

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

• @MulEquiv.mulEquivOfUnique = @MulEquiv.ofUnique

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

• @AddEquiv.addEquivOfUnique = @AddEquiv.ofUnique

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

• MulEquiv.instUnique = { default := MulEquiv.ofUnique, uniq := ⋯ }

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

• AddEquiv.instUnique = { default := AddEquiv.ofUnique, uniq := ⋯ }

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) : (M → P) ≃* (N → Q)

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

Equations

• MulEquiv.arrowCongr f g = { toFun := fun (h : M → P) (n : N) => g (h (f.symm n)), invFun := fun (k : N → Q) (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) : (M → P) ≃+ (N → Q)

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

Equations

• AddEquiv.arrowCongr f g = { toFun := fun (h : M → P) (n : N) => g (h (f.symm n)), invFun := fun (k : N → Q) (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 : M → P) (n : N) : (AddEquiv.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 : M → P) (n : N) : (MulEquiv.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 : η) : (AddEquiv.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 : η) : (MulEquiv.piCongrRight es) x j = (es j) (x j)

@[simp]

theorem MulEquiv.piCongrRight_refl {η : Type u_9} {Ms : η → Type u_10} [(j : η) → Mul (Ms j)] : (MulEquiv.piCongrRight fun (j : η) => MulEquiv.refl (Ms j)) = MulEquiv.refl ((j : η) → Ms j)

@[simp]

theorem AddEquiv.piCongrRight_refl {η : Type u_9} {Ms : η → Type u_10} [(j : η) → Add (Ms j)] : (AddEquiv.piCongrRight fun (j : η) => AddEquiv.refl (Ms j)) = AddEquiv.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) : (MulEquiv.piCongrRight es).symm = MulEquiv.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) : (AddEquiv.piCongrRight es).symm = AddEquiv.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) : (MulEquiv.piCongrRight es).trans (MulEquiv.piCongrRight fs) = MulEquiv.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) : (AddEquiv.piCongrRight es).trans (AddEquiv.piCongrRight fs) = AddEquiv.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

• MulEquiv.piUnique M = { toEquiv := Equiv.piUnique M, map_mul' := ⋯ }

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

• AddEquiv.piUnique M = { toEquiv := Equiv.piUnique M, map_add' := ⋯ }

@[simp]

theorem AddEquiv.piUnique_symm_apply {ι : Type u_9} (M : ι → Type u_10) [(j : ι) → Add (M j)] [Unique ι] (x : M default) (i : ι) : (AddEquiv.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 : ι) : (MulEquiv.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) : (MulEquiv.piUnique M) f = f default

@[simp]

theorem AddEquiv.piUnique_apply {ι : Type u_9} (M : ι → Type u_10) [(j : ι) → Add (M j)] [Unique ι] (f : (i : ι) → M i) : (AddEquiv.piUnique M) f = f default

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

• AddMonoidHom.precompEquiv e γ = { toFun := fun (f : β →+ γ) => f.comp ↑e, invFun := fun (g : α →+ γ) => g.comp ↑e.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MonoidHom.precompEquiv_apply {α : Type u_9} {β : Type u_10} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_11) [Monoid γ] (f : β →* γ) : (MonoidHom.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 : α →* γ) : (MonoidHom.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 : β →+ γ) : (AddMonoidHom.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 : α →+ γ) : (AddMonoidHom.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 : γ →* α) : (MonoidHom.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 : γ →+ β) : (AddMonoidHom.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 : γ →* β) : (MonoidHom.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 : γ →+ α) : (AddMonoidHom.postcompEquiv e γ) f = e.toAddMonoidHom.comp f

def Equiv.inv (G : Type u_7) [InvolutiveInv G] : Equiv.Perm G

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

Equations

• Equiv.inv G = Function.Involutive.toPerm Inv.inv ⋯

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

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

Equations

• Equiv.neg G = Function.Involutive.toPerm Neg.neg ⋯

@[simp]

theorem Equiv.inv_apply (G : Type u_7) [InvolutiveInv G] : ⇑(Equiv.inv G) = Inv.inv

@[simp]

theorem Equiv.neg_apply (G : Type u_7) [InvolutiveNeg G] : ⇑(Equiv.neg G) = Neg.neg

@[simp]

theorem Equiv.inv_symm {G : Type u_7} [InvolutiveInv G] : Equiv.symm (Equiv.inv G) = Equiv.inv G

@[simp]

theorem Equiv.neg_symm {G : Type u_7} [InvolutiveNeg G] : Equiv.symm (Equiv.neg G) = Equiv.neg G