Monoid, group etc structures on M × N
#
In this file we define one-binop (Monoid
, Group
etc) structures on M × N
.
We also prove trivial simp
lemmas, and define the following operations on MonoidHom
s:
fst M N : M × N →* M
,snd M N : M × N →* N
: projectionsProd.fst
andProd.snd
asMonoidHom
s;inl M N : M →* M × N
,inr M N : N →* M × N
: inclusions of first/second monoid into the product;f.prod g
:M →* N × P
: sendsx
to(f x, g x)
;- When
P
is commutative,f.coprod g : M × N →* P
sends(x, y)
tof x * g y
(without the commutativity assumption onP
, seeMonoidHom.noncommPiCoprod
); f.prodMap g : M × N → M' × N'
:prod.map f g
as aMonoidHom
, sends(x, y)
to(f x, g y)
.
Main declarations #
mulMulHom
/mulMonoidHom
: Multiplication bundled as a multiplicative/monoid homomorphism.divMonoidHom
: Division bundled as a monoid homomorphism.
Equations
- Prod.instInvolutiveInv = InvolutiveInv.mk ⋯
Equations
- Prod.instInvolutiveNeg = InvolutiveNeg.mk ⋯
Equations
- Prod.instSemigroup = Semigroup.mk ⋯
Equations
- Prod.instAddSemigroup = AddSemigroup.mk ⋯
Equations
- Prod.instCommSemigroup = CommSemigroup.mk ⋯
Equations
- Prod.instAddCommSemigroup = AddCommSemigroup.mk ⋯
Equations
- Prod.instMulOneClass = MulOneClass.mk ⋯ ⋯
Equations
- Prod.instAddZeroClass = AddZeroClass.mk ⋯ ⋯
Equations
- Prod.instMonoid = Monoid.mk ⋯ ⋯ (fun (z : ℕ) (a : M × N) => (Monoid.npow z a.1, Monoid.npow z a.2)) ⋯ ⋯
Equations
- Prod.instAddMonoid = AddMonoid.mk ⋯ ⋯ (fun (z : ℕ) (a : M × N) => (AddMonoid.nsmul z a.1, AddMonoid.nsmul z a.2)) ⋯ ⋯
Equations
- Prod.instDivInvMonoid = DivInvMonoid.mk ⋯ (fun (z : ℤ) (a : G × H) => (DivInvMonoid.zpow z a.1, DivInvMonoid.zpow z a.2)) ⋯ ⋯ ⋯
Equations
- Prod.subNegMonoid = SubNegMonoid.mk ⋯ (fun (z : ℤ) (a : G × H) => (SubNegMonoid.zsmul z a.1, SubNegMonoid.zsmul z a.2)) ⋯ ⋯ ⋯
Equations
- Prod.instDivisionMonoid = DivisionMonoid.mk ⋯ ⋯ ⋯
Equations
- Prod.instSubtractionMonoid = SubtractionMonoid.mk ⋯ ⋯ ⋯
Equations
- Prod.instDivisionCommMonoid = DivisionCommMonoid.mk ⋯
Equations
- Prod.SubtractionCommMonoid = SubtractionCommMonoid.mk ⋯
Equations
- Prod.instAddGroup = AddGroup.mk ⋯
Equations
- Prod.instLeftCancelSemigroup = LeftCancelSemigroup.mk ⋯
Equations
- Prod.instAddLeftCancelSemigroup = AddLeftCancelSemigroup.mk ⋯
Equations
- Prod.instRightCancelSemigroup = RightCancelSemigroup.mk ⋯
Equations
- Prod.instAddRightCancelSemigroup = AddRightCancelSemigroup.mk ⋯
Equations
- Prod.instLeftCancelMonoid = LeftCancelMonoid.mk ⋯
Equations
- Prod.instAddLeftCancelMonoid = AddLeftCancelMonoid.mk ⋯
Equations
- Prod.instRightCancelMonoid = RightCancelMonoid.mk ⋯
Equations
- Prod.instAddRightCancelMonoid = AddRightCancelMonoid.mk ⋯
Equations
- Prod.instCancelMonoid = CancelMonoid.mk ⋯
Equations
- Prod.instAddCancelMonoid = AddCancelMonoid.mk ⋯
Equations
- Prod.instCommMonoid = CommMonoid.mk ⋯
Equations
- Prod.instAddCommMonoid = AddCommMonoid.mk ⋯
Equations
- Prod.instCancelCommMonoid = CancelCommMonoid.mk ⋯
Equations
- Prod.instAddCancelCommMonoid = AddCancelCommMonoid.mk ⋯
Equations
- Prod.instCommGroup = CommGroup.mk ⋯
Equations
- Prod.instAddCommGroup = AddCommGroup.mk ⋯
Given magmas M
, N
, the natural projection homomorphism from M × N
to M
.
Equations
- MulHom.fst M N = { toFun := Prod.fst, map_mul' := ⋯ }
Instances For
Given additive magmas A
, B
, the natural projection homomorphism
from A × B
to A
Equations
- AddHom.fst M N = { toFun := Prod.fst, map_add' := ⋯ }
Instances For
Given magmas M
, N
, the natural projection homomorphism from M × N
to N
.
Equations
- MulHom.snd M N = { toFun := Prod.snd, map_mul' := ⋯ }
Instances For
Given additive magmas A
, B
, the natural projection homomorphism
from A × B
to B
Equations
- AddHom.snd M N = { toFun := Prod.snd, map_add' := ⋯ }
Instances For
Prod.map
as an AddMonoidHom
Equations
- f.prodMap g = (f.comp (AddHom.fst M N)).prod (g.comp (AddHom.snd M N))
Instances For
Coproduct of two MulHom
s with the same codomain:
f.coprod g (p : M × N) = f p.1 * g p.2
.
(Commutative codomain; for the general case, see MulHom.noncommCoprod
)
Equations
- f.coprod g = f.comp (MulHom.fst M N) * g.comp (MulHom.snd M N)
Instances For
Coproduct of two AddHom
s with the same codomain:
f.coprod g (p : M × N) = f p.1 + g p.2
.
(Commutative codomain; for the general case, see AddHom.noncommCoprod
)
Equations
- f.coprod g = f.comp (AddHom.fst M N) + g.comp (AddHom.snd M N)
Instances For
Given monoids M
, N
, the natural projection homomorphism from M × N
to M
.
Equations
- MonoidHom.fst M N = { toFun := Prod.fst, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Given additive monoids A
, B
, the natural projection homomorphism
from A × B
to A
Equations
- AddMonoidHom.fst M N = { toFun := Prod.fst, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Given monoids M
, N
, the natural projection homomorphism from M × N
to N
.
Equations
- MonoidHom.snd M N = { toFun := Prod.snd, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Given additive monoids A
, B
, the natural projection homomorphism
from A × B
to B
Equations
- AddMonoidHom.snd M N = { toFun := Prod.snd, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Given monoids M
, N
, the natural inclusion homomorphism from M
to M × N
.
Equations
- MonoidHom.inl M N = { toFun := fun (x : M) => (x, 1), map_one' := ⋯, map_mul' := ⋯ }
Instances For
Given additive monoids A
, B
, the natural inclusion homomorphism
from A
to A × B
.
Equations
- AddMonoidHom.inl M N = { toFun := fun (x : M) => (x, 0), map_zero' := ⋯, map_add' := ⋯ }
Instances For
Given monoids M
, N
, the natural inclusion homomorphism from N
to M × N
.
Equations
- MonoidHom.inr M N = { toFun := fun (y : N) => (1, y), map_one' := ⋯, map_mul' := ⋯ }
Instances For
Given additive monoids A
, B
, the natural inclusion homomorphism
from B
to A × B
.
Equations
- AddMonoidHom.inr M N = { toFun := fun (y : N) => (0, y), map_zero' := ⋯, map_add' := ⋯ }
Instances For
Combine two MonoidHom
s f : M →* N
, g : M →* P
into f.prod g : M →* N × P
given by (f.prod g) x = (f x, g x)
.
Instances For
Combine two AddMonoidHom
s f : M →+ N
, g : M →+ P
into
f.prod g : M →+ N × P
given by (f.prod g) x = (f x, g x)
Instances For
prod.map
as a MonoidHom
.
Equations
- f.prodMap g = (f.comp (MonoidHom.fst M N)).prod (g.comp (MonoidHom.snd M N))
Instances For
prod.map
as an AddMonoidHom
.
Equations
- f.prodMap g = (f.comp (AddMonoidHom.fst M N)).prod (g.comp (AddMonoidHom.snd M N))
Instances For
Coproduct of two MonoidHom
s with the same codomain:
f.coprod g (p : M × N) = f p.1 * g p.2
.
(Commutative case; for the general case, see MonoidHom.noncommCoprod
.)
Equations
- f.coprod g = f.comp (MonoidHom.fst M N) * g.comp (MonoidHom.snd M N)
Instances For
Coproduct of two AddMonoidHom
s with the same codomain:
f.coprod g (p : M × N) = f p.1 + g p.2
.
(Commutative case; for the general case, see AddHom.noncommCoprod
.)
Equations
- f.coprod g = f.comp (AddMonoidHom.fst M N) + g.comp (AddMonoidHom.snd M N)
Instances For
The equivalence between M × N
and N × M
given by swapping the components
is multiplicative.
Equations
- MulEquiv.prodComm = { toEquiv := Equiv.prodComm M N, map_mul' := ⋯ }
Instances For
The equivalence between M × N
and N × M
given by swapping the
components is additive.
Equations
- AddEquiv.prodComm = { toEquiv := Equiv.prodComm M N, map_add' := ⋯ }
Instances For
The equivalence between (M × N) × P
and M × (N × P)
is multiplicative.
Equations
- MulEquiv.prodAssoc = { toEquiv := Equiv.prodAssoc M N P, map_mul' := ⋯ }
Instances For
The equivalence between (M × N) × P
and M × (N × P)
is additive.
Equations
- AddEquiv.prodAssoc = { toEquiv := Equiv.prodAssoc M N P, map_add' := ⋯ }
Instances For
Four-way commutativity of Prod
. The name matches mul_mul_mul_comm
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Four-way commutativity of Prod
.
The name matches mul_mul_mul_comm
Equations
- One or more equations did not get rendered due to their size.
Instances For
Product of multiplicative isomorphisms; the maps come from Equiv.prodCongr
.
Equations
- f.prodCongr g = { toEquiv := f.prodCongr g.toEquiv, map_mul' := ⋯ }
Instances For
Product of additive isomorphisms; the maps come from Equiv.prodCongr
.
Equations
- f.prodCongr g = { toEquiv := f.prodCongr g.toEquiv, map_add' := ⋯ }
Instances For
Multiplying by the trivial monoid doesn't change the structure.
Equations
- MulEquiv.uniqueProd = { toEquiv := Equiv.uniqueProd M N, map_mul' := ⋯ }
Instances For
Multiplying by the trivial monoid doesn't change the structure.
Equations
- AddEquiv.uniqueProd = { toEquiv := Equiv.uniqueProd M N, map_add' := ⋯ }
Instances For
Multiplying by the trivial monoid doesn't change the structure.
Equations
- MulEquiv.prodUnique = { toEquiv := Equiv.prodUnique M N, map_mul' := ⋯ }
Instances For
Multiplying by the trivial monoid doesn't change the structure.
Equations
- AddEquiv.prodUnique = { toEquiv := Equiv.prodUnique M N, map_add' := ⋯ }
Instances For
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.
Instances For
Canonical homomorphism of monoids from αˣ
into α × αᵐᵒᵖ
.
Used mainly to define the natural topology of αˣ
.
Equations
- Units.embedProduct α = { toFun := fun (x : αˣ) => (↑x, MulOpposite.op ↑x⁻¹), map_one' := ⋯, map_mul' := ⋯ }
Instances For
Canonical homomorphism of additive monoids from AddUnits α
into α × αᵃᵒᵖ
.
Used mainly to define the natural topology of AddUnits α
.
Equations
- AddUnits.embedProduct α = { toFun := fun (x : AddUnits α) => (↑x, AddOpposite.op ↑(-x)), map_zero' := ⋯, map_add' := ⋯ }
Instances For
Multiplication and division as homomorphisms #
Multiplication as a monoid homomorphism.
Equations
- mulMonoidHom = { toFun := mulMulHom.toFun, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Addition as an additive monoid homomorphism.
Equations
- addAddMonoidHom = { toFun := addAddHom.toFun, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Division as a monoid homomorphism.
Instances For
Subtraction as an additive monoid homomorphism.