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 #
infix ` ≃* `:25 := MulEquiv≃* `:25 := MulEquiv
infix ` ≃+ `:25 := AddEquiv≃+ `:25 := AddEquiv
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.
Equations
- AddHom.inverse f g h₁ h₂ = { toFun := g, map_add' := (_ : ∀ (x y : N), g (x + y) = g x + g y) }
Makes a multiplicative inverse from a bijection which preserves multiplication.
Equations
- MulHom.inverse f g h₁ h₂ = { toFun := g, map_mul' := (_ : ∀ (x y : N), g (x * y) = g x * g y) }
Equations
- One or more equations did not get rendered due to their size.
The inverse of a bijective AddMonoidHom
is an AddMonoidHom
.
Equations
- One or more equations did not get rendered due to their size.
The inverse of a bijective MonoidHom
is a MonoidHom
.
Equations
- One or more equations did not get rendered due to their size.
The proposition that the function preserves addition
map_add' : ∀ (x y : A), Equiv.toFun toEquiv (x + y) = Equiv.toFun toEquiv x + Equiv.toFun toEquiv y
AddEquiv α β
is the type of an equiv α ≃ β≃ β
which preserves addition.
Instances For
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
The AddHom
underlying a AddEquiv
.
Equations
- AddEquiv.toAddHom self = { toFun := self.toEquiv.toFun, map_add' := (_ : ∀ (x y : A), Equiv.toFun self.toEquiv (x + y) = Equiv.toFun self.toEquiv x + Equiv.toFun self.toEquiv y) }
The proposition that the function preserves multiplication
map_mul' : ∀ (x y : M), Equiv.toFun toEquiv (x * y) = Equiv.toFun toEquiv x * Equiv.toFun toEquiv y
MulEquiv α β
is the type of an equiv α ≃ β≃ β
which preserves multiplication.
Instances For
The MulHom
underlying a MulEquiv
.
Equations
- MulEquiv.toMulHom self = { toFun := self.toEquiv.toFun, map_mul' := (_ : ∀ (x y : M), Equiv.toFun self.toEquiv (x * y) = Equiv.toFun self.toEquiv x * Equiv.toFun self.toEquiv y) }
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
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))
Equations
- AddEquivClass.instAddHomClass F = AddHomClass.mk (_ : ∀ (f : F) (a b : M), ↑f (a + b) = ↑f a + ↑f b)
Equations
- (_ : Function.Injective FunLike.coe) = (_ : Function.Injective FunLike.coe)
Equations
- MulEquivClass.instMulHomClass F = MulHomClass.mk (_ : ∀ (f : F) (a b : M), ↑f (a * b) = ↑f a * ↑f b)
Equations
- AddEquivClass.instAddMonoidHomClass F = let src := AddEquivClass.instAddHomClass F; AddMonoidHomClass.mk (_ : ∀ (e : F), ↑e 0 = 0)
Equations
- (_ : Function.Injective FunLike.coe) = (_ : Function.Injective FunLike.coe)
Equations
- MulEquivClass.instMonoidHomClass F = let src := MulEquivClass.instMulHomClass F; MonoidHomClass.mk (_ : ∀ (e : F), ↑e 1 = 1)
Equations
- MulEquivClass.toMonoidWithZeroHomClass F = let src := MulEquivClass.instMonoidHomClass F; MonoidWithZeroHomClass.mk (_ : ∀ (e : F), ↑e 0 = 0)
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Any type satisfying AddEquivClass
can be cast into AddEquiv
via
AddEquivClass.toAddEquiv
.
Equations
- instCoeTCAddEquiv = { coe := AddEquivClass.toAddEquiv }
Any type satisfying MulEquivClass
can be cast into MulEquiv
via
MulEquivClass.toMulEquiv
.
Equations
- instCoeTCMulEquiv = { coe := MulEquivClass.toMulEquiv }
Equations
- AddEquiv.instAddEquivClassAddEquiv = AddEquivClass.mk (_ : ∀ (self : M ≃+ N) (x y : M), Equiv.toFun self.toEquiv (x + y) = Equiv.toFun self.toEquiv x + Equiv.toFun self.toEquiv y)
Equations
- (_ : Function.LeftInverse f.toEquiv.invFun f.toEquiv.toFun) = (_ : Function.LeftInverse f.toEquiv.invFun f.toEquiv.toFun)
Equations
- (_ : Function.RightInverse f.toEquiv.invFun f.toEquiv.toFun) = (_ : Function.RightInverse f.toEquiv.invFun f.toEquiv.toFun)
Equations
- MulEquiv.instMulEquivClassMulEquiv = MulEquivClass.mk (_ : ∀ (self : M ≃* N) (x y : M), Equiv.toFun self.toEquiv (x * y) = Equiv.toFun self.toEquiv x * Equiv.toFun self.toEquiv y)
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddEquiv.instInhabitedAddEquiv = { default := AddEquiv.refl M }
Equations
- MulEquiv.instInhabitedMulEquiv = { default := MulEquiv.refl M }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- One or more equations did not get rendered due to their size.
A bijective Semigroup
homomorphism is an isomorphism
Equations
- One or more equations did not get rendered due to their size.
Extract the forward direction of an additive equivalence as an addition-preserving function.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Extract the forward direction of a multiplicative equivalence as a multiplication-preserving function.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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.
A family of additive equivalences Π j, (Ms j ≃+ Ns 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.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
A family of multiplicative equivalences Π j, (Ms j ≃* Ns 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.
Equations
- (_ : Function.LeftInverse (Equiv.piSubsingleton M i).invFun (Equiv.piSubsingleton M i).toFun) = (_ : Function.LeftInverse (Equiv.piSubsingleton M i).invFun (Equiv.piSubsingleton M i).toFun)
Equations
- (_ : (((i : ι) → M i) + ((i : ι) → M i)) ((i : ι) → M i) instHAdd x x i = x i + x i) = (_ : (((i : ι) → M i) + ((i : ι) → M i)) ((i : ι) → M i) instHAdd x x i = x i + x i)
Equations
- (_ : Function.RightInverse (Equiv.piSubsingleton M i).invFun (Equiv.piSubsingleton M i).toFun) = (_ : Function.RightInverse (Equiv.piSubsingleton M i).invFun (Equiv.piSubsingleton M i).toFun)
A family indexed by a nonempty subsingleton type is equivalent to the element at the single index.
Equations
- One or more equations did not get rendered due to their size.
A family indexed by a nonempty subsingleton type is equivalent to the element at the single index.
Equations
- One or more equations did not get rendered due to their size.
Groups #
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
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (x : N), ↑(AddHom.comp f g) x = ↑(AddHom.id N) x) = (_ : ∀ (x : N), ↑(AddHom.comp f g) x = ↑(AddHom.id N) x)
Equations
- (_ : ∀ (x : M), ↑(AddHom.comp g f) x = ↑(AddHom.id M) x) = (_ : ∀ (x : M), ↑(AddHom.comp g f) x = ↑(AddHom.id M) x)
Given a pair of multiplicative homomorphisms f
, g
such that g.comp f = id
and
f.comp g = id
, returns an 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
- One or more equations did not get rendered due to their size.
Equations
- (_ : ∀ (x : M), ↑(AddMonoidHom.comp g f) x = ↑(AddMonoidHom.id M) x) = (_ : ∀ (x : M), ↑(AddMonoidHom.comp g f) x = ↑(AddMonoidHom.id M) x)
Equations
- (_ : ∀ (x : N), ↑(AddMonoidHom.comp f g) x = ↑(AddMonoidHom.id N) x) = (_ : ∀ (x : N), ↑(AddMonoidHom.comp f g) x = ↑(AddMonoidHom.id N) x)
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
- One or more equations did not get rendered due to their size.
Given a pair of monoid homomorphisms f
, g
such that g.comp f = id
and f.comp g = id
,
returns an 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
- One or more equations did not get rendered due to their size.
Negation on an AddGroup
is a permutation of the underlying type.
Equations
- Equiv.neg G = Function.Involutive.toPerm Neg.neg (_ : Function.Involutive Neg.neg)
Inversion on a Group
or GroupWithZero
is a permutation of the underlying type.
Equations
- Equiv.inv G = Function.Involutive.toPerm Inv.inv (_ : Function.Involutive Inv.inv)