Multiplicative and additive equivs #
In this file we define two extensions of Equiv called AddEquiv and MulEquiv, which are
datatypes representing isomorphisms of AddMonoids/AddGroups and Monoids/Groups.
Notations #
The extended equivs all have coercions to functions, and the coercions are the canonical notation when treating the isomorphisms as maps.
Tags #
Equiv, MulEquiv, AddEquiv
def
ZeroHom.inverse
{M : Type u_6}
{N : Type u_7}
[Zero M]
[Zero N]
(f : ZeroHom M N)
(g : N → M)
(h₁ : Function.LeftInverse g ⇑f)
:
ZeroHom N M
Make a ZeroHom inverse from the bijective inverse of a ZeroHom
Equations
- ZeroHom.inverse f g h₁ = { toFun := g, map_zero' := ⋯ }
theorem
ZeroHom.inverse.proof_1
{M : Type u_1}
{N : Type u_2}
[Zero M]
[Zero N]
(f : ZeroHom M N)
(g : N → M)
(h₁ : Function.LeftInverse g ⇑f)
:
g 0 = 0
@[simp]
theorem
OneHom.inverse_apply
{M : Type u_6}
{N : Type u_7}
[One M]
[One N]
(f : OneHom M N)
(g : N → M)
(h₁ : Function.LeftInverse g ⇑f)
:
∀ (a : N), (OneHom.inverse f g h₁) a = g a
@[simp]
theorem
ZeroHom.inverse_apply
{M : Type u_6}
{N : Type u_7}
[Zero M]
[Zero N]
(f : ZeroHom M N)
(g : N → M)
(h₁ : Function.LeftInverse g ⇑f)
:
∀ (a : N), (ZeroHom.inverse f g h₁) a = g a
def
OneHom.inverse
{M : Type u_6}
{N : Type u_7}
[One M]
[One N]
(f : OneHom M N)
(g : N → M)
(h₁ : Function.LeftInverse g ⇑f)
:
OneHom N M
Makes a OneHom inverse from the bijective inverse of a OneHom
Equations
- OneHom.inverse f g h₁ = { toFun := g, map_one' := ⋯ }
def
AddHom.inverse
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(f : AddHom M N)
(g : N → M)
(h₁ : Function.LeftInverse g ⇑f)
(h₂ : Function.RightInverse g ⇑f)
:
AddHom N M
Makes an additive inverse from a bijection which preserves addition.
Equations
- AddHom.inverse f g h₁ h₂ = { toFun := g, map_add' := ⋯ }
theorem
AddHom.inverse.proof_1
{M : Type u_1}
{N : Type u_2}
[Add M]
[Add N]
(f : AddHom M N)
(g : N → M)
(h₁ : Function.LeftInverse g ⇑f)
(h₂ : Function.RightInverse g ⇑f)
(x : N)
(y : N)
:
@[simp]
theorem
AddHom.inverse_apply
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(f : AddHom M N)
(g : N → M)
(h₁ : Function.LeftInverse g ⇑f)
(h₂ : Function.RightInverse g ⇑f)
:
∀ (a : N), (AddHom.inverse f g h₁ h₂) a = g a
@[simp]
theorem
MulHom.inverse_apply
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(f : M →ₙ* N)
(g : N → M)
(h₁ : Function.LeftInverse g ⇑f)
(h₂ : Function.RightInverse g ⇑f)
:
∀ (a : N), (MulHom.inverse f g h₁ h₂) a = g a
def
MulHom.inverse
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(f : M →ₙ* N)
(g : N → M)
(h₁ : Function.LeftInverse g ⇑f)
(h₂ : Function.RightInverse g ⇑f)
:
N →ₙ* M
Makes a multiplicative inverse from a bijection which preserves multiplication.
Equations
- MulHom.inverse f g h₁ h₂ = { toFun := g, map_mul' := ⋯ }
theorem
AddMonoidHom.inverse.proof_3
{A : Type u_1}
{B : Type u_2}
[AddMonoid A]
[AddMonoid B]
(f : A →+ B)
(g : B → A)
(h₁ : Function.LeftInverse g ⇑f)
:
(ZeroHom.inverse (↑f) g h₁).toFun 0 = 0
theorem
AddMonoidHom.inverse.proof_4
{A : Type u_1}
{B : Type u_2}
[AddMonoid A]
[AddMonoid B]
(f : A →+ B)
(g : B → A)
(h₁ : Function.LeftInverse g ⇑f)
(h₂ : Function.RightInverse g ⇑f)
(x : B)
(y : B)
:
(AddHom.inverse (↑f) g h₁ h₂).toFun (x + y) = (AddHom.inverse (↑f) g h₁ h₂).toFun x + (AddHom.inverse (↑f) g h₁ h₂).toFun y
theorem
AddMonoidHom.inverse.proof_1
{A : Type u_2}
{B : Type u_1}
[AddMonoid A]
[AddMonoid B]
:
ZeroHomClass (A →+ B) A B
def
AddMonoidHom.inverse
{A : Type u_12}
{B : Type u_13}
[AddMonoid A]
[AddMonoid B]
(f : A →+ B)
(g : B → A)
(h₁ : Function.LeftInverse g ⇑f)
(h₂ : Function.RightInverse g ⇑f)
:
B →+ A
The inverse of a bijective AddMonoidHom is an AddMonoidHom.
Equations
- AddMonoidHom.inverse f g h₁ h₂ = let __src := ZeroHom.inverse (↑f) g h₁; let __src := AddHom.inverse (↑f) g h₁ h₂; { toZeroHom := { toFun := g, map_zero' := ⋯ }, map_add' := ⋯ }
theorem
AddMonoidHom.inverse.proof_2
{A : Type u_2}
{B : Type u_1}
[AddMonoid A]
[AddMonoid B]
:
AddHomClass (A →+ B) A B
@[simp]
theorem
AddMonoidHom.inverse_apply
{A : Type u_12}
{B : Type u_13}
[AddMonoid A]
[AddMonoid B]
(f : A →+ B)
(g : B → A)
(h₁ : Function.LeftInverse g ⇑f)
(h₂ : Function.RightInverse g ⇑f)
:
∀ (a : B), (AddMonoidHom.inverse f g h₁ h₂) a = g a
@[simp]
theorem
MonoidHom.inverse_apply
{A : Type u_12}
{B : Type u_13}
[Monoid A]
[Monoid B]
(f : A →* B)
(g : B → A)
(h₁ : Function.LeftInverse g ⇑f)
(h₂ : Function.RightInverse g ⇑f)
:
∀ (a : B), (MonoidHom.inverse f g h₁ h₂) a = g a
def
MonoidHom.inverse
{A : Type u_12}
{B : Type u_13}
[Monoid A]
[Monoid B]
(f : A →* B)
(g : B → A)
(h₁ : Function.LeftInverse g ⇑f)
(h₂ : Function.RightInverse g ⇑f)
:
B →* A
The inverse of a bijective MonoidHom is a MonoidHom.
Equations
- MonoidHom.inverse f g h₁ h₂ = let __src := OneHom.inverse (↑f) g h₁; let __src := MulHom.inverse (↑f) g h₁ h₂; { toOneHom := { toFun := g, map_one' := ⋯ }, map_mul' := ⋯ }
structure
AddEquiv
(A : Type u_12)
(B : Type u_13)
[Add A]
[Add B]
extends
Equiv
:
Type (max u_12 u_13)
AddEquiv α β is the type of an equiv α ≃ β which preserves addition.
- toFun : A → B
- invFun : B → A
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
The proposition that the function preserves addition
structure
MulEquiv
(M : Type u_12)
(N : Type u_13)
[Mul M]
[Mul N]
extends
Equiv
:
Type (max u_12 u_13)
MulEquiv α β is the type of an equiv α ≃ β which preserves multiplication.
- toFun : M → N
- invFun : N → M
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
The proposition that the function preserves multiplication
Notation for a MulEquiv.
Equations
- «term_≃*_» = Lean.ParserDescr.trailingNode `term_≃*_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃* ") (Lean.ParserDescr.cat `term 26))
Notation for an AddEquiv.
Equations
- «term_≃+_» = Lean.ParserDescr.trailingNode `term_≃+_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃+ ") (Lean.ParserDescr.cat `term 26))
instance
AddEquivClass.instAddHomClass
{M : Type u_6}
{N : Type u_7}
(F : Type u_12)
[Add M]
[Add N]
[EquivLike F M N]
[h : AddEquivClass F M N]
:
AddHomClass F M N
Equations
- ⋯ = ⋯
instance
MulEquivClass.instMulHomClass
{M : Type u_6}
{N : Type u_7}
(F : Type u_12)
[Mul M]
[Mul N]
[EquivLike F M N]
[h : MulEquivClass F M N]
:
MulHomClass F M N
Equations
- ⋯ = ⋯
instance
AddEquivClass.instAddMonoidHomClass
(F : Type u_1)
{M : Type u_6}
{N : Type u_7}
[EquivLike F M N]
[AddZeroClass M]
[AddZeroClass N]
[AddEquivClass F M N]
:
AddMonoidHomClass F M N
Equations
- ⋯ = ⋯
instance
MulEquivClass.instMonoidHomClass
(F : Type u_1)
{M : Type u_6}
{N : Type u_7}
[EquivLike F M N]
[MulOneClass M]
[MulOneClass N]
[MulEquivClass F M N]
:
MonoidHomClass F M N
Equations
- ⋯ = ⋯
@[simp]
theorem
AddEquivClass.map_eq_zero_iff
{F : Type u_1}
{M : Type u_12}
{N : Type u_13}
[AddZeroClass M]
[AddZeroClass N]
[EquivLike F M N]
[AddEquivClass F M N]
(h : F)
{x : M}
:
@[simp]
theorem
MulEquivClass.map_eq_one_iff
{F : Type u_1}
{M : Type u_12}
{N : Type u_13}
[MulOneClass M]
[MulOneClass N]
[EquivLike F M N]
[MulEquivClass F M N]
(h : F)
{x : M}
:
theorem
AddEquivClass.map_ne_zero_iff
{F : Type u_1}
{M : Type u_12}
{N : Type u_13}
[AddZeroClass M]
[AddZeroClass N]
[EquivLike F M N]
[AddEquivClass F M N]
(h : F)
{x : M}
:
theorem
MulEquivClass.map_ne_one_iff
{F : Type u_1}
{M : Type u_12}
{N : Type u_13}
[MulOneClass M]
[MulOneClass N]
[EquivLike F M N]
[MulEquivClass F M N]
(h : F)
{x : M}
:
def
AddEquivClass.toAddEquiv
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[EquivLike F α β]
[Add α]
[Add β]
[AddEquivClass F α β]
(f : F)
:
α ≃+ β
Turn an element of a type F satisfying AddEquivClass F α β into an actual
AddEquiv. This is declared as the default coercion from F to α ≃+ β.
Equations
- ↑f = let __src := ↑f; let __src_1 := ↑f; { toEquiv := __src, map_add' := ⋯ }
def
MulEquivClass.toMulEquiv
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[EquivLike F α β]
[Mul α]
[Mul β]
[MulEquivClass F α β]
(f : F)
:
α ≃* β
Turn an element of a type F satisfying MulEquivClass F α β into an actual
MulEquiv. This is declared as the default coercion from F to α ≃* β.
Equations
- ↑f = let __src := ↑f; let __src_1 := ↑f; { toEquiv := __src, map_mul' := ⋯ }
instance
instCoeTCAddEquiv
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[EquivLike F α β]
[Add α]
[Add β]
[AddEquivClass F α β]
:
Any type satisfying AddEquivClass can be cast into AddEquiv via
AddEquivClass.toAddEquiv.
Equations
- instCoeTCAddEquiv = { coe := AddEquivClass.toAddEquiv }
instance
instCoeTCMulEquiv
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[EquivLike F α β]
[Mul α]
[Mul β]
[MulEquivClass F α β]
:
Any type satisfying MulEquivClass can be cast into MulEquiv via
MulEquivClass.toMulEquiv.
Equations
- instCoeTCMulEquiv = { coe := 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
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
AddEquiv.instEquivLikeAddEquiv.proof_2
{M : Type u_2}
{N : Type u_1}
[Add M]
[Add N]
(f : M ≃+ N)
:
Function.RightInverse f.invFun f.toFun
theorem
AddEquiv.instEquivLikeAddEquiv.proof_1
{M : Type u_2}
{N : Type u_1}
[Add M]
[Add N]
(f : M ≃+ N)
:
Function.LeftInverse f.invFun f.toFun
instance
AddEquiv.instAddEquivClassAddEquivInstEquivLikeAddEquiv
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
:
AddEquivClass (M ≃+ N) M N
Equations
- ⋯ = ⋯
instance
MulEquiv.instMulEquivClassMulEquivInstEquivLikeMulEquiv
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
:
MulEquivClass (M ≃* N) M N
Equations
- ⋯ = ⋯
@[simp]
theorem
AddEquiv.toAddHom_eq_coe
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(f : M ≃+ N)
:
AddEquiv.toAddHom f = ↑f
@[simp]
theorem
MulEquiv.toMulHom_eq_coe
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(f : M ≃* N)
:
MulEquiv.toMulHom f = ↑f
@[simp]
theorem
AddEquiv.coe_toAddHom
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
{f : M ≃+ N}
:
⇑(AddEquiv.toAddHom f) = ⇑f
@[simp]
theorem
MulEquiv.coe_toMulHom
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
{f : M ≃* N}
:
⇑(MulEquiv.toMulHom f) = ⇑f
The identity map is an additive isomorphism.
Equations
- AddEquiv.refl M = let __src := Equiv.refl M; { toEquiv := __src, map_add' := ⋯ }
theorem
AddEquiv.refl.proof_1
(M : Type u_1)
[Add M]
:
∀ (x x_1 : M), (Equiv.refl M).toFun (x + x_1) = (Equiv.refl M).toFun (x + x_1)
The identity map is a multiplicative isomorphism.
Equations
- MulEquiv.refl M = let __src := Equiv.refl M; { toEquiv := __src, map_mul' := ⋯ }
Equations
- AddEquiv.instInhabitedAddEquiv = { default := AddEquiv.refl M }
Equations
- MulEquiv.instInhabitedMulEquiv = { default := MulEquiv.refl M }
The inverse of an isomorphism is an isomorphism.
Equations
- AddEquiv.symm h = { toEquiv := h.symm, map_add' := ⋯ }
The inverse of an isomorphism is an isomorphism.
Equations
- MulEquiv.symm h = { toEquiv := h.symm, map_mul' := ⋯ }
theorem
AddEquiv.invFun_eq_symm
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
{f : M ≃+ N}
:
f.invFun = ⇑(AddEquiv.symm f)
theorem
MulEquiv.invFun_eq_symm
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
{f : M ≃* N}
:
f.invFun = ⇑(MulEquiv.symm f)
@[simp]
theorem
AddEquiv.coe_toEquiv_symm
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(f : M ≃+ N)
:
⇑(↑f).symm = ⇑(AddEquiv.symm f)
@[simp]
theorem
MulEquiv.coe_toEquiv_symm
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(f : M ≃* N)
:
⇑(↑f).symm = ⇑(MulEquiv.symm f)
@[simp]
theorem
AddEquiv.equivLike_neg_eq_symm
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(f : M ≃+ N)
:
EquivLike.inv f = ⇑(AddEquiv.symm f)
@[simp]
theorem
MulEquiv.equivLike_inv_eq_symm
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(f : M ≃* N)
:
EquivLike.inv f = ⇑(MulEquiv.symm f)
See Note [custom simps projection]
Equations
See Note [custom simps projection]
Equations
@[simp]
theorem
AddEquiv.toEquiv_symm
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(f : M ≃+ N)
:
↑(AddEquiv.symm f) = (↑f).symm
@[simp]
theorem
MulEquiv.toEquiv_symm
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(f : M ≃* N)
:
↑(MulEquiv.symm f) = (↑f).symm
@[simp]
theorem
AddEquiv.symm_symm
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(f : M ≃+ N)
:
AddEquiv.symm (AddEquiv.symm f) = f
@[simp]
theorem
MulEquiv.symm_symm
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(f : M ≃* N)
:
MulEquiv.symm (MulEquiv.symm f) = f
theorem
AddEquiv.symm_bijective
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
:
Function.Bijective AddEquiv.symm
theorem
MulEquiv.symm_bijective
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
:
Function.Bijective MulEquiv.symm
@[simp]
@[simp]
@[simp]
theorem
AddEquiv.symm_comp_self
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(e : M ≃+ N)
:
⇑(AddEquiv.symm e) ∘ ⇑e = id
@[simp]
theorem
MulEquiv.symm_comp_self
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(e : M ≃* N)
:
⇑(MulEquiv.symm e) ∘ ⇑e = id
@[simp]
theorem
AddEquiv.self_comp_symm
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(e : M ≃+ N)
:
⇑e ∘ ⇑(AddEquiv.symm e) = id
@[simp]
theorem
MulEquiv.self_comp_symm
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(e : M ≃* N)
:
⇑e ∘ ⇑(MulEquiv.symm e) = id
@[simp]
theorem
AddEquiv.symm_trans_apply
{M : Type u_6}
{N : Type u_7}
{P : Type u_8}
[Add M]
[Add N]
[Add P]
(e₁ : M ≃+ N)
(e₂ : N ≃+ P)
(p : P)
:
(AddEquiv.symm (AddEquiv.trans e₁ e₂)) p = (AddEquiv.symm e₁) ((AddEquiv.symm e₂) p)
@[simp]
theorem
MulEquiv.symm_trans_apply
{M : Type u_6}
{N : Type u_7}
{P : Type u_8}
[Mul M]
[Mul N]
[Mul P]
(e₁ : M ≃* N)
(e₂ : N ≃* P)
(p : P)
:
(MulEquiv.symm (MulEquiv.trans e₁ e₂)) p = (MulEquiv.symm e₁) ((MulEquiv.symm e₂) p)
@[simp]
theorem
AddEquiv.symm_trans_self
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(e : M ≃+ N)
:
AddEquiv.trans (AddEquiv.symm e) e = AddEquiv.refl N
@[simp]
theorem
MulEquiv.symm_trans_self
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(e : M ≃* N)
:
MulEquiv.trans (MulEquiv.symm e) e = MulEquiv.refl N
@[simp]
theorem
AddEquiv.self_trans_symm
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(e : M ≃+ N)
:
AddEquiv.trans e (AddEquiv.symm e) = AddEquiv.refl M
@[simp]
theorem
MulEquiv.self_trans_symm
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(e : M ≃* N)
:
MulEquiv.trans e (MulEquiv.symm e) = MulEquiv.refl M
@[simp]
theorem
AddEquiv.mk_coe
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(e : M ≃+ N)
(e' : N → M)
(h₁ : Function.LeftInverse e' ⇑e)
(h₂ : Function.RightInverse e' ⇑e)
(h₃ : ∀ (x y : M),
{ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y)
:
{ toEquiv := { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }, map_add' := h₃ } = e
@[simp]
theorem
MulEquiv.mk_coe
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(e : M ≃* N)
(e' : N → M)
(h₁ : Function.LeftInverse e' ⇑e)
(h₂ : Function.RightInverse e' ⇑e)
(h₃ : ∀ (x y : M),
{ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y)
:
{ toEquiv := { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃ } = e
@[simp]
theorem
AddEquiv.mk_coe'
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(e : M ≃+ N)
(f : N → M)
(h₁ : Function.LeftInverse (⇑e) f)
(h₂ : Function.RightInverse (⇑e) f)
(h₃ : ∀ (x y : N),
{ toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y)
:
{ toEquiv := { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }, map_add' := h₃ } = AddEquiv.symm e
@[simp]
theorem
MulEquiv.mk_coe'
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(e : M ≃* N)
(f : N → M)
(h₁ : Function.LeftInverse (⇑e) f)
(h₂ : Function.RightInverse (⇑e) f)
(h₃ : ∀ (x y : N),
{ toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y)
:
{ toEquiv := { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃ } = MulEquiv.symm e
theorem
AddEquiv.addEquivOfUnique.proof_1
{M : Type u_2}
{N : Type u_1}
[Unique M]
[Unique N]
[Add M]
[Add N]
:
∀ (x x_1 : M),
(Equiv.equivOfUnique M N).toFun (x + x_1) = (Equiv.equivOfUnique M N).toFun x + (Equiv.equivOfUnique M N).toFun x_1
instance
AddEquiv.instUniqueAddEquiv
{M : Type u_12}
{N : Type u_13}
[Unique M]
[Unique N]
[Add M]
[Add N]
:
There is a unique additive monoid homomorphism between two additive monoids with a unique element.
Equations
- AddEquiv.instUniqueAddEquiv = { toInhabited := { default := AddEquiv.addEquivOfUnique }, uniq := ⋯ }
Monoids #
theorem
AddEquiv.coe_addMonoidHom_refl
{M : Type u_6}
[AddZeroClass M]
:
↑(AddEquiv.refl M) = AddMonoidHom.id M
theorem
MulEquiv.coe_monoidHom_refl
{M : Type u_6}
[MulOneClass M]
:
↑(MulEquiv.refl M) = MonoidHom.id M
theorem
AddEquiv.coe_addMonoidHom_trans
{M : Type u_6}
{N : Type u_7}
{P : Type u_8}
[AddZeroClass M]
[AddZeroClass N]
[AddZeroClass P]
(e₁ : M ≃+ N)
(e₂ : N ≃+ P)
:
↑(AddEquiv.trans e₁ e₂) = AddMonoidHom.comp ↑e₂ ↑e₁
theorem
MulEquiv.coe_monoidHom_trans
{M : Type u_6}
{N : Type u_7}
{P : Type u_8}
[MulOneClass M]
[MulOneClass N]
[MulOneClass P]
(e₁ : M ≃* N)
(e₂ : N ≃* P)
:
↑(MulEquiv.trans e₁ e₂) = MonoidHom.comp ↑e₂ ↑e₁
@[simp]
theorem
AddEquiv.coe_addMonoidHom_comp_coe_addMonoidHom_symm
{M : Type u_6}
{N : Type u_7}
[AddZeroClass M]
[AddZeroClass N]
(e : M ≃+ N)
:
AddMonoidHom.comp ↑e ↑(AddEquiv.symm e) = AddMonoidHom.id N
@[simp]
theorem
MulEquiv.coe_monoidHom_comp_coe_monoidHom_symm
{M : Type u_6}
{N : Type u_7}
[MulOneClass M]
[MulOneClass N]
(e : M ≃* N)
:
MonoidHom.comp ↑e ↑(MulEquiv.symm e) = MonoidHom.id N
@[simp]
theorem
AddEquiv.coe_addMonoidHom_symm_comp_coe_addMonoidHom
{M : Type u_6}
{N : Type u_7}
[AddZeroClass M]
[AddZeroClass N]
(e : M ≃+ N)
:
AddMonoidHom.comp ↑(AddEquiv.symm e) ↑e = AddMonoidHom.id M
@[simp]
theorem
MulEquiv.coe_monoidHom_symm_comp_coe_monoidHom
{M : Type u_6}
{N : Type u_7}
[MulOneClass M]
[MulOneClass N]
(e : M ≃* N)
:
MonoidHom.comp ↑(MulEquiv.symm e) ↑e = MonoidHom.id M
theorem
AddEquiv.comp_left_injective
{M : Type u_6}
{N : Type u_7}
{P : Type u_8}
[AddZeroClass M]
[AddZeroClass N]
[AddZeroClass P]
(e : M ≃+ N)
:
Function.Injective fun (f : N →+ P) => AddMonoidHom.comp f ↑e
theorem
MulEquiv.comp_left_injective
{M : Type u_6}
{N : Type u_7}
{P : Type u_8}
[MulOneClass M]
[MulOneClass N]
[MulOneClass P]
(e : M ≃* N)
:
Function.Injective fun (f : N →* P) => MonoidHom.comp f ↑e
theorem
AddEquiv.comp_right_injective
{M : Type u_6}
{N : Type u_7}
{P : Type u_8}
[AddZeroClass M]
[AddZeroClass N]
[AddZeroClass P]
(e : M ≃+ N)
:
Function.Injective fun (f : P →+ M) => AddMonoidHom.comp (↑e) f
theorem
MulEquiv.comp_right_injective
{M : Type u_6}
{N : Type u_7}
{P : Type u_8}
[MulOneClass M]
[MulOneClass N]
[MulOneClass P]
(e : M ≃* N)
:
Function.Injective fun (f : P →* M) => MonoidHom.comp (↑e) f
theorem
AddEquiv.map_zero
{M : Type u_6}
{N : Type u_7}
[AddZeroClass M]
[AddZeroClass N]
(h : M ≃+ N)
:
h 0 = 0
An additive isomorphism of additive monoids sends 0 to 0
(and is hence an additive monoid isomorphism).
theorem
MulEquiv.map_one
{M : Type u_6}
{N : Type u_7}
[MulOneClass M]
[MulOneClass N]
(h : M ≃* N)
:
h 1 = 1
A multiplicative isomorphism of monoids sends 1 to 1 (and is hence a monoid isomorphism).
theorem
AddEquiv.map_eq_zero_iff
{M : Type u_6}
{N : Type u_7}
[AddZeroClass M]
[AddZeroClass N]
(h : M ≃+ N)
{x : M}
:
theorem
MulEquiv.map_eq_one_iff
{M : Type u_6}
{N : Type u_7}
[MulOneClass M]
[MulOneClass N]
(h : M ≃* N)
{x : M}
:
theorem
AddEquiv.map_ne_zero_iff
{M : Type u_6}
{N : Type u_7}
[AddZeroClass M]
[AddZeroClass N]
(h : M ≃+ N)
{x : M}
:
theorem
MulEquiv.map_ne_one_iff
{M : Type u_6}
{N : Type u_7}
[MulOneClass M]
[MulOneClass N]
(h : M ≃* N)
{x : M}
:
noncomputable def
AddEquiv.ofBijective
{M : Type u_12}
{N : Type u_13}
{F : Type u_14}
[Add M]
[Add N]
[FunLike F M N]
[AddHomClass F M N]
(f : F)
(hf : Function.Bijective ⇑f)
:
M ≃+ N
A bijective AddSemigroup homomorphism is an isomorphism
Equations
- AddEquiv.ofBijective f hf = let __src := Equiv.ofBijective (⇑f) hf; { toEquiv := __src, map_add' := ⋯ }
@[simp]
theorem
MulEquiv.ofBijective_apply
{M : Type u_12}
{N : Type u_13}
{F : Type u_14}
[Mul M]
[Mul N]
[FunLike F M N]
[MulHomClass F M N]
(f : F)
(hf : Function.Bijective ⇑f)
(a : M)
:
(MulEquiv.ofBijective f hf) a = f a
@[simp]
theorem
AddEquiv.ofBijective_apply
{M : Type u_12}
{N : Type u_13}
{F : Type u_14}
[Add M]
[Add N]
[FunLike F M N]
[AddHomClass F M N]
(f : F)
(hf : Function.Bijective ⇑f)
(a : M)
:
(AddEquiv.ofBijective f hf) a = f a
noncomputable def
MulEquiv.ofBijective
{M : Type u_12}
{N : Type u_13}
{F : Type u_14}
[Mul M]
[Mul N]
[FunLike F M N]
[MulHomClass F M N]
(f : F)
(hf : Function.Bijective ⇑f)
:
M ≃* N
A bijective Semigroup homomorphism is an isomorphism
Equations
- MulEquiv.ofBijective f hf = let __src := Equiv.ofBijective (⇑f) hf; { toEquiv := __src, map_mul' := ⋯ }
@[simp]
theorem
AddEquiv.ofBijective_apply_symm_apply
{M : Type u_6}
{N : Type u_7}
[AddZeroClass M]
[AddZeroClass N]
{n : N}
(f : M →+ N)
(hf : Function.Bijective ⇑f)
:
f ((AddEquiv.symm (AddEquiv.ofBijective f hf)) n) = n
@[simp]
theorem
MulEquiv.ofBijective_apply_symm_apply
{M : Type u_6}
{N : Type u_7}
[MulOneClass M]
[MulOneClass N]
{n : N}
(f : M →* N)
(hf : Function.Bijective ⇑f)
:
f ((MulEquiv.symm (MulEquiv.ofBijective f hf)) n) = n
def
AddEquiv.toAddMonoidHom
{M : Type u_6}
{N : Type u_7}
[AddZeroClass M]
[AddZeroClass N]
(h : M ≃+ N)
:
M →+ N
Extract the forward direction of an additive equivalence as an addition-preserving function.
Equations
- AddEquiv.toAddMonoidHom h = { toZeroHom := { toFun := h.toFun, map_zero' := ⋯ }, map_add' := ⋯ }
theorem
AddEquiv.toAddMonoidHom.proof_1
{M : Type u_2}
{N : Type u_1}
[AddZeroClass M]
[AddZeroClass N]
(h : M ≃+ N)
(x : M)
(y : M)
:
def
MulEquiv.toMonoidHom
{M : Type u_6}
{N : Type u_7}
[MulOneClass M]
[MulOneClass N]
(h : M ≃* N)
:
M →* N
Extract the forward direction of a multiplicative equivalence as a multiplication-preserving function.
Equations
- MulEquiv.toMonoidHom h = { toOneHom := { toFun := h.toFun, map_one' := ⋯ }, map_mul' := ⋯ }
@[simp]
theorem
AddEquiv.coe_toAddMonoidHom
{M : Type u_6}
{N : Type u_7}
[AddZeroClass M]
[AddZeroClass N]
(e : M ≃+ N)
:
⇑(AddEquiv.toAddMonoidHom e) = ⇑e
@[simp]
theorem
MulEquiv.coe_toMonoidHom
{M : Type u_6}
{N : Type u_7}
[MulOneClass M]
[MulOneClass N]
(e : M ≃* N)
:
⇑(MulEquiv.toMonoidHom e) = ⇑e
theorem
AddEquiv.toAddMonoidHom_injective
{M : Type u_6}
{N : Type u_7}
[AddZeroClass M]
[AddZeroClass N]
:
Function.Injective AddEquiv.toAddMonoidHom
theorem
MulEquiv.toMonoidHom_injective
{M : Type u_6}
{N : Type u_7}
[MulOneClass M]
[MulOneClass N]
:
Function.Injective MulEquiv.toMonoidHom
theorem
AddEquiv.arrowCongr.proof_3
{M : Type u_3}
{N : Type u_1}
{P : Type u_4}
{Q : Type u_2}
[Add P]
[Add Q]
(f : M ≃ N)
(g : P ≃+ Q)
(h : M → P)
(k : M → P)
:
{ toFun := fun (h : M → P) (n : N) => g (h (f.symm n)),
invFun := fun (k : N → Q) (m : M) => (AddEquiv.symm g) (k (f m)), left_inv := ⋯, right_inv := ⋯ }.toFun
(h + k) = { toFun := fun (h : M → P) (n : N) => g (h (f.symm n)),
invFun := fun (k : N → Q) (m : M) => (AddEquiv.symm g) (k (f m)), left_inv := ⋯, right_inv := ⋯ }.toFun
h + { toFun := fun (h : M → P) (n : N) => g (h (f.symm n)),
invFun := fun (k : N → Q) (m : M) => (AddEquiv.symm g) (k (f m)), left_inv := ⋯, right_inv := ⋯ }.toFun
k
def
AddEquiv.arrowCongr
{M : Type u_12}
{N : Type u_13}
{P : Type u_14}
{Q : Type u_15}
[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
- One or more equations did not get rendered due to their size.
def
MulEquiv.arrowCongr
{M : Type u_12}
{N : Type u_13}
{P : Type u_14}
{Q : Type u_15}
[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
- One or more equations did not get rendered due to their size.
theorem
AddEquiv.addMonoidHomCongr.proof_2
{M : Type u_4}
{N : Type u_2}
{P : Type u_3}
{Q : Type u_1}
[AddZeroClass M]
[AddZeroClass N]
[AddCommMonoid P]
[AddCommMonoid Q]
(f : M ≃+ N)
(g : P ≃+ Q)
(k : N →+ Q)
:
(fun (h : M →+ P) =>
AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))))
((fun (k : N →+ Q) =>
AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)))
k) = k
def
AddEquiv.addMonoidHomCongr
{M : Type u_12}
{N : Type u_13}
{P : Type u_14}
{Q : Type u_15}
[AddZeroClass M]
[AddZeroClass N]
[AddCommMonoid P]
[AddCommMonoid Q]
(f : M ≃+ N)
(g : P ≃+ 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.
theorem
AddEquiv.addMonoidHomCongr.proof_3
{M : Type u_2}
{N : Type u_3}
{P : Type u_1}
{Q : Type u_4}
[AddZeroClass M]
[AddZeroClass N]
[AddCommMonoid P]
[AddCommMonoid Q]
(f : M ≃+ N)
(g : P ≃+ Q)
(h : M →+ P)
(k : M →+ P)
:
{
toFun := fun (h : M →+ P) =>
AddMonoidHom.comp (AddEquiv.toAddMonoidHom g)
(AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))),
invFun := fun (k : N →+ Q) =>
AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g))
(AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)),
left_inv := ⋯, right_inv := ⋯ }.toFun
(h + k) = {
toFun := fun (h : M →+ P) =>
AddMonoidHom.comp (AddEquiv.toAddMonoidHom g)
(AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))),
invFun := fun (k : N →+ Q) =>
AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g))
(AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)),
left_inv := ⋯, right_inv := ⋯ }.toFun
h + {
toFun := fun (h : M →+ P) =>
AddMonoidHom.comp (AddEquiv.toAddMonoidHom g)
(AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))),
invFun := fun (k : N →+ Q) =>
AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g))
(AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)),
left_inv := ⋯, right_inv := ⋯ }.toFun
k
theorem
AddEquiv.addMonoidHomCongr.proof_1
{M : Type u_2}
{N : Type u_4}
{P : Type u_1}
{Q : Type u_3}
[AddZeroClass M]
[AddZeroClass N]
[AddCommMonoid P]
[AddCommMonoid Q]
(f : M ≃+ N)
(g : P ≃+ Q)
(h : M →+ P)
:
(fun (k : N →+ Q) =>
AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)))
((fun (h : M →+ P) =>
AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))))
h) = h
@[simp]
theorem
AddEquiv.addMonoidHomCongr_apply
{M : Type u_12}
{N : Type u_13}
{P : Type u_14}
{Q : Type u_15}
[AddZeroClass M]
[AddZeroClass N]
[AddCommMonoid P]
[AddCommMonoid Q]
(f : M ≃+ N)
(g : P ≃+ Q)
(h : M →+ P)
:
@[simp]
theorem
MulEquiv.monoidHomCongr_apply
{M : Type u_12}
{N : Type u_13}
{P : Type u_14}
{Q : Type u_15}
[MulOneClass M]
[MulOneClass N]
[CommMonoid P]
[CommMonoid Q]
(f : M ≃* N)
(g : P ≃* Q)
(h : M →* P)
:
(MulEquiv.monoidHomCongr f g) h = MonoidHom.comp (MulEquiv.toMonoidHom g) (MonoidHom.comp h (MulEquiv.toMonoidHom (MulEquiv.symm f)))
def
MulEquiv.monoidHomCongr
{M : Type u_12}
{N : Type u_13}
{P : Type u_14}
{Q : Type u_15}
[MulOneClass M]
[MulOneClass N]
[CommMonoid P]
[CommMonoid Q]
(f : M ≃* N)
(g : P ≃* 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.piCongrRight
{η : Type u_12}
{Ms : η → Type u_13}
{Ns : η → Type u_14}
[(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.
theorem
AddEquiv.piCongrRight.proof_1
{η : Type u_1}
{Ms : η → Type u_2}
{Ns : η → Type u_3}
[(j : η) → Add (Ms j)]
[(j : η) → Add (Ns j)]
(es : (j : η) → Ms j ≃+ Ns j)
:
Function.LeftInverse (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).invFun
(Equiv.piCongrRight fun (j : η) => (es j).toEquiv).toFun
theorem
AddEquiv.piCongrRight.proof_2
{η : Type u_1}
{Ms : η → Type u_2}
{Ns : η → Type u_3}
[(j : η) → Add (Ms j)]
[(j : η) → Add (Ns j)]
(es : (j : η) → Ms j ≃+ Ns j)
:
Function.RightInverse (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).invFun
(Equiv.piCongrRight fun (j : η) => (es j).toEquiv).toFun
theorem
AddEquiv.piCongrRight.proof_3
{η : Type u_1}
{Ms : η → Type u_3}
{Ns : η → Type u_2}
[(j : η) → Add (Ms j)]
[(j : η) → Add (Ns j)]
(es : (j : η) → Ms j ≃+ Ns j)
(x : (j : η) → Ms j)
(y : (j : η) → Ms j)
:
{ toFun := fun (x : (j : η) → Ms j) (j : η) => (es j) (x j),
invFun := fun (x : (j : η) → Ns j) (j : η) => (AddEquiv.symm (es j)) (x j), left_inv := ⋯,
right_inv := ⋯ }.toFun
(x + y) = { toFun := fun (x : (j : η) → Ms j) (j : η) => (es j) (x j),
invFun := fun (x : (j : η) → Ns j) (j : η) => (AddEquiv.symm (es j)) (x j), left_inv := ⋯,
right_inv := ⋯ }.toFun
x + { toFun := fun (x : (j : η) → Ms j) (j : η) => (es j) (x j),
invFun := fun (x : (j : η) → Ns j) (j : η) => (AddEquiv.symm (es j)) (x j), left_inv := ⋯,
right_inv := ⋯ }.toFun
y
@[simp]
theorem
AddEquiv.piCongrRight_apply
{η : Type u_12}
{Ms : η → Type u_13}
{Ns : η → Type u_14}
[(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_12}
{Ms : η → Type u_13}
{Ns : η → Type u_14}
[(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)
def
MulEquiv.piCongrRight
{η : Type u_12}
{Ms : η → Type u_13}
{Ns : η → Type u_14}
[(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.
@[simp]
theorem
AddEquiv.piCongrRight_refl
{η : Type u_12}
{Ms : η → Type u_13}
[(j : η) → Add (Ms j)]
:
(AddEquiv.piCongrRight fun (j : η) => AddEquiv.refl (Ms j)) = AddEquiv.refl ((j : η) → Ms j)
@[simp]
theorem
MulEquiv.piCongrRight_refl
{η : Type u_12}
{Ms : η → Type u_13}
[(j : η) → Mul (Ms j)]
:
(MulEquiv.piCongrRight fun (j : η) => MulEquiv.refl (Ms j)) = MulEquiv.refl ((j : η) → Ms j)
@[simp]
theorem
AddEquiv.piCongrRight_symm
{η : Type u_12}
{Ms : η → Type u_13}
{Ns : η → Type u_14}
[(j : η) → Add (Ms j)]
[(j : η) → Add (Ns j)]
(es : (j : η) → Ms j ≃+ Ns j)
:
AddEquiv.symm (AddEquiv.piCongrRight es) = AddEquiv.piCongrRight fun (i : η) => AddEquiv.symm (es i)
@[simp]
theorem
MulEquiv.piCongrRight_symm
{η : Type u_12}
{Ms : η → Type u_13}
{Ns : η → Type u_14}
[(j : η) → Mul (Ms j)]
[(j : η) → Mul (Ns j)]
(es : (j : η) → Ms j ≃* Ns j)
:
MulEquiv.symm (MulEquiv.piCongrRight es) = MulEquiv.piCongrRight fun (i : η) => MulEquiv.symm (es i)
@[simp]
theorem
AddEquiv.piCongrRight_trans
{η : Type u_12}
{Ms : η → Type u_13}
{Ns : η → Type u_14}
{Ps : η → Type u_15}
[(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.trans (AddEquiv.piCongrRight es) (AddEquiv.piCongrRight fs) = AddEquiv.piCongrRight fun (i : η) => AddEquiv.trans (es i) (fs i)
@[simp]
theorem
MulEquiv.piCongrRight_trans
{η : Type u_12}
{Ms : η → Type u_13}
{Ns : η → Type u_14}
{Ps : η → Type u_15}
[(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.trans (MulEquiv.piCongrRight es) (MulEquiv.piCongrRight fs) = MulEquiv.piCongrRight fun (i : η) => MulEquiv.trans (es i) (fs i)
def
AddEquiv.piUnique
{ι : Type u_12}
(M : ι → Type u_13)
[(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 = let __src := Equiv.piUnique M; { toEquiv := __src, map_add' := ⋯ }
@[simp]
theorem
MulEquiv.piUnique_symm_apply
{ι : Type u_12}
(M : ι → Type u_13)
[(j : ι) → Mul (M j)]
[Unique ι]
(x : M default)
(i : ι)
:
(MulEquiv.symm (MulEquiv.piUnique M)) x i = uniqueElim x i
@[simp]
theorem
MulEquiv.piUnique_apply
{ι : Type u_12}
(M : ι → Type u_13)
[(j : ι) → Mul (M j)]
[Unique ι]
(f : (i : ι) → M i)
:
(MulEquiv.piUnique M) f = f default
@[simp]
theorem
AddEquiv.piUnique_symm_apply
{ι : Type u_12}
(M : ι → Type u_13)
[(j : ι) → Add (M j)]
[Unique ι]
(x : M default)
(i : ι)
:
(AddEquiv.symm (AddEquiv.piUnique M)) x i = uniqueElim x i
@[simp]
theorem
AddEquiv.piUnique_apply
{ι : Type u_12}
(M : ι → Type u_13)
[(j : ι) → Add (M j)]
[Unique ι]
(f : (i : ι) → M i)
:
(AddEquiv.piUnique M) f = f default
def
MulEquiv.piUnique
{ι : Type u_12}
(M : ι → Type u_13)
[(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 = let __src := Equiv.piUnique M; { toEquiv := __src, map_mul' := ⋯ }
Groups #
theorem
AddEquiv.map_neg
{G : Type u_10}
{H : Type u_11}
[AddGroup G]
[SubtractionMonoid H]
(h : G ≃+ H)
(x : G)
:
An additive equivalence of additive groups preserves negation.
theorem
MulEquiv.map_inv
{G : Type u_10}
{H : Type u_11}
[Group G]
[DivisionMonoid H]
(h : G ≃* H)
(x : G)
:
A multiplicative equivalence of groups preserves inversion.
theorem
AddEquiv.map_sub
{G : Type u_10}
{H : Type u_11}
[AddGroup G]
[SubtractionMonoid H]
(h : G ≃+ H)
(x : G)
(y : G)
:
An additive equivalence of additive groups preserves subtractions.
theorem
MulEquiv.map_div
{G : Type u_10}
{H : Type u_11}
[Group G]
[DivisionMonoid H]
(h : G ≃* H)
(x : G)
(y : G)
:
A multiplicative equivalence of groups preserves division.
theorem
AddHom.toAddEquiv.proof_2
{M : Type u_2}
{N : Type u_1}
[Add M]
[Add N]
(f : AddHom M N)
(g : AddHom N M)
(h₂ : AddHom.comp f g = AddHom.id N)
(x : N)
:
(AddHom.comp f g) x = (AddHom.id N) x
theorem
AddHom.toAddEquiv.proof_1
{M : Type u_1}
{N : Type u_2}
[Add M]
[Add N]
(f : AddHom M N)
(g : AddHom N M)
(h₁ : AddHom.comp g f = AddHom.id M)
(x : M)
:
(AddHom.comp g f) x = (AddHom.id M) x
def
AddHom.toAddEquiv
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(f : AddHom M N)
(g : AddHom N M)
(h₁ : AddHom.comp g f = AddHom.id M)
(h₂ : AddHom.comp f g = AddHom.id N)
:
M ≃+ N
Given a pair of additive homomorphisms f, g such that g.comp f = id and
f.comp g = id, returns an additive equivalence with toFun = f and invFun = g. This
constructor is useful if the underlying type(s) have specialized ext lemmas for additive
homomorphisms.
Equations
- AddHom.toAddEquiv f g h₁ h₂ = { toEquiv := { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }
def
MulHom.toMulEquiv
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(f : M →ₙ* N)
(g : N →ₙ* M)
(h₁ : MulHom.comp g f = MulHom.id M)
(h₂ : MulHom.comp f g = MulHom.id N)
:
M ≃* N
Given a pair of multiplicative homomorphisms f, g such that g.comp f = id and
f.comp g = id, returns a multiplicative equivalence with toFun = f and invFun = g. This
constructor is useful if the underlying type(s) have specialized ext lemmas for multiplicative
homomorphisms.
Equations
- MulHom.toMulEquiv f g h₁ h₂ = { toEquiv := { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯ }
@[simp]
theorem
AddHom.toAddEquiv_apply
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(f : AddHom M N)
(g : AddHom N M)
(h₁ : AddHom.comp g f = AddHom.id M)
(h₂ : AddHom.comp f g = AddHom.id N)
:
⇑(AddHom.toAddEquiv f g h₁ h₂) = ⇑f
@[simp]
theorem
MulHom.toMulEquiv_apply
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(f : M →ₙ* N)
(g : N →ₙ* M)
(h₁ : MulHom.comp g f = MulHom.id M)
(h₂ : MulHom.comp f g = MulHom.id N)
:
⇑(MulHom.toMulEquiv f g h₁ h₂) = ⇑f
@[simp]
theorem
AddHom.toAddEquiv_symm_apply
{M : Type u_6}
{N : Type u_7}
[Add M]
[Add N]
(f : AddHom M N)
(g : AddHom N M)
(h₁ : AddHom.comp g f = AddHom.id M)
(h₂ : AddHom.comp f g = AddHom.id N)
:
⇑(AddEquiv.symm (AddHom.toAddEquiv f g h₁ h₂)) = ⇑g
@[simp]
theorem
MulHom.toMulEquiv_symm_apply
{M : Type u_6}
{N : Type u_7}
[Mul M]
[Mul N]
(f : M →ₙ* N)
(g : N →ₙ* M)
(h₁ : MulHom.comp g f = MulHom.id M)
(h₂ : MulHom.comp f g = MulHom.id N)
:
⇑(MulEquiv.symm (MulHom.toMulEquiv f g h₁ h₂)) = ⇑g
theorem
AddMonoidHom.toAddEquiv.proof_2
{M : Type u_2}
{N : Type u_1}
[AddZeroClass M]
[AddZeroClass N]
(f : M →+ N)
(g : N →+ M)
(h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N)
(x : N)
:
(AddMonoidHom.comp f g) x = (AddMonoidHom.id N) x
def
AddMonoidHom.toAddEquiv
{M : Type u_6}
{N : Type u_7}
[AddZeroClass M]
[AddZeroClass N]
(f : M →+ N)
(g : N →+ M)
(h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M)
(h₂ : AddMonoidHom.comp f g = AddMonoidHom.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 toFun = f and invFun = g. This
constructor is useful if the underlying type(s) have specialized ext lemmas for additive
monoid homomorphisms.
Equations
- AddMonoidHom.toAddEquiv f g h₁ h₂ = { toEquiv := { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }
theorem
AddMonoidHom.toAddEquiv.proof_1
{M : Type u_1}
{N : Type u_2}
[AddZeroClass M]
[AddZeroClass N]
(f : M →+ N)
(g : N →+ M)
(h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M)
(x : M)
:
(AddMonoidHom.comp g f) x = (AddMonoidHom.id M) x
@[simp]
theorem
MonoidHom.toMulEquiv_symm_apply
{M : Type u_6}
{N : Type u_7}
[MulOneClass M]
[MulOneClass N]
(f : M →* N)
(g : N →* M)
(h₁ : MonoidHom.comp g f = MonoidHom.id M)
(h₂ : MonoidHom.comp f g = MonoidHom.id N)
:
⇑(MulEquiv.symm (MonoidHom.toMulEquiv f g h₁ h₂)) = ⇑g
@[simp]
theorem
AddMonoidHom.toAddEquiv_symm_apply
{M : Type u_6}
{N : Type u_7}
[AddZeroClass M]
[AddZeroClass N]
(f : M →+ N)
(g : N →+ M)
(h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M)
(h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N)
:
⇑(AddEquiv.symm (AddMonoidHom.toAddEquiv f g h₁ h₂)) = ⇑g
@[simp]
theorem
AddMonoidHom.toAddEquiv_apply
{M : Type u_6}
{N : Type u_7}
[AddZeroClass M]
[AddZeroClass N]
(f : M →+ N)
(g : N →+ M)
(h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M)
(h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N)
:
⇑(AddMonoidHom.toAddEquiv f g h₁ h₂) = ⇑f
@[simp]
theorem
MonoidHom.toMulEquiv_apply
{M : Type u_6}
{N : Type u_7}
[MulOneClass M]
[MulOneClass N]
(f : M →* N)
(g : N →* M)
(h₁ : MonoidHom.comp g f = MonoidHom.id M)
(h₂ : MonoidHom.comp f g = MonoidHom.id N)
:
⇑(MonoidHom.toMulEquiv f g h₁ h₂) = ⇑f
def
MonoidHom.toMulEquiv
{M : Type u_6}
{N : Type u_7}
[MulOneClass M]
[MulOneClass N]
(f : M →* N)
(g : N →* M)
(h₁ : MonoidHom.comp g f = MonoidHom.id M)
(h₂ : MonoidHom.comp f g = MonoidHom.id N)
:
M ≃* N
Given a pair of monoid homomorphisms f, g such that g.comp f = id and f.comp g = id,
returns a multiplicative equivalence with toFun = f and invFun = g. This constructor is
useful if the underlying type(s) have specialized ext lemmas for monoid homomorphisms.
Equations
- MonoidHom.toMulEquiv f g h₁ h₂ = { toEquiv := { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯ }
Negation on an AddGroup is a permutation of the underlying type.
Equations
- Equiv.neg G = Function.Involutive.toPerm Neg.neg ⋯
Inversion on a Group or GroupWithZero is a permutation of the underlying type.
Equations
- Equiv.inv G = Function.Involutive.toPerm Inv.inv ⋯
@[simp]
@[simp]