TropicalGeometry: tropical linear spaces from graphs

[YueRen]

This pull requests adds a new constructor for tropical linear spaces from graphs. Useful (for me) for example for graph rigidity questions (see e.g. here).

[YueRen]

@ollieclarke8787 Would you be able to review this pull request?

[codecov]

Codecov Report

Attention: Patch coverage is 81.81818% with 4 lines in your changes missing coverage. Please review.

Project coverage is 84.40%. Comparing base (3e86180) to head (67a77f1).
Report is 161 commits behind head on master.

Files with missing lines	Patch %	Lines
src/TropicalGeometry/linear_space.jl	81.81%	4 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #4445      +/-   ##
==========================================
- Coverage   84.55%   84.40%   -0.16%     
==========================================
  Files         672      673       +1     
  Lines       88880    90278    +1398     
==========================================
+ Hits        75152    76198    +1046     
- Misses      13728    14080     +352     

Files with missing lines	Coverage Δ
src/TropicalGeometry/linear_space.jl	85.71% <81.81%> (+4.59%)	⬆️

... and 187 files with indirect coverage changes

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[ollieclarke8787]

Code correctly produces Bergman fan of the cycle matroid the graph. The example of K_3 is also correct.

[fingolfin]

I am not sure who from the inside is able to review (and approve!) this tropical geometry PR. Perhaps someone from Berlin, e.g. @lkastner @benlorenz @micjoswig ?

[micjoswig]

The docs on tropical linear spaces (and the rest of tropical geometry) need to state explicitly where the various objects (tropical varieties, tropical linear spaces etc) actually live. Candidates include R^n or the tropical projective torus R^n/R1 (in the homogeneous setting). Either there are choices for the user to make, or there are fixed global decisions.

Specifically, tropical linear spaces may also be viewed as tropical polytopes. And then there are more choices, for they can be considered in a tropical projective torus or in a tropical projective space. I guess, none of this is currently supported in OSCAR.

The role of Bergman fans and constant vs non-constant coefficients must be explained.

[YueRen]

Good points, I will adjust the documentation accordingly.

[YueRen]

Besides enabling the constructing of tropical linear spaces from graphs, the following have changed:

1. Replaced how optional TropicalSemiringMap are written. Before the function signature included nu::Union{Nothing,TropicalSemiringMap}=nothing and the function body included code that set nu when nu==nothing. Now this is done in the function signature directly like:

function tropical_linear_space(I::MPolyIdeal, nu::TropicalSemiringMap=tropical_semiring_map(coefficient_ring(I)); weighted_polyhedral_complex_only::Bool=false)

2. Adding a few sentences to the documentation, that emphasize that

• tropical linear spaces in OSCAR live in the euclidean space, not the tropical torus
• tropical linear spaces under a trivial valuation are Bergman fans and they may have different structures depending on how they are constructed

[micjoswig]

I think it is OK now.

Some minor edits, e.g., improving the docs further, can be made after the merge. I find that easier than messing with the code in an external repo.