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 toMulEquiv

theorem AddEquivClass.toAddEquiv_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] : Function.Injective 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.

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.

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

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

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.

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.

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.

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.

@[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) : (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) : (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.

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.

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

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.

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

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.

@[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) : (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) : (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 : α ≃* β.

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 : α ≃+ β.

@[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 : α ≃* β.

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 : α ≃+ β.

@[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] : Perm G

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

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

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

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