Monoid, group etc structures on M × N× N
#
In this file we define one-binop (Monoid
, Group
etc) structures on M × N× N
. We also prove
trivial simp
lemmas, and define the following operations on MonoidHom
s:
fst M N : M × N →* M× N →* M→* M
,snd M N : M × N →* N× N →* N→* N
: projectionsprod.fst
andprod.snd
asMonoidHom
s;inl M N : M →* M × N→* M × N× N
,inr M N : N →* M × N→* M × N× N
: inclusions of first/second monoid into the product;f.prod g :
M →* N × P: sends
xto
(f x, g x)`;f.coprod g : M × N →* P× N →* P→* P
: sends(x, y)
tof x * g y
;f.prodMap g : M × N → M' × N'× N → M' × N'→ M' × N'× N'
:prod.map f g
as aMonoidHom
, sends(x, y)
to(f x, g y)
.
Main declarations #
mulMulHom
/mulMonoidHom
/mulMonoidWithZeroHom
: Multiplication bundled as a multiplicative/monoid/monoid with zero homomorphism.divMonoidHom
/divMonoidWithZeroHom
: Division bundled as a monoid/monoid with zero homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Prod.instAddMonoidSum = AddMonoid.mk (_ : ∀ (a : M × N), 0 + a = a) (_ : ∀ (a : M × N), a + 0 = a) fun z a => (AddMonoid.nsmul z a.fst, AddMonoid.nsmul z a.snd)
Equations
- (_ : (fun z a => (AddMonoid.nsmul z a.fst, AddMonoid.nsmul z a.snd)) 0 z = 0) = (_ : (fun z a => (AddMonoid.nsmul z a.fst, AddMonoid.nsmul z a.snd)) 0 z = 0)
Equations
- (_ : (fun z a => (SubNegMonoid.zsmul z a.fst, SubNegMonoid.zsmul z a.snd)) 0 x = 0) = (_ : (fun z a => (SubNegMonoid.zsmul z a.fst, SubNegMonoid.zsmul z a.snd)) 0 x = 0)
Equations
- One or more equations did not get rendered due to their size.
Equations
- Prod.subNegMonoid = SubNegMonoid.mk fun z a => (SubNegMonoid.zsmul z a.fst, SubNegMonoid.zsmul z a.snd)
Equations
- One or more equations did not get rendered due to their size.
Equations
- Prod.instDivInvMonoidProd = DivInvMonoid.mk fun z a => (DivInvMonoid.zpow z a.fst, DivInvMonoid.zpow z a.snd)
Equations
- Prod.SubtractionCommMonoid.match_1 motive x h_1 = Prod.casesOn x fun fst snd => h_1 fst snd
Combine two AddMonoidHom
s f : AddHom M N
, g : AddHom M P
into
f.prod g : AddHom M (N × P)× P)
given by (f.prod g) x = (f x, g x)
prod.map
as an AddMonoidHom
Equations
- AddHom.prodMap f g = AddHom.prod (AddHom.comp f (AddHom.fst M N)) (AddHom.comp g (AddHom.snd M N))
Equations
- MulHom.prodMap f g = MulHom.prod (MulHom.comp f (MulHom.fst M N)) (MulHom.comp g (MulHom.snd M N))
Coproduct of two AddHom
s with the same codomain:
f.coprod g (p : M × N) = f p.1 + g p.2× N) = f p.1 + g p.2
.
Equations
- AddHom.coprod f g = AddHom.comp f (AddHom.fst M N) + AddHom.comp g (AddHom.snd M N)
Coproduct of two MulHom
s with the same codomain:
f.coprod g (p : M × N) = f p.1 * g p.2× N) = f p.1 * g p.2
.
Equations
- MulHom.coprod f g = MulHom.comp f (MulHom.fst M N) * MulHom.comp g (MulHom.snd M N)
Given additive monoids A
, B
, the natural projection homomorphism
from A × B× B
to A
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.
Given monoids M
, N
, the natural projection homomorphism from M × N× N
to M
.
Equations
- One or more equations did not get rendered due to their size.
Given additive monoids A
, B
, the natural projection homomorphism
from A × B× B
to B
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.
Given monoids M
, N
, the natural projection homomorphism from M × N× N
to N
.
Equations
- One or more equations did not get rendered due to their size.
Given additive monoids A
, B
, the natural inclusion homomorphism
from A
to A × B× B
.
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.
Given monoids M
, N
, the natural inclusion homomorphism from M
to M × N× N
.
Equations
- One or more equations did not get rendered due to their size.
Given additive monoids A
, B
, the natural inclusion homomorphism
from B
to A × B× B
.
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.
Given monoids M
, N
, the natural inclusion homomorphism from N
to M × N× N
.
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.
Combine two AddMonoidHom
s f : M →+ N→+ N
, g : M →+ P→+ P
into
f.prod g : M →+ N × P→+ N × P× P
given by (f.prod g) x = (f x, g x)
Equations
- One or more equations did not get rendered due to their size.
Combine two MonoidHom
s f : M →* N→* N
, g : M →* P→* P
into f.prod g : M →* N × P→* N × P× P
given by (f.prod g) x = (f x, g x)
.
Equations
- One or more equations did not get rendered due to their size.
prod.map
as an AddHonoidHom
Equations
- AddMonoidHom.prodMap f g = AddMonoidHom.prod (AddMonoidHom.comp f (AddMonoidHom.fst M N)) (AddMonoidHom.comp g (AddMonoidHom.snd M N))
prod.map
as a MonoidHom
.
Equations
- MonoidHom.prodMap f g = MonoidHom.prod (MonoidHom.comp f (MonoidHom.fst M N)) (MonoidHom.comp g (MonoidHom.snd M N))
Coproduct of two AddMonoidHom
s with the same codomain:
f.coprod g (p : M × N) = f p.1 + g p.2× N) = f p.1 + g p.2
.
Equations
- AddMonoidHom.coprod f g = AddMonoidHom.comp f (AddMonoidHom.fst M N) + AddMonoidHom.comp g (AddMonoidHom.snd M N)
Coproduct of two MonoidHom
s with the same codomain:
f.coprod g (p : M × N) = f p.1 * g p.2× N) = f p.1 * g p.2
.
Equations
- MonoidHom.coprod f g = MonoidHom.comp f (MonoidHom.fst M N) * MonoidHom.comp g (MonoidHom.snd M N)
Equations
- (_ : Function.LeftInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun) = (_ : Function.LeftInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun)
The equivalence between M × N× N
and N × M× M
given by swapping the
components 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
- (_ : Function.RightInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun) = (_ : Function.RightInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun)
The equivalence between M × N× N
and N × M× M
given by swapping the components
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.
Product of additive isomorphisms; the maps come from Equiv.prodCongr
.
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.
Product of multiplicative isomorphisms; the maps come from Equiv.prodCongr
.
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.
Multiplying by the trivial monoid doesn't change the structure.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.LeftInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun) = (_ : Function.LeftInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun)
Equations
- (_ : Function.RightInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun) = (_ : Function.RightInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun)
Multiplying by the trivial monoid doesn't change the structure.
Equations
- One or more equations did not get rendered due to their size.
Multiplying by the trivial monoid doesn't change the structure.
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.RightInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun) = (_ : Function.RightInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun)
Equations
- One or more equations did not get rendered due to their size.
Equations
- (_ : Function.LeftInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun) = (_ : Function.LeftInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun)
Multiplying by the trivial monoid doesn't change the structure.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddEquiv.prodAddUnits.match_1 motive x h_1 = Prod.casesOn x fun fst snd => h_1 fst snd
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.
The additive monoid equivalence between additive units of a product of two additive monoids, and the product of the additive units of each 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.
Canonical homomorphism of additive monoids from AddUnits α
into α × αᵃᵒᵖ× αᵃᵒᵖ
.
Used mainly to define the natural topology of AddUnits α
.
Equations
- One or more equations did not get rendered due to their size.
Multiplication and division as homomorphisms #
Addition as an additive monoid homomorphism.
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.
Multiplication as a monoid homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Multiplication as a multiplicative homomorphism with zero.
Equations
- One or more equations did not get rendered due to their size.
Subtraction as an additive monoid homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Division as a monoid homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Division as a multiplicative homomorphism with zero.
Equations
- One or more equations did not get rendered due to their size.