algebra.hom.equiv - mathlib docs

source

def add_hom.inverse {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : add_hom M N) (g : N → M) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) :

add_hom N M

Makes an additive inverse from a bijection which preserves addition.

Equations

f.inverse g h₁ h₂ = {to_fun := g, map_add' := _}

source

def mul_hom.inverse {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M →ₙ* N) (g : N → M) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) :

N →ₙ* M

Makes a multiplicative inverse from a bijection which preserves multiplication.

Equations

f.inverse g h₁ h₂ = {to_fun := g, map_mul' := _}

source

def add_monoid_hom.inverse {A : Type u_1} {B : Type u_2} [add_monoid A] [add_monoid B] (f : A →+ B) (g : B → A) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) :

B →+ A

The inverse of a bijective add_monoid_hom is an add_monoid_hom.

Equations

f.inverse g h₁ h₂ = {to_fun := g, map_zero' := _, map_add' := _}

source

def monoid_hom.inverse {A : Type u_1} {B : Type u_2} [monoid A] [monoid B] (f : A →* B) (g : B → A) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) :

B →* A

The inverse of a bijective monoid_hom is a monoid_hom.

Equations

f.inverse g h₁ h₂ = {to_fun := g, map_one' := _, map_mul' := _}

source

@[simp]

theorem add_monoid_hom.inverse_apply {A : Type u_1} {B : Type u_2} [add_monoid A] [add_monoid B] (f : A →+ B) (g : B → A) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) (ᾰ : B) :

⇑(f.inverse g h₁ h₂) ᾰ = g ᾰ

source

@[simp]

theorem monoid_hom.inverse_apply {A : Type u_1} {B : Type u_2} [monoid A] [monoid B] (f : A →* B) (g : B → A) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) (ᾰ : B) :

⇑(f.inverse g h₁ h₂) ᾰ = g ᾰ

source

def add_equiv.to_equiv {A : Type u_12} {B : Type u_13} [has_add A] [has_add B] (self : A ≃+ B) :

A ≃ B

The equiv underlying an add_equiv.

source

structure add_equiv (A : Type u_12) (B : Type u_13) [has_add A] [has_add B] :

Type (max u_12 u_13)

to_fun : A → B
inv_fun : B → A
left_inv : function.left_inverse self.inv_fun self.to_fun
right_inv : function.right_inverse self.inv_fun self.to_fun
map_add' : ∀ (x y : A), self.to_fun (x + y) = self.to_fun x + self.to_fun y

add_equiv α β is the type of an equiv α ≃ β which preserves addition.

source

def add_equiv.to_add_hom {A : Type u_12} {B : Type u_13} [has_add A] [has_add B] (self : A ≃+ B) :

add_hom A B

The add_hom underlying a add_equiv.

source

@[instance]

def add_equiv_class.to_equiv_like (F : Type u_12) (A : Type u_13) (B : Type u_14) [has_add A] [has_add B] [self : add_equiv_class F A B] :

equiv_like F A B

source

@[class]

structure add_equiv_class (F : Type u_12) (A : Type u_13) (B : Type u_14) [has_add A] [has_add B] :

Type (max u_12 u_13 u_14)

coe : F → A → B
inv : F → B → A
left_inv : ∀ (e : F), function.left_inverse (add_equiv_class.inv e) (add_equiv_class.coe e)
right_inv : ∀ (e : F), function.right_inverse (add_equiv_class.inv e) (add_equiv_class.coe e)
coe_injective' : ∀ (e g : F), add_equiv_class.coe e = add_equiv_class.coe g → add_equiv_class.inv e = add_equiv_class.inv g → e = g
map_add : ∀ (f : F) (a b : A), ⇑f (a + b) = ⇑f a + ⇑f b

add_equiv_class F A B states that F is a type of addition-preserving morphisms. You should extend this class when you extend add_equiv.

Instances

source

def mul_equiv.to_mul_hom {M : Type u_12} {N : Type u_13} [has_mul M] [has_mul N] (self : M ≃* N) :

M →ₙ* N

The mul_hom underlying a mul_equiv.

source

def mul_equiv.to_equiv {M : Type u_12} {N : Type u_13} [has_mul M] [has_mul N] (self : M ≃* N) :

M ≃ N

The equiv underlying a mul_equiv.

source

structure mul_equiv (M : Type u_12) (N : Type u_13) [has_mul M] [has_mul N] :

Type (max u_12 u_13)

to_fun : M → N
inv_fun : N → M
left_inv : function.left_inverse self.inv_fun self.to_fun
right_inv : function.right_inverse self.inv_fun self.to_fun
map_mul' : ∀ (x y : M), self.to_fun (x * y) = (self.to_fun x) * self.to_fun y

mul_equiv α β is the type of an equiv α ≃ β which preserves multiplication.

source

@[class]

structure mul_equiv_class (F : Type u_12) (A : Type u_13) (B : Type u_14) [has_mul A] [has_mul B] :

Type (max u_12 u_13 u_14)

coe : F → A → B
inv : F → B → A
left_inv : ∀ (e : F), function.left_inverse (mul_equiv_class.inv e) (mul_equiv_class.coe e)
right_inv : ∀ (e : F), function.right_inverse (mul_equiv_class.inv e) (mul_equiv_class.coe e)
coe_injective' : ∀ (e g : F), mul_equiv_class.coe e = mul_equiv_class.coe g → mul_equiv_class.inv e = mul_equiv_class.inv g → e = g
map_mul : ∀ (f : F) (a b : A), ⇑f (a * b) = (⇑f a) * ⇑f b

mul_equiv_class F A B states that F is a type of multiplication-preserving morphisms. You should extend this class when you extend mul_equiv.

Instances

source

@[instance]

def mul_equiv_class.to_equiv_like (F : Type u_12) (A : Type u_13) (B : Type u_14) [has_mul A] [has_mul B] [self : mul_equiv_class F A B] :

equiv_like F A B

source

@[protected, instance]

def mul_equiv_class.mul_hom_class (F : Type u_1) {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] [h : mul_equiv_class F M N] :

mul_hom_class F M N

Equations

mul_equiv_class.mul_hom_class F = {coe := mul_equiv_class.coe h, coe_injective' := _, map_mul := _}

source

@[protected, instance]

def add_equiv_class.add_hom_class (F : Type u_1) {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] [h : add_equiv_class F M N] :

add_hom_class F M N

Equations

add_equiv_class.add_hom_class F = {coe := add_equiv_class.coe h, coe_injective' := _, map_add := _}

source

@[protected, instance]

def mul_equiv_class.monoid_hom_class (F : Type u_1) {M : Type u_6} {N : Type u_7} [mul_one_class M] [mul_one_class N] [mul_equiv_class F M N] :

monoid_hom_class F M N

Equations

mul_equiv_class.monoid_hom_class F = {coe := mul_equiv_class.coe _inst_3, coe_injective' := _, map_mul := _, map_one := _}

source

@[protected, instance]

def add_equiv_class.add_monoid_hom_class (F : Type u_1) {M : Type u_6} {N : Type u_7} [add_zero_class M] [add_zero_class N] [add_equiv_class F M N] :

add_monoid_hom_class F M N

Equations

add_equiv_class.add_monoid_hom_class F = {coe := add_equiv_class.coe _inst_3, coe_injective' := _, map_add := _, map_zero := _}

source

@[protected, instance]

def mul_equiv_class.to_monoid_with_zero_hom_class (F : Type u_1) {α : Type u_2} {β : Type u_3} [mul_zero_one_class α] [mul_zero_one_class β] [mul_equiv_class F α β] :

monoid_with_zero_hom_class F α β

Equations

mul_equiv_class.to_monoid_with_zero_hom_class F = {coe := monoid_hom_class.coe (mul_equiv_class.monoid_hom_class F), coe_injective' := _, map_mul := _, map_one := _, map_zero := _}

source

@[simp]

theorem add_equiv_class.map_eq_zero_iff {F : Type u_1} {M : Type u_2} {N : Type u_3} [add_zero_class M] [add_zero_class N] [add_equiv_class F M N] (h : F) {x : M} :

⇑h x = 0 ↔ x = 0

source

@[simp]

theorem mul_equiv_class.map_eq_one_iff {F : Type u_1} {M : Type u_2} {N : Type u_3} [mul_one_class M] [mul_one_class N] [mul_equiv_class F M N] (h : F) {x : M} :

⇑h x = 1 ↔ x = 1

source

theorem mul_equiv_class.map_ne_one_iff {F : Type u_1} {M : Type u_2} {N : Type u_3} [mul_one_class M] [mul_one_class N] [mul_equiv_class F M N] (h : F) {x : M} :

⇑h x ≠ 1 ↔ x ≠ 1

source

theorem add_equiv_class.map_ne_zero_iff {F : Type u_1} {M : Type u_2} {N : Type u_3} [add_zero_class M] [add_zero_class N] [add_equiv_class F M N] (h : F) {x : M} :

⇑h x ≠ 0 ↔ x ≠ 0

source

@[protected, instance]

def mul_equiv.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_mul α] [has_mul β] [mul_equiv_class F α β] :

has_coe_t F (α ≃* β)

Equations

mul_equiv.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, inv_fun := equiv_like.inv f, left_inv := _, right_inv := _, map_mul' := _}}

source

@[protected, instance]

def add_equiv.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_add α] [has_add β] [add_equiv_class F α β] :

has_coe_t F (α ≃+ β)

Equations

add_equiv.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, inv_fun := equiv_like.inv f, left_inv := _, right_inv := _, map_add' := _}}

source

@[protected, instance]

def add_equiv.has_coe_to_fun {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] :

has_coe_to_fun (M ≃+ N) (λ (_x : M ≃+ N), M → N)

Equations

add_equiv.has_coe_to_fun = {coe := add_equiv.to_fun _inst_2}

source

@[protected, instance]

def mul_equiv.has_coe_to_fun {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] :

has_coe_to_fun (M ≃* N) (λ (_x : M ≃* N), M → N)

Equations

mul_equiv.has_coe_to_fun = {coe := mul_equiv.to_fun _inst_2}

source

@[protected, instance]

def mul_equiv.mul_equiv_class {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] :

mul_equiv_class (M ≃* N) M N

Equations

mul_equiv.mul_equiv_class = {coe := mul_equiv.to_fun _inst_2, inv := mul_equiv.inv_fun _inst_2, left_inv := _, right_inv := _, coe_injective' := _, map_mul := _}

source

@[protected, instance]

def add_equiv.add_equiv_class {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] :

add_equiv_class (M ≃+ N) M N

Equations

add_equiv.add_equiv_class = {coe := add_equiv.to_fun _inst_2, inv := add_equiv.inv_fun _inst_2, left_inv := _, right_inv := _, coe_injective' := _, map_add := _}

source

@[simp]

theorem add_equiv.to_equiv_eq_coe {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M ≃+ N) :

f.to_equiv = ↑f

source

@[simp]

theorem mul_equiv.to_equiv_eq_coe {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M ≃* N) :

f.to_equiv = ↑f

source

@[simp]

theorem mul_equiv.to_fun_eq_coe {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f : M ≃* N} :

f.to_fun = ⇑f

source

@[simp]

theorem add_equiv.to_fun_eq_coe {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f : M ≃+ N} :

f.to_fun = ⇑f

source

@[simp]

theorem mul_equiv.coe_to_equiv {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f : M ≃* N} :

⇑↑f = ⇑f

source

@[simp]

theorem add_equiv.coe_to_equiv {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f : M ≃+ N} :

⇑↑f = ⇑f

source

@[simp]

theorem mul_equiv.coe_to_mul_hom {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f : M ≃* N} :

⇑(f.to_mul_hom) = ⇑f

source

@[simp]

theorem add_equiv.coe_to_add_hom {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f : M ≃+ N} :

⇑(f.to_add_hom) = ⇑f

source

@[protected]

theorem add_equiv.map_add {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M ≃+ N) (x y : M) :

⇑f (x + y) = ⇑f x + ⇑f y

An additive isomorphism preserves addition.

source

@[protected]

theorem mul_equiv.map_mul {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M ≃* N) (x y : M) :

⇑f (x * y) = (⇑f x) * ⇑f y

A multiplicative isomorphism preserves multiplication.

source

def add_equiv.mk' {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M ≃ N) (h : ∀ (x y : M), ⇑f (x + y) = ⇑f x + ⇑f y) :

M ≃+ N

Makes an additive isomorphism from a bijection which preserves addition.

Equations

add_equiv.mk' f h = {to_fun := f.to_fun, inv_fun := f.inv_fun, left_inv := _, right_inv := _, map_add' := h}

source

def mul_equiv.mk' {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M ≃ N) (h : ∀ (x y : M), ⇑f (x * y) = (⇑f x) * ⇑f y) :

M ≃* N

Makes a multiplicative isomorphism from a bijection which preserves multiplication.

Equations

mul_equiv.mk' f h = {to_fun := f.to_fun, inv_fun := f.inv_fun, left_inv := _, right_inv := _, map_mul' := h}

source

@[protected]

theorem add_equiv.bijective {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :

function.bijective ⇑e

source

@[protected]

theorem mul_equiv.bijective {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :

function.bijective ⇑e

source

@[protected]

theorem mul_equiv.injective {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :

function.injective ⇑e

source

@[protected]

theorem add_equiv.injective {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :

function.injective ⇑e

source

@[protected]

theorem mul_equiv.surjective {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :

function.surjective ⇑e

source

@[protected]

theorem add_equiv.surjective {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :

function.surjective ⇑e

source

def add_equiv.refl (M : Type u_1) [has_add M] :

M ≃+ M

The identity map is an additive isomorphism.

Equations

add_equiv.refl M = {to_fun := (equiv.refl M).to_fun, inv_fun := (equiv.refl M).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

def mul_equiv.refl (M : Type u_1) [has_mul M] :

M ≃* M

The identity map is a multiplicative isomorphism.

Equations

mul_equiv.refl M = {to_fun := (equiv.refl M).to_fun, inv_fun := (equiv.refl M).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

@[protected, instance]

def add_equiv.inhabited {M : Type u_6} [has_add M] :

inhabited (M ≃+ M)

Equations

add_equiv.inhabited = {default := add_equiv.refl M _inst_1}

source

@[protected, instance]

def mul_equiv.inhabited {M : Type u_6} [has_mul M] :

inhabited (M ≃* M)

Equations

mul_equiv.inhabited = {default := mul_equiv.refl M _inst_1}

source

def add_equiv.symm {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (h : M ≃+ N) :

N ≃+ M

The inverse of an isomorphism is an isomorphism.

Equations

h.symm = {to_fun := h.to_equiv.symm.to_fun, inv_fun := h.to_equiv.symm.inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

def mul_equiv.symm {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (h : M ≃* N) :

N ≃* M

The inverse of an isomorphism is an isomorphism.

Equations

h.symm = {to_fun := h.to_equiv.symm.to_fun, inv_fun := h.to_equiv.symm.inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem mul_equiv.inv_fun_eq_symm {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f : M ≃* N} :

f.inv_fun = ⇑(f.symm)

source

@[simp]

theorem add_equiv.neg_fun_eq_symm {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f : M ≃+ N} :

f.inv_fun = ⇑(f.symm)

source

def add_equiv.simps.symm_apply {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :

N → M

See Note custom simps projection

Equations

add_equiv.simps.symm_apply e = ⇑(e.symm)

source

def mul_equiv.simps.symm_apply {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :

N → M

See Note [custom simps projection]

Equations

mul_equiv.simps.symm_apply e = ⇑(e.symm)

source

@[simp]

theorem mul_equiv.to_equiv_symm {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M ≃* N) :

f.symm.to_equiv = f.to_equiv.symm

source

@[simp]

theorem add_equiv.to_equiv_symm {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M ≃+ N) :

f.symm.to_equiv = f.to_equiv.symm

source

@[simp]

theorem mul_equiv.coe_mk {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x * y) = (f x) * f y) :

⇑{to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_mul' := h₃} = f

source

@[simp]

theorem add_equiv.coe_mk {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x + y) = f x + f y) :

⇑{to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_add' := h₃} = f

source

@[simp]

theorem mul_equiv.to_equiv_mk {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x * y) = (f x) * f y) :

{to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_mul' := h₃}.to_equiv = {to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂}

source

@[simp]

theorem add_equiv.to_equiv_mk {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x + y) = f x + f y) :

{to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_add' := h₃}.to_equiv = {to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂}

source

@[simp]

theorem mul_equiv.symm_symm {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M ≃* N) :

f.symm.symm = f

source

@[simp]

theorem add_equiv.symm_symm {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M ≃+ N) :

f.symm.symm = f

source

theorem mul_equiv.symm_bijective {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] :

function.bijective mul_equiv.symm

source

theorem add_equiv.symm_bijective {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] :

function.bijective add_equiv.symm

source

@[simp]

theorem mul_equiv.symm_mk {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x * y) = (f x) * f y) :

{to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_mul' := h₃}.symm = {to_fun := g, inv_fun := f, left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem add_equiv.symm_mk {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x + y) = f x + f y) :

{to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_add' := h₃}.symm = {to_fun := g, inv_fun := f, left_inv := _, right_inv := _, map_add' := _}

source

def mul_equiv.trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_mul M] [has_mul N] [has_mul P] (h1 : M ≃* N) (h2 : N ≃* P) :

M ≃* P

Transitivity of multiplication-preserving isomorphisms

Equations

h1.trans h2 = {to_fun := (h1.to_equiv.trans h2.to_equiv).to_fun, inv_fun := (h1.to_equiv.trans h2.to_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

def add_equiv.trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_add M] [has_add N] [has_add P] (h1 : M ≃+ N) (h2 : N ≃+ P) :

M ≃+ P

Transitivity of addition-preserving isomorphisms

Equations

h1.trans h2 = {to_fun := (h1.to_equiv.trans h2.to_equiv).to_fun, inv_fun := (h1.to_equiv.trans h2.to_equiv).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

@[simp]

theorem mul_equiv.apply_symm_apply {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) (y : N) :

⇑e (⇑(e.symm) y) = y

e.symm is a right inverse of e, written as e (e.symm y) = y.

source

@[simp]

theorem add_equiv.apply_symm_apply {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) (y : N) :

⇑e (⇑(e.symm) y) = y

e.symm is a right inverse of e, written as e (e.symm y) = y.

source

@[simp]

theorem mul_equiv.symm_apply_apply {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) (x : M) :

⇑(e.symm) (⇑e x) = x

e.symm is a left inverse of e, written as e.symm (e y) = y.

source

@[simp]

theorem add_equiv.symm_apply_apply {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) (x : M) :

⇑(e.symm) (⇑e x) = x

e.symm is a left inverse of e, written as e.symm (e y) = y.

source

@[simp]

theorem mul_equiv.symm_comp_self {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :

⇑(e.symm) ∘ ⇑e = id

source

@[simp]

theorem add_equiv.symm_comp_self {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :

⇑(e.symm) ∘ ⇑e = id

source

@[simp]

theorem add_equiv.self_comp_symm {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :

⇑e ∘ ⇑(e.symm) = id

source

@[simp]

theorem mul_equiv.self_comp_symm {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :

⇑e ∘ ⇑(e.symm) = id

source

@[simp]

theorem mul_equiv.coe_refl {M : Type u_6} [has_mul M] :

⇑(mul_equiv.refl M) = id

source

@[simp]

theorem add_equiv.coe_refl {M : Type u_6} [has_add M] :

⇑(add_equiv.refl M) = id

source

theorem add_equiv.refl_apply {M : Type u_6} [has_add M] (m : M) :

⇑(add_equiv.refl M) m = m

source

theorem mul_equiv.refl_apply {M : Type u_6} [has_mul M] (m : M) :

⇑(mul_equiv.refl M) m = m

source

@[simp]

theorem mul_equiv.coe_trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_mul M] [has_mul N] [has_mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) :

⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁

source

@[simp]

theorem add_equiv.coe_trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_add M] [has_add N] [has_add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :

⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁

source

theorem mul_equiv.trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_mul M] [has_mul N] [has_mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) :

⇑(e₁.trans e₂) m = ⇑e₂ (⇑e₁ m)

source

theorem add_equiv.trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_add M] [has_add N] [has_add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (m : M) :

⇑(e₁.trans e₂) m = ⇑e₂ (⇑e₁ m)

source

@[simp]

theorem add_equiv.symm_trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_add M] [has_add N] [has_add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (p : P) :

⇑((e₁.trans e₂).symm) p = ⇑(e₁.symm) (⇑(e₂.symm) p)

source

@[simp]

theorem mul_equiv.symm_trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_mul M] [has_mul N] [has_mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) :

⇑((e₁.trans e₂).symm) p = ⇑(e₁.symm) (⇑(e₂.symm) p)

source

@[simp]

theorem add_equiv.apply_eq_iff_eq {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) {x y : M} :

⇑e x = ⇑e y ↔ x = y

source

@[simp]

theorem mul_equiv.apply_eq_iff_eq {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) {x y : M} :

⇑e x = ⇑e y ↔ x = y

source

theorem add_equiv.apply_eq_iff_symm_apply {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) {x : M} {y : N} :

⇑e x = y ↔ x = ⇑(e.symm) y

source

theorem mul_equiv.apply_eq_iff_symm_apply {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) {x : M} {y : N} :

⇑e x = y ↔ x = ⇑(e.symm) y

source

theorem add_equiv.symm_apply_eq {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) {x : N} {y : M} :

⇑(e.symm) x = y ↔ x = ⇑e y

source

theorem mul_equiv.symm_apply_eq {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) {x : N} {y : M} :

⇑(e.symm) x = y ↔ x = ⇑e y

source

theorem mul_equiv.eq_symm_apply {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) {x : N} {y : M} :

y = ⇑(e.symm) x ↔ ⇑e y = x

source

theorem add_equiv.eq_symm_apply {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) {x : N} {y : M} :

y = ⇑(e.symm) x ↔ ⇑e y = x

source

theorem add_equiv.eq_comp_symm {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {α : Type u_1} (e : M ≃+ N) (f : N → α) (g : M → α) :

f = g ∘ ⇑(e.symm) ↔ f ∘ ⇑e = g

source

theorem mul_equiv.eq_comp_symm {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {α : Type u_1} (e : M ≃* N) (f : N → α) (g : M → α) :

f = g ∘ ⇑(e.symm) ↔ f ∘ ⇑e = g

source

theorem mul_equiv.comp_symm_eq {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {α : Type u_1} (e : M ≃* N) (f : N → α) (g : M → α) :

g ∘ ⇑(e.symm) = f ↔ g = f ∘ ⇑e

source

theorem add_equiv.comp_symm_eq {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {α : Type u_1} (e : M ≃+ N) (f : N → α) (g : M → α) :

g ∘ ⇑(e.symm) = f ↔ g = f ∘ ⇑e

source

theorem mul_equiv.eq_symm_comp {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {α : Type u_1} (e : M ≃* N) (f : α → M) (g : α → N) :

f = ⇑(e.symm) ∘ g ↔ ⇑e ∘ f = g

source

theorem add_equiv.eq_symm_comp {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {α : Type u_1} (e : M ≃+ N) (f : α → M) (g : α → N) :

f = ⇑(e.symm) ∘ g ↔ ⇑e ∘ f = g

source

theorem add_equiv.symm_comp_eq {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {α : Type u_1} (e : M ≃+ N) (f : α → M) (g : α → N) :

⇑(e.symm) ∘ g = f ↔ g = ⇑e ∘ f

source

theorem mul_equiv.symm_comp_eq {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {α : Type u_1} (e : M ≃* N) (f : α → M) (g : α → N) :

⇑(e.symm) ∘ g = f ↔ g = ⇑e ∘ f

source

theorem add_equiv.ext {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f g : M ≃+ N} (h : ∀ (x : M), ⇑f x = ⇑g x) :

f = g

Two additive isomorphisms agree if they are defined by the same underlying function.

source

@[ext]

theorem mul_equiv.ext {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f g : M ≃* N} (h : ∀ (x : M), ⇑f x = ⇑g x) :

f = g

Two multiplicative isomorphisms agree if they are defined by the same underlying function.

source

theorem add_equiv.ext_iff {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f g : M ≃+ N} :

f = g ↔ ∀ (x : M), ⇑f x = ⇑g x

source

theorem mul_equiv.ext_iff {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f g : M ≃* N} :

f = g ↔ ∀ (x : M), ⇑f x = ⇑g x

source

@[simp]

theorem mul_equiv.mk_coe {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) (e' : N → M) (h₁ : function.left_inverse e' ⇑e) (h₂ : function.right_inverse e' ⇑e) (h₃ : ∀ (x y : M), ⇑e (x * y) = (⇑e x) * ⇑e y) :

{to_fun := ⇑e, inv_fun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃} = e

source

@[simp]

theorem add_equiv.mk_coe {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) (e' : N → M) (h₁ : function.left_inverse e' ⇑e) (h₂ : function.right_inverse e' ⇑e) (h₃ : ∀ (x y : M), ⇑e (x + y) = ⇑e x + ⇑e y) :

{to_fun := ⇑e, inv_fun := e', left_inv := h₁, right_inv := h₂, map_add' := h₃} = e

source

@[simp]

theorem mul_equiv.mk_coe' {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) (f : N → M) (h₁ : function.left_inverse ⇑e f) (h₂ : function.right_inverse ⇑e f) (h₃ : ∀ (x y : N), f (x * y) = (f x) * f y) :

{to_fun := f, inv_fun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃} = e.symm

source

@[simp]

theorem add_equiv.mk_coe' {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) (f : N → M) (h₁ : function.left_inverse ⇑e f) (h₂ : function.right_inverse ⇑e f) (h₃ : ∀ (x y : N), f (x + y) = f x + f y) :

{to_fun := f, inv_fun := ⇑e, left_inv := h₁, right_inv := h₂, map_add' := h₃} = e.symm

source

@[protected]

theorem add_equiv.congr_arg {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f : M ≃+ N} {x x' : M} :

x = x' → ⇑f x = ⇑f x'

source

@[protected]

theorem mul_equiv.congr_arg {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f : M ≃* N} {x x' : M} :

x = x' → ⇑f x = ⇑f x'

source

@[protected]

theorem add_equiv.congr_fun {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f g : M ≃+ N} (h : f = g) (x : M) :

⇑f x = ⇑g x

source

@[protected]

theorem mul_equiv.congr_fun {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f g : M ≃* N} (h : f = g) (x : M) :

⇑f x = ⇑g x

source

def add_equiv.add_equiv_of_unique_of_unique {M : Type u_1} {N : Type u_2} [unique M] [unique N] [has_add M] [has_add N] :

M ≃+ N

The add_equiv between two add_monoids with a unique element.

Equations

add_equiv.add_equiv_of_unique_of_unique = {to_fun := equiv_of_unique_of_unique.to_fun, inv_fun := equiv_of_unique_of_unique.inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

def mul_equiv.mul_equiv_of_unique_of_unique {M : Type u_1} {N : Type u_2} [unique M] [unique N] [has_mul M] [has_mul N] :

M ≃* N

The mul_equiv between two monoids with a unique element.

Equations

mul_equiv.mul_equiv_of_unique_of_unique = {to_fun := equiv_of_unique_of_unique.to_fun, inv_fun := equiv_of_unique_of_unique.inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

@[protected, instance]

def add_equiv.unique {M : Type u_1} {N : Type u_2} [unique M] [unique N] [has_add M] [has_add N] :

unique (M ≃+ N)

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

Equations

add_equiv.unique = {to_inhabited := {default := add_equiv.add_equiv_of_unique_of_unique _inst_8}, uniq := _}

source

@[protected, instance]

def mul_equiv.unique {M : Type u_1} {N : Type u_2} [unique M] [unique N] [has_mul M] [has_mul N] :

unique (M ≃* N)

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

Equations

mul_equiv.unique = {to_inhabited := {default := mul_equiv.mul_equiv_of_unique_of_unique _inst_8}, uniq := _}

source

@[protected]

theorem add_equiv.map_zero {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (h : M ≃+ N) :

⇑h 0 = 0

An additive isomorphism of additive monoids sends 0 to 0 (and is hence an additive monoid isomorphism).

source

@[protected]

theorem mul_equiv.map_one {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (h : M ≃* N) :

⇑h 1 = 1

A multiplicative isomorphism of monoids sends 1 to 1 (and is hence a monoid isomorphism).

source

@[protected]

theorem add_equiv.map_eq_zero_iff {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (h : M ≃+ N) {x : M} :

⇑h x = 0 ↔ x = 0

source

@[protected]

theorem mul_equiv.map_eq_one_iff {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (h : M ≃* N) {x : M} :

⇑h x = 1 ↔ x = 1

source

theorem add_equiv.map_ne_zero_iff {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (h : M ≃+ N) {x : M} :

⇑h x ≠ 0 ↔ x ≠ 0

source

theorem mul_equiv.map_ne_one_iff {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (h : M ≃* N) {x : M} :

⇑h x ≠ 1 ↔ x ≠ 1

source

noncomputable def add_equiv.of_bijective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (hf : function.bijective ⇑f) :

M ≃+ N

A bijective add_monoid homomorphism is an isomorphism

Equations

add_equiv.of_bijective f hf = {to_fun := (equiv.of_bijective ⇑f hf).to_fun, inv_fun := (equiv.of_bijective ⇑f hf).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

noncomputable def mul_equiv.of_bijective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (hf : function.bijective ⇑f) :

M ≃* N

A bijective monoid homomorphism is an isomorphism

Equations

mul_equiv.of_bijective f hf = {to_fun := (equiv.of_bijective ⇑f hf).to_fun, inv_fun := (equiv.of_bijective ⇑f hf).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

def add_equiv.to_add_monoid_hom {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (h : M ≃+ N) :

M →+ N

Extract the forward direction of an additive equivalence as an addition-preserving function.

Equations

h.to_add_monoid_hom = {to_fun := h.to_fun, map_zero' := _, map_add' := _}

source

def mul_equiv.to_monoid_hom {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (h : M ≃* N) :

M →* N

Extract the forward direction of a multiplicative equivalence as a multiplication-preserving function.

Equations

h.to_monoid_hom = {to_fun := h.to_fun, map_one' := _, map_mul' := _}

source

@[simp]

theorem mul_equiv.coe_to_monoid_hom {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (e : M ≃* N) :

⇑(e.to_monoid_hom) = ⇑e

source

@[simp]

theorem add_equiv.coe_to_add_monoid_hom {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (e : M ≃+ N) :

⇑(e.to_add_monoid_hom) = ⇑e

source

theorem mul_equiv.to_monoid_hom_injective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

function.injective mul_equiv.to_monoid_hom

source

theorem add_equiv.to_add_monoid_hom_injective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

function.injective add_equiv.to_add_monoid_hom

source

@[simp]

theorem add_equiv.arrow_congr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [add_zero_class P] [add_zero_class Q] (f : M ≃ N) (g : P ≃+ Q) (h : M → P) (n : N) :

⇑(add_equiv.arrow_congr f g) h n = ⇑g (h (⇑(f.symm) n))

source

def add_equiv.arrow_congr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [add_zero_class P] [add_zero_class Q] (f : M ≃ N) (g : P ≃+ Q) :

(M → P) ≃+ (N → Q)

An additive analogue of equiv.arrow_congr, where the equivalence between the targets is additive.

Equations

add_equiv.arrow_congr f g = {to_fun := λ (h : M → P) (n : N), ⇑g (h (⇑(f.symm) n)), inv_fun := λ (k : N → Q) (m : M), ⇑(g.symm) (k (⇑f m)), left_inv := _, right_inv := _, map_add' := _}

source

def mul_equiv.arrow_congr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [mul_one_class P] [mul_one_class Q] (f : M ≃ N) (g : P ≃* Q) :

(M → P) ≃* (N → Q)

A multiplicative analogue of equiv.arrow_congr, where the equivalence between the targets is multiplicative.

Equations

mul_equiv.arrow_congr f g = {to_fun := λ (h : M → P) (n : N), ⇑g (h (⇑(f.symm) n)), inv_fun := λ (k : N → Q) (m : M), ⇑(g.symm) (k (⇑f m)), left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem mul_equiv.arrow_congr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [mul_one_class P] [mul_one_class Q] (f : M ≃ N) (g : P ≃* Q) (h : M → P) (n : N) :

⇑(mul_equiv.arrow_congr f g) h n = ⇑g (h (⇑(f.symm) n))

source

def add_equiv.add_monoid_hom_congr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] [add_comm_monoid Q] (f : M ≃+ N) (g : P ≃+ Q) :

(M →+ P) ≃+ (N →+ Q)

An additive analogue of equiv.arrow_congr, for additive maps from an additive monoid to a commutative additive monoid.

Equations

f.add_monoid_hom_congr g = {to_fun := λ (h : M →+ P), g.to_add_monoid_hom.comp (h.comp f.symm.to_add_monoid_hom), inv_fun := λ (k : N →+ Q), g.symm.to_add_monoid_hom.comp (k.comp f.to_add_monoid_hom), left_inv := _, right_inv := _, map_add' := _}

source

@[simp]

theorem add_equiv.add_monoid_hom_congr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] [add_comm_monoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) :

⇑(f.add_monoid_hom_congr g) h = g.to_add_monoid_hom.comp (h.comp f.symm.to_add_monoid_hom)

source

def mul_equiv.monoid_hom_congr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [mul_one_class M] [mul_one_class N] [comm_monoid P] [comm_monoid Q] (f : M ≃* N) (g : P ≃* Q) :

(M →* P) ≃* (N →* Q)

A multiplicative analogue of equiv.arrow_congr, for multiplicative maps from a monoid to a commutative monoid.

Equations

f.monoid_hom_congr g = {to_fun := λ (h : M →* P), g.to_monoid_hom.comp (h.comp f.symm.to_monoid_hom), inv_fun := λ (k : N →* Q), g.symm.to_monoid_hom.comp (k.comp f.to_monoid_hom), left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem mul_equiv.monoid_hom_congr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [mul_one_class M] [mul_one_class N] [comm_monoid P] [comm_monoid Q] (f : M ≃* N) (g : P ≃* Q) (h : M →* P) :

⇑(f.monoid_hom_congr g) h = g.to_monoid_hom.comp (h.comp f.symm.to_monoid_hom)

source

@[simp]

theorem mul_equiv.Pi_congr_right_apply {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [Π (j : η), mul_one_class (Ms j)] [Π (j : η), mul_one_class (Ns j)] (es : Π (j : η), Ms j ≃* Ns j) (x : Π (j : η), Ms j) (j : η) :

⇑(mul_equiv.Pi_congr_right es) x j = ⇑(es j) (x j)

source

@[simp]

theorem add_equiv.Pi_congr_right_apply {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [Π (j : η), add_zero_class (Ms j)] [Π (j : η), add_zero_class (Ns j)] (es : Π (j : η), Ms j ≃+ Ns j) (x : Π (j : η), Ms j) (j : η) :

⇑(add_equiv.Pi_congr_right es) x j = ⇑(es j) (x j)

source

def add_equiv.Pi_congr_right {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [Π (j : η), add_zero_class (Ms j)] [Π (j : η), add_zero_class (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 add_equiv version of equiv.Pi_congr_right, and the dependent version of add_equiv.arrow_congr.

Equations

add_equiv.Pi_congr_right es = {to_fun := λ (x : Π (j : η), Ms j) (j : η), ⇑(es j) (x j), inv_fun := λ (x : Π (j : η), Ns j) (j : η), ⇑((es j).symm) (x j), left_inv := _, right_inv := _, map_add' := _}

source

def mul_equiv.Pi_congr_right {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [Π (j : η), mul_one_class (Ms j)] [Π (j : η), mul_one_class (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 mul_equiv version of equiv.Pi_congr_right, and the dependent version of mul_equiv.arrow_congr.

Equations

mul_equiv.Pi_congr_right es = {to_fun := λ (x : Π (j : η), Ms j) (j : η), ⇑(es j) (x j), inv_fun := λ (x : Π (j : η), Ns j) (j : η), ⇑((es j).symm) (x j), left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem mul_equiv.Pi_congr_right_refl {η : Type u_1} {Ms : η → Type u_2} [Π (j : η), mul_one_class (Ms j)] :

mul_equiv.Pi_congr_right (λ (j : η), mul_equiv.refl (Ms j)) = mul_equiv.refl (Π (j : η), Ms j)

source

@[simp]

theorem mul_equiv.Pi_congr_right_symm {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [Π (j : η), mul_one_class (Ms j)] [Π (j : η), mul_one_class (Ns j)] (es : Π (j : η), Ms j ≃* Ns j) :

(mul_equiv.Pi_congr_right es).symm = mul_equiv.Pi_congr_right (λ (i : η), (es i).symm)

source

@[simp]

theorem mul_equiv.Pi_congr_right_trans {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} {Ps : η → Type u_4} [Π (j : η), mul_one_class (Ms j)] [Π (j : η), mul_one_class (Ns j)] [Π (j : η), mul_one_class (Ps j)] (es : Π (j : η), Ms j ≃* Ns j) (fs : Π (j : η), Ns j ≃* Ps j) :

(mul_equiv.Pi_congr_right es).trans (mul_equiv.Pi_congr_right fs) = mul_equiv.Pi_congr_right (λ (i : η), (es i).trans (fs i))

source

@[simp]

theorem mul_equiv.Pi_subsingleton_apply {ι : Type u_1} (M : ι → Type u_2) [Π (j : ι), has_mul (M j)] [subsingleton ι] (i : ι) (ᾰ : Π (a' : ι), M a') :

⇑(mul_equiv.Pi_subsingleton M i) ᾰ = (equiv.Pi_subsingleton M i).to_fun ᾰ

source

@[simp]

theorem mul_equiv.Pi_subsingleton_symm_apply {ι : Type u_1} (M : ι → Type u_2) [Π (j : ι), has_mul (M j)] [subsingleton ι] (i : ι) (ᾰ : M i) (a' : ι) :

⇑((mul_equiv.Pi_subsingleton M i).symm) ᾰ a' = (equiv.Pi_subsingleton M i).inv_fun ᾰ a'

source

def mul_equiv.Pi_subsingleton {ι : Type u_1} (M : ι → Type u_2) [Π (j : ι), has_mul (M j)] [subsingleton ι] (i : ι) :

(Π (j : ι), M j) ≃* M i

A family indexed by a nonempty subsingleton type is equivalent to the element at the single index.

Equations

mul_equiv.Pi_subsingleton M i = {to_fun := (equiv.Pi_subsingleton M i).to_fun, inv_fun := (equiv.Pi_subsingleton M i).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

def add_equiv.Pi_subsingleton {ι : Type u_1} (M : ι → Type u_2) [Π (j : ι), has_add (M j)] [subsingleton ι] (i : ι) :

(Π (j : ι), M j) ≃+ M i

A family indexed by a nonempty subsingleton type is equivalent to the element at the single index.

Equations

add_equiv.Pi_subsingleton M i = {to_fun := (equiv.Pi_subsingleton M i).to_fun, inv_fun := (equiv.Pi_subsingleton M i).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

@[simp]

theorem add_equiv.Pi_subsingleton_apply {ι : Type u_1} (M : ι → Type u_2) [Π (j : ι), has_add (M j)] [subsingleton ι] (i : ι) (ᾰ : Π (a' : ι), M a') :

⇑(add_equiv.Pi_subsingleton M i) ᾰ = (equiv.Pi_subsingleton M i).to_fun ᾰ

source

@[simp]

theorem add_equiv.Pi_subsingleton_symm_apply {ι : Type u_1} (M : ι → Type u_2) [Π (j : ι), has_add (M j)] [subsingleton ι] (i : ι) (ᾰ : M i) (a' : ι) :

⇑((add_equiv.Pi_subsingleton M i).symm) ᾰ a' = (equiv.Pi_subsingleton M i).inv_fun ᾰ a'

source

@[protected]

theorem add_equiv.map_neg {G : Type u_10} {H : Type u_11} [add_group G] [add_group H] (h : G ≃+ H) (x : G) :

⇑h (-x) = -⇑h x

An additive equivalence of additive groups preserves negation.

source

@[protected]

theorem mul_equiv.map_inv {G : Type u_10} {H : Type u_11} [group G] [group H] (h : G ≃* H) (x : G) :

⇑h x⁻¹ = (⇑h x)⁻¹

A multiplicative equivalence of groups preserves inversion.

source

@[protected]

theorem add_equiv.map_sub {G : Type u_10} {H : Type u_11} [add_group G] [add_group H] (h : G ≃+ H) (x y : G) :

⇑h (x - y) = ⇑h x - ⇑h y

An additive equivalence of additive groups preserves subtractions.

source

@[protected]

theorem mul_equiv.map_div {G : Type u_10} {H : Type u_11} [group G] [group H] (h : G ≃* H) (x y : G) :

⇑h (x / y) = ⇑h x / ⇑h y

A multiplicative equivalence of groups preserves division.

source

def add_monoid_hom.to_add_equiv {M : Type u_6} {N : Type u_7} [add_zero_class M] [add_zero_class N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = add_monoid_hom.id M) (h₂ : f.comp g = add_monoid_hom.id N) :

M ≃+ N

Given a pair of additive monoid homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an additive equivalence with to_fun = f and inv_fun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for additive monoid homomorphisms.

Equations

f.to_add_equiv g h₁ h₂ = {to_fun := ⇑f, inv_fun := ⇑g, left_inv := _, right_inv := _, map_add' := _}

source

@[simp]

theorem monoid_hom.to_mul_equiv_apply {M : Type u_6} {N : Type u_7} [mul_one_class M] [mul_one_class N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = monoid_hom.id M) (h₂ : f.comp g = monoid_hom.id N) :

⇑(f.to_mul_equiv g h₁ h₂) = ⇑f

source

def monoid_hom.to_mul_equiv {M : Type u_6} {N : Type u_7} [mul_one_class M] [mul_one_class N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = monoid_hom.id M) (h₂ : f.comp g = monoid_hom.id N) :

M ≃* N

Given a pair of monoid homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an multiplicative equivalence with to_fun = f and inv_fun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for monoid homomorphisms.

Equations