feat(Geometry/Convex/Cone/Pointed): face lattice of pointed cones

[ooovi]

• Define PointedCone.IsFaceOf, for a pointed cone being a face of another pointed cone.
• Prove some basic properties, that faces are extreme sets of their cone, and how they behave under intersection, map and product operations.
• Define Face by bundling the IsFaceOf structure, and show the complete lattice structure on it.
• Prove that taking the product of two faces is an order isomorphism.

Co-authored-by: Martin Winter

---

• depends on: [Merged by Bors] - feat(Geometry/Convex/Cone): lineality space of pointed cones #33780 for the definition of the lineal space

[github-actions]

PR summary 77d929d750

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Convex.Cone.Face.Basic (new file)	1073
Mathlib.Geometry.Convex.Cone.Face.Lattice (new file)	1074

---

Declarations diff

+ Face
+ IsFaceOf
+ comap
+ ext
+ fst_prod
+ fst_prod_snd
+ inf
+ inf_left
+ inf_right
+ instance : CoeOut (Face C) (PointedCone R M) := ⟨toPointedCone⟩
+ instance : CompleteLattice (Face C)
+ instance : CompleteSemilatticeInf (Face C)
+ instance : InfSet (Face C)
+ instance : Inhabited (Face C) := ⟨⊤⟩
+ instance : Min (Face C)
+ instance : Nonempty (Face C) := ⟨⊤⟩
+ instance : PartialOrder (Face C) := .ofSetLike (Face C) M
+ instance : SemilatticeInf (Face C)
+ instance : SetLike (Face C) M
+ isExtreme
+ isFaceOf_comap_iff
+ isFaceOf_iff_le
+ isFaceOf_iff_mem_of_add_mem
+ isFaceOf_iff_mem_of_smul_add_smul_mem
+ isFaceOf_map_iff
+ lineal
+ lineal_congr
+ lineal_eq_bot
+ lineal_le
+ map
+ map_equiv
+ mem_add_iff
+ mem_coe
+ mem_of_add_mem
+ mem_of_sum_smul_mem
+ of_comap_surjective
+ prodOrderIso
+ prod_mono
+ refl
+ rfl
+ snd_prod
+ sum_mem_iff_mem
+ toPointedCone
+ toPointedCone_le_toPointedCone
+ toPointedCone_lt_toPointedCone
+ trans
++ fst
++ prod
++ snd

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.

---

No changes to technical debt.

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).

[YaelDillies]

Per the discussion on Zulip, perhaps let's not create this new Pointed folder

[YaelDillies]

Do you really need to give this explicitly?

Suggested change

inf := min

[ooovi]

it seems so...

[YaelDillies]

Hmm, weird. I'll have a look later

[YaelDillies]

Looks like this file has converged. Do you want to move .Lattice to a later PR so that we can move forward here?

[martinwintermath]

Do you expect much further work on Lattice? I felt we are near the end here, no?

[YaelDillies]

Maybe, I am simply trying to be helpful and proactively ensure that no part of your PR gets blocked on details in other parts

[Rida-Hamadani]

Thank you!

[Rida-Hamadani]

Suggested change

	constructor <;> intro h
	· exact ⟨h.le, IsFaceOf.mem_of_add_mem h⟩
	· refine ⟨h.1, fun {x y a} xC yC a0 haxy => ?_⟩
	have := smul_mem _ (inv_nonneg.mpr (le_of_lt a0)) <| h.2 (smul_mem _ (le_of_lt a0) xC) yC haxy
	simpa [← smul_assoc, inv_mul_cancel₀ (ne_of_gt a0)] using this
	refine ⟨fun h ↦ ⟨h.le, h.mem_of_add_mem⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, fun hx hy ha haxy ↦ ?_⟩⟩
	simpa [← smul_assoc, inv_mul_cancel₀ (ne_of_gt ha)] using smul_mem _
	(inv_nonneg.mpr (le_of_lt ha)) <| h₂ (smul_mem _ (le_of_lt ha) hx) hy haxy

Some of the proofs could be made cleaner by making use of refine, this is an example, but the same ideas apply elsewhere too.

[YaelDillies]

Can you put it on the declarations that need it instead?

Suggested change

	@[expose] public section
	public section

[ooovi]

I don't know how to determine who needs it. I somehow thought everything ought to be exposed, given how many files in mathlib are?