[Merged by Bors] - feat(LinearAlgebra/Projectivization/Subspace): correspondence between linear and projective subspaces

[gasparattila]

---

[github-actions]

PR summary 1f467e3c77

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ mem_projectivization_iff_submodule_le
+ mem_submodule_iff
+ mk_mem_projectivization_iff
+ projectivization
+ submodule

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

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

[gasparattila]

Thanks for the suggestions! I realized that the inverse is inconvenient to use, so I added an abbrev for the inverse. I also added a lemma relating the definition to the submodule of a single point.

[Vierkantor]

I have a few comments, overall it looks quite nice. Do you have any further work building on this, so I can get a bit of context?

[gasparattila]

Thanks for the suggestions! The motivation for this is defining bundled projective transforms. This could be done using a class like this:

class IsProjectivization K V P [Field K] [Module K V] where
  equiv : P ≃ Projectivization K V

Then we would have an instance IsProjectivization K s.submodule s for s : Projectivization.Subspace K V to allow defining maps between subspaces. But I'm not sure if this is the best design and I'm currently not planning to work on this.

-awaiting-author

[Vierkantor]

I took a look at the proofs and found some tricks to make them a bit shorter and more elegant. With those changes, we should be ready to merge, thank you for all the work! 🎉

bors d+

[mathlib-bors]

✌️ gasparattila can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[gasparattila]

bors r+

[mathlib-bors]

Build failed (retrying...):

• Lint style

[mathlib-bors]

Build failed (retrying...):

• Post-Build Step

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Post-Build Step
• Build