feat(Algebra/Category): some lemmas about adjunctions in Under R

[undergraduate-ruiqi-chen]

Proves tensor-forgetful and free-forgetful adjunctions for Under R

[github-actions]

PR summary c501ba7387

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Category.Ring.Under.Adjunctions (new file)	1406
Mathlib.Algebra.Category.Ring.Topology (new file)	1482

---

Declarations diff

+ Function.Surjective.isEmbedding_comp
+ Under_ℤ
+ adjFreeForget
+ adjTensorForget
+ algebra
+ closure_range_union_range_eq_top_of_isPushout
+ coe_prodUnique
+ coe_uniqueProd
+ continuous_apply
+ continuous_precomp
+ forget
+ forgetRelative
+ freeAbs
+ freeAbs_map
+ freeAbs_obj
+ freeAbs_ℤ_tauto
+ instance (R : CommRingCat.{u}) : Algebra (of (ULift.{u, 0} ℤ)) R
+ instance [TopologicalSpace S] [IsTopologicalRing S] [T1Space S] [CompactSpace S] :
+ instance [TopologicalSpace S] [T2Space S] : T2Space (R ⟶ S)
+ isClosedEmbedding_hom
+ isClosedEmbedding_precomp_of_surjective
+ isEmbedding_hom
+ isEmbedding_precomp_of_surjective
+ isEmbedding_pushout
+ isHomeomorph_precomp
+ mkUnder_eq
+ mvPolynomialHomeo
+ precompHomeo
+ prodUnique
+ tensorProd_freeAbs
+ tensorProd_freeAbs_tauto
+ toUnder_eq
+ topFunctor
+ topFunctor_forget
+ uniqueProd
- instance (A : Under R) : Algebra R A := RingHom.toAlgebra A.hom.hom

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