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 an additive inverse from a bijection which preserves addition.
Instances For
Makes a multiplicative inverse from a bijection which preserves multiplication.
Instances For
The inverse of a bijective AddMonoidHom
is an AddMonoidHom
.
Instances For
The inverse of a bijective MonoidHom
is a MonoidHom
.
Instances For
- toFun : A → B
- invFun : B → A
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- map_add' : ∀ (x y : A), Equiv.toFun s.toEquiv (x + y) = Equiv.toFun s.toEquiv x + Equiv.toFun s.toEquiv y
The proposition that the function preserves addition
AddEquiv α β
is the type of an equiv α ≃ β
which preserves addition.
Instances For
- coe : F → A → B
- inv : F → B → A
- left_inv : ∀ (e : F), Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
- right_inv : ∀ (e : F), Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
- coe_injective' : ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
Preserves addition.
AddEquivClass F A B
states that F
is a type of addition-preserving morphisms.
You should extend this class when you extend AddEquiv
.
Instances
- toFun : M → N
- invFun : N → M
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- map_mul' : ∀ (x y : M), Equiv.toFun s.toEquiv (x * y) = Equiv.toFun s.toEquiv x * Equiv.toFun s.toEquiv y
The proposition that the function preserves multiplication
MulEquiv α β
is the type of an equiv α ≃ β
which preserves multiplication.
Instances For
- coe : F → A → B
- inv : F → B → A
- left_inv : ∀ (e : F), Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
- right_inv : ∀ (e : F), Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
- coe_injective' : ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
Preserves multiplication.
MulEquivClass F A B
states that F
is a type of multiplication-preserving morphisms.
You should extend this class when you extend MulEquiv
.
Instances
Turn an element of a type F
satisfying AddEquivClass F α β
into an actual
AddEquiv
. This is declared as the default coercion from F
to α ≃+ β
.
Instances For
Turn an element of a type F
satisfying MulEquivClass F α β
into an actual
MulEquiv
. This is declared as the default coercion from F
to α ≃* β
.
Instances For
Any type satisfying AddEquivClass
can be cast into AddEquiv
via
AddEquivClass.toAddEquiv
.
Any type satisfying MulEquivClass
can be cast into MulEquiv
via
MulEquivClass.toMulEquiv
.
The identity map is an additive isomorphism.
Instances For
The identity map is a multiplicative isomorphism.
Instances For
Monoids #
An additive isomorphism of additive monoids sends 0
to 0
(and is hence an additive monoid isomorphism).
A multiplicative isomorphism of monoids sends 1
to 1
(and is hence a monoid isomorphism).
A bijective AddSemigroup
homomorphism is an isomorphism
Instances For
A bijective Semigroup
homomorphism is an isomorphism
Instances For
Extract the forward direction of an additive equivalence as an addition-preserving function.
Instances For
Extract the forward direction of a multiplicative equivalence as a multiplication-preserving function.
Instances For
An additive analogue of Equiv.arrowCongr
,
for additive maps from an additive monoid to a commutative additive monoid.
Instances For
A multiplicative analogue of Equiv.arrowCongr
,
for multiplicative maps from a monoid to a commutative monoid.
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
.
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
.
Instances For
A family indexed by a nonempty subsingleton type is equivalent to the element at the single index.
Instances For
A family indexed by a nonempty subsingleton type is equivalent to the element at the single index.
Instances For
Groups #
An additive equivalence of additive groups preserves negation.
A multiplicative equivalence of groups preserves inversion.
An additive equivalence of additive groups preserves subtractions.
A multiplicative equivalence of groups preserves division.
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.
Instances For
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.
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.
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.
Instances For
Negation on an AddGroup
is a permutation of the underlying type.
Instances For
Inversion on a Group
or GroupWithZero
is a permutation of the underlying type.