Submonoid of units #
Given a submonoid S
of a monoid M
, we define the subgroup S.units
as the units of S
as a
subgroup of Mˣ
. That is to say, S.units
contains all members of S
which have a
two-sided inverse within S
, as terms of type Mˣ
.
We also define, for subgroups S
of Mˣ
, S.ofUnits
, which is S
considered as a submonoid
of M
. Submonoid.units
and Subgroup.ofUnits
form a Galois coinsertion.
We also make the equivalent additive definitions.
Implementation details #
There are a number of other constructions which are multiplicatively equivalent to S.units
but
which have a different type.
Definition | Type |
---|---|
S.units |
Subgroup Mˣ |
Sˣ |
Type u |
IsUnit.submonoid S |
Submonoid S |
S.units.ofUnits |
Submonoid M |
All of these are distinct from S.leftInv
, which is the submonoid of M
which contains
every member of M
with a right inverse in S
.
The additive units of S
, packaged as an additive subgroup of AddUnits M
.
Equations
- S.addUnits = { toAddSubmonoid := AddSubmonoid.comap (AddUnits.coeHom M) S ⊓ -AddSubmonoid.comap (AddUnits.coeHom M) S, neg_mem' := ⋯ }
Instances For
The units of S
, packaged as a subgroup of Mˣ
.
Equations
- S.units = { toSubmonoid := Submonoid.comap (Units.coeHom M) S ⊓ (Submonoid.comap (Units.coeHom M) S)⁻¹, inv_mem' := ⋯ }
Instances For
A additive subgroup of additive units represented as a additive submonoid of M
.
Equations
- S.ofAddUnits = AddSubmonoid.map (AddUnits.coeHom M) S.toAddSubmonoid
Instances For
A subgroup of units represented as a submonoid of M
.
Equations
- S.ofUnits = Submonoid.map (Units.coeHom M) S.toSubmonoid
Instances For
A Galois coinsertion exists between the coercion from a additive subgroup of additive units to a additive submonoid and the reduction from a additive submonoid to its unit group.
Equations
- ofAddUnits_addUnits_gci = GaloisCoinsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯
Instances For
A Galois coinsertion exists between the coercion from a subgroup of units to a submonoid and the reduction from a submonoid to its unit group.
Equations
- ofUnits_units_gci = GaloisCoinsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯
Instances For
The equivalence between the additive subgroup of additive units of
S
and the type of additive units of S
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The equivalence between the additive subgroup of additive units of
S
and the additive submonoid of additive unit elements of S
.
Equations
- S.addUnitsEquivIsAddUnitAddSubmonoid = S.addUnitsEquivAddUnitsType.trans AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid
Instances For
The equivalence between the subgroup of units of S
and the submonoid of unit
elements of S
.
Equations
- S.unitsEquivIsUnitSubmonoid = S.unitsEquivUnitsType.trans Submonoid.unitsTypeEquivIsUnitSubmonoid
Instances For
Given some x : M
which is a member of the additive submonoid of additive unit
elements corresponding to a subgroup of units, produce a unit of M
whose coercion is equal to
x
.
Equations
- S.addUnit_of_mem_ofAddUnits h = (Classical.choose h).copy x ⋯ ↑(-Classical.choose h) ⋯
Instances For
Given some x : M
which is a member of the submonoid of unit elements corresponding to a
subgroup of units, produce a unit of M
whose coercion is equal to x
. `
Equations
- S.unit_of_mem_ofUnits h = (Classical.choose h).copy x ⋯ ↑(Classical.choose h)⁻¹ ⋯
Instances For
The equivalence between the coercion of an additive subgroup S
of
Mˣ
to an additive submonoid of M
and the additive subgroup itself as a type.
Equations
- S.ofAddUnitsEquivType = { toFun := fun (x : ↥S.ofAddUnits) => ⟨S.addUnit_of_mem_ofAddUnits ⋯, ⋯⟩, invFun := fun (x : ↥S) => ⟨↑↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
The equivalence between the coercion of a subgroup S
of Mˣ
to a submonoid of M
and
the subgroup itself as a type.
Equations
- S.ofUnitsEquivType = { toFun := fun (x : ↥S.ofUnits) => ⟨S.unit_of_mem_ofUnits ⋯, ⋯⟩, invFun := fun (x : ↥S) => ⟨↑↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
Instances For
The equivalence between the additive subgroup of additive units of
S
and the additive submonoid of additive unit elements of S
.
Instances For
The equivalence between the greatest subgroup of additive units
contained within T
and T
itself.
Equations
- H.addUnitsEquivSelf = H.addUnitsEquivAddUnitsType.trans toAddUnits.symm