refactor(Algebra/Order): unbundle group and ring cone

[artie2000]

• Unbundle GroupCone and RingCone using Submonoid.IsMulPointed

The material in Mathlib.Algebra.Group.Submonoid.Support was created to treat uniformly

• positive cones in groups and rings
• pointed cones in vector spaces over an ordered field
• orderings in rings

This PR deprecates the GroupCone and RingCone structures, making use of the predicates Submonoid.IsMulPointed and AddSubmonoid.IsPointed defined in that file instead.

See also #36863 for the analogous change to ring orderings.

---

[github-actions]

PR summary 35471d41e9

Import changes exceeding 2%

%	File
+89.37%	Mathlib.Algebra.Order.Group.Cone
+67.15%	Mathlib.Algebra.Order.Ring.Cone

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Order.Group.Cone	348	659	+311 (+89.37%)
Mathlib.Algebra.Order.Ring.Cone	414	692	+278 (+67.15%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Order.Ring.Cone	278
Mathlib.Algebra.Order.Group.Cone	311

---

Declarations diff

+ IsOrderedMonoid.mkOfSubmonoid
+ IsOrderedRing.mkOfSubsemiring
+ LinearOrder.mkOfSubmonoid
+ PartialOrder.mkOfSubmonoid
+ PartialOrder.mkOfSubmonoid_le_iff
+ Submonoid.oneLE.isMulPointed
+ Submonoid.oneLE.isMulSpanning
+ Subsemiring.nonneg.isPointed
+ Subsemiring.nonneg.isSpanning

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (3.00, 0.12)

Current number	Change	Type
25	3	disabled deprecation lints

Current commit 85c2dc228d
Reference commit 35471d41e9

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[joneugster]

Could you please extend the PR description explaining why this is desired or what thee benefits are? And if there is a relevant Zulip discussion, could you please link that, too?

Not sure I'm the right person to review. I'll unassign myself for now but keep this on my list to revisit again

[YaelDillies]

Are we never going to talk about suprema/infima of group cones?

Why unbundle group cones and not other types of subobjects. Is the point that group cones aren't subobjects?

[Vierkantor]

I agree with Jon that we should discuss this on Zulip before more review.

[artie2000]

@YaelDillies the operations on them are just the operations on the underlying submonoids / subsemirings. They don't have a sup or sInf in general. I believe this is the exact reasoning you used to convince me to unbundle RingPreordering, which led to me writing unbundled group/ring cones (Submonoid.IsPointed) in the first place.

[artie2000]

Before I stopped contributing for around a month, I had spent months trying to get engagement on discussing this design on Zulip, to little avail. I don't think it makes sense to have the bundled and the unbundled version at the same time, so we should pick one and stick with it. My understanding of the consensus for bundling/unbundling subobjects was that we should bundle when the objects form a lattice and unbundle when we can't define lattice operations on them.
https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Ring.20orderings.20-.20structure.20or.20predicate.3F/with/562594050

[artie2000]

Removed awaiting-zulip because there is no active Zulip discussion and the previous discussion on this topic got little engagement.

[YaelDillies]

Suggested change

	theorem Submonoid.oneLE.isMulPointed [PartialOrder G] [IsOrderedMonoid G] :
	(oneLE G).IsMulPointed := by aesop (add simp ge_antisymm_iff)
	theorem Submonoid.IsMulPointed.oneLE [PartialOrder G] [IsOrderedMonoid G] :
	(oneLE G).IsMulPointed := by aesop (add simp ge_antisymm_iff)

Same below

[YaelDillies]

Suggested change

	abbrev PartialOrder.mkOfSubmonoid : PartialOrder G where
	abbrev PartialOrder.ofSubmonoid : PartialOrder G where

is clear enough IMO

[YaelDillies]

Suggested change

	@[to_additive
	/-- Construct a partial order by designating a submonoid with zero support in an abelian group. -/]
	abbrev PartialOrder.mkOfSubmonoid : PartialOrder G where
	@[to_additive (attr := implicit_reducible)
	/-- Construct a partial order by designating a submonoid with zero support in an abelian group. -/]
	def PartialOrder.mkOfSubmonoid : PartialOrder G where

is preferred now I believe

[YaelDillies]

Suggested change

	a maximal submonoid with zero support in an abelian group. -/
	a maximal submonoid with zero support in an abelian group. -/

Same below

[YaelDillies]

Suggested change

	theorem Subsemiring.nonneg.isPointed [PartialOrder R] [IsOrderedRing R] :
	(Subsemiring.nonneg R).IsPointed := AddSubmonoid.nonneg.isPointed R
	theorem Subsemiring.nonneg.isSpanning [LinearOrder R] [IsOrderedRing R] :
	theorem Subsemiring.IsPointed.nonneg [PartialOrder R] [IsOrderedRing R] :
	(Subsemiring.nonneg R).IsPointed := AddSubmonoid.nonneg.isPointed R
	theorem Subsemiring.IsPointed.nonneg [LinearOrder R] [IsOrderedRing R] :

[YaelDillies]

I don't really mind that there was no discussion on Zulip. All I care about is that the PR description AND the code document why the situation is different to all the subobjects, so that your refactor doesn't get undone in the future.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.