ofAddUnits_addUnits_gc
theorem ofAddUnits_addUnits_gc :
∀ {M : Type u_1} [inst : AddMonoid M], GaloisConnection AddSubgroup.ofAddUnits AddSubmonoid.addUnits
The theorem `ofAddUnits_addUnits_gc` asserts that for any type `M` having an additive monoid structure, there exists a Galois connection between the function `AddSubgroup.ofAddUnits` and the function `AddSubmonoid.addUnits`. In other words, for all members `a` of the additive subgroup of additive units and all members `b` of the additive submonoid `M`, the condition that `AddSubgroup.ofAddUnits a` is less than or equal to `b` is logically equivalent to the condition that `a` is less than or equal to `AddSubmonoid.addUnits b`. This states a special kind of duality between certain operations on additive subgroups of additive units and additive submonoids.
More concisely: The theorem `ofAddUnits_addUnits_gc` states that for any additive monoid `M`, the function `AddSubgroup.ofAddUnits` and `AddSubmonoid.addUnits` form a Galois connection, i.e., for all `a` in the additive subgroup of additive units and `b` in `M`, `AddSubgroup.ofAddUnits a ≤ b` if and only if `a ≤ AddSubmonoid.addUnits b`.
|
ofUnits_units_gc
theorem ofUnits_units_gc : ∀ {M : Type u_1} [inst : Monoid M], GaloisConnection Subgroup.ofUnits Submonoid.units := by
sorry
The theorem `ofUnits_units_gc` states that for any type `M` that forms a monoid, there exists a Galois connection between the operation `Subgroup.ofUnits` and `Submonoid.units`. In other words, for every subgroup of units in `M`, there is a corresponding submonoid in `M` and vice versa. A Galois connection is a pair of operations related in such a way that an inequality involving one operation on one side implies and is implied by an inequality involving the other operation on the other side. This theorem thus provides a conceptual link between the structure of monoids and the structure of their associated unit groups.
More concisely: For any monoid `M`, there exists a Galois connection between `Subgroup.ofUnits` and `Submonoid.units`.
|