Multiplicative and additive equivs #
In this file we define two extensions of Equiv
called AddEquiv
and MulEquiv
, which are
datatypes representing isomorphisms of AddMonoid
s/AddGroup
s and Monoid
s/Group
s.
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
Makes a multiplicative inverse from a bijection which preserves multiplication.
Equations
- f.inverse g h₁ h₂ = { toFun := g, map_mul' := ⋯ }
Instances For
Makes an additive inverse from a bijection which preserves addition.
Equations
- f.inverse g h₁ h₂ = { toFun := g, map_add' := ⋯ }
Instances For
The inverse of a bijective MonoidHom
is a MonoidHom
.
Equations
- f.inverse g h₁ h₂ = { toFun := g, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The inverse of a bijective AddMonoidHom
is an AddMonoidHom
.
Equations
- f.inverse g h₁ h₂ = { toFun := g, map_zero' := ⋯, map_add' := ⋯ }
Instances For
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
Instances For
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
Instances For
Notation for a MulEquiv
.
Equations
- «term_≃*_» = Lean.ParserDescr.trailingNode `«term_≃*_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃* ") (Lean.ParserDescr.cat `term 26))
Instances For
Notation for an AddEquiv
.
Equations
- «term_≃+_» = Lean.ParserDescr.trailingNode `«term_≃+_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃+ ") (Lean.ParserDescr.cat `term 26))
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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 = { toEquiv := ↑f, map_mul' := ⋯ }
Instances For
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 = { toEquiv := ↑f, map_add' := ⋯ }
Instances For
Any type satisfying MulEquivClass
can be cast into MulEquiv
via
MulEquivClass.toMulEquiv
.
Equations
- instCoeTCMulEquivOfMulEquivClass = { coe := MulEquivClass.toMulEquiv }
Any type satisfying AddEquivClass
can be cast into AddEquiv
via
AddEquivClass.toAddEquiv
.
Equations
- instCoeTCAddEquivOfAddEquivClass = { coe := AddEquivClass.toAddEquiv }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The identity map is a multiplicative isomorphism.
Equations
- MulEquiv.refl M = { toEquiv := Equiv.refl M, map_mul' := ⋯ }
Instances For
The identity map is an additive isomorphism.
Equations
- AddEquiv.refl M = { toEquiv := Equiv.refl M, map_add' := ⋯ }
Instances For
Equations
- MulEquiv.instInhabited = { default := MulEquiv.refl M }
Equations
- AddEquiv.instInhabited = { default := AddEquiv.refl M }
Monoids #
A multiplicative isomorphism of monoids sends 1
to 1
(and is hence a monoid isomorphism).
An additive isomorphism of additive monoids sends 0
to 0
(and is hence an additive monoid isomorphism).
A bijective Semigroup
homomorphism is an isomorphism
Equations
- MulEquiv.ofBijective f hf = { toEquiv := Equiv.ofBijective (⇑f) hf, map_mul' := ⋯ }
Instances For
A bijective AddSemigroup
homomorphism is an isomorphism
Equations
- AddEquiv.ofBijective f hf = { toEquiv := Equiv.ofBijective (⇑f) hf, map_add' := ⋯ }
Instances For
Extract the forward direction of a multiplicative equivalence as a multiplication-preserving function.
Equations
- h.toMonoidHom = { toFun := h.toFun, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Extract the forward direction of an additive equivalence as an addition-preserving function.
Equations
- h.toAddMonoidHom = { toFun := h.toFun, map_zero' := ⋯, map_add' := ⋯ }
Instances For
A multiplicative analogue of Equiv.arrowCongr
,
where the equivalence between the targets is multiplicative.
Equations
- MulEquiv.arrowCongr f g = { toFun := fun (h : M → P) (n : N) => g (h (f.symm n)), invFun := fun (k : N → Q) (m : M) => g.symm (k (f m)), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Instances For
An additive analogue of Equiv.arrowCongr
,
where the equivalence between the targets is additive.
Equations
- AddEquiv.arrowCongr f g = { toFun := fun (h : M → P) (n : N) => g (h (f.symm n)), invFun := fun (k : N → Q) (m : M) => g.symm (k (f m)), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
A family indexed by a type with a unique element
is MulEquiv
to the element at the single index.
Equations
- MulEquiv.piUnique M = { toEquiv := Equiv.piUnique M, map_mul' := ⋯ }
Instances For
A family indexed by a type with a unique element
is AddEquiv
to the element at the single index.
Equations
- AddEquiv.piUnique M = { toEquiv := Equiv.piUnique M, map_add' := ⋯ }
Instances For
Groups #
A multiplicative equivalence of groups preserves inversion.
An additive equivalence of additive groups preserves negation.
A multiplicative equivalence of groups preserves division.
An additive equivalence of additive groups preserves subtractions.
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
- f.toMulEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Instances For
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
- f.toAddEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
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
- f.toMulEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Instances For
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
- f.toAddEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
Inversion on a Group
or GroupWithZero
is a permutation of the underlying type.
Equations
- Equiv.inv G = Function.Involutive.toPerm Inv.inv ⋯
Instances For
Negation on an AddGroup
is a permutation of the underlying type.
Equations
- Equiv.neg G = Function.Involutive.toPerm Neg.neg ⋯