feat(Algebra/Category): Under.pushout f is left-exact if f is flat.

[chrisflav]

---

• depends on: feat(Algebra/Category): API for Under R #19058

[github-actions]

PR summary 0388324e34

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Category.Ring.Constructions	1289	1298	+9 (+0.70%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Etale.Field	4
39 files Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.Localization.Finiteness Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.NumberTheory.Cyclotomic.Three Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.Localization.Free Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.RingTheory.RingHom.Locally Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.RingHomProperties Mathlib.Algebra.Category.Ring.Constructions Mathlib.RingTheory.LocalProperties.Basic Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.RingTheory.RingHom.Surjective Mathlib.RingTheory.DedekindDomain.PID Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.AdeleRing	9
Mathlib.RingTheory.TensorProduct.Pi	925
Mathlib.Algebra.Category.Ring.Under.Basic	1306
Mathlib.Algebra.Category.Ring.Under.Limits	1644

---

Declarations diff

+ Algebra.TensorProduct.piRight
+ Algebra.TensorProduct.piRight_tmul
+ Under.equalizerFork
+ Under.equalizerFork'
+ Under.equalizerFork'IsLimit
+ Under.equalizerFork'_ι
+ Under.equalizerForkIsLimit
+ Under.equalizerFork_ι
+ Under.piFan
+ Under.piFanIsLimit
+ equalizerForkTensorProdIso
+ equalizer_comp
+ hom_left_inv_left
+ hom_right_inv_right
+ instance (A : Under R) : Algebra R A := RingHom.toAlgebra A.hom
+ instance (J : Type u) [Finite J] (f : J → Under R) :
+ instance (J : Type) [Finite J] :
+ instance : CoeSort (Under R) (Type u)
+ instance : PreservesFiniteProducts (Under.pushout f)
+ instance : PreservesFiniteProducts (tensorProd R S)
+ instance [Module.Flat R S] : PreservesFiniteLimits (tensorProd R S)
+ instance [Module.Flat R S] : PreservesLimitsOfShape WalkingParallelPair (tensorProd R S)
+ instance [Module.Flat R S] {A B : Under R} (f g : A ⟶ B) :
+ inv_left_hom_left
+ inv_right_hom_right
+ isPushout_tensorProduct
+ map_comp_id
+ map_id_comp
+ mkUnder
+ mkUnder_ext
+ piFanTensorProductIsLimit
+ piRightHom
+ piRightHom_mul
+ piRightHom_one
+ preservesColimitsOfShapeDiscrete
+ preservesFiniteLimitsOfFlat
+ preservesLimitsOfShapeDiscrete
+ pushout_inl_tensorProdObjIsoPushoutObj_inv_right
+ pushout_inr_tensorProdObjIsoPushoutObj_inv_right
+ tensorProd
+ tensorProdEqualizer
+ tensorProdEqualizer_ι
+ tensorProdIsoPushout
+ tensorProdIsoPushout_app
+ tensorProdMapEqualizerForkIsLimit
+ tensorProdObjIsoPushoutObj
+ tensorProductFan
+ tensorProductFan'
+ tensorProductFanIsLimit
+ tensorProductFanIso
+ toAlgHom
+ toAlgHom_apply
+ toAlgHom_comp
+ toAlgHom_id
+ toUnder_comp
+ toUnder_hom_right_apply
+ toUnder_inv_right_apply
+ toUnder_right
+ toUnder_trans
++ toUnder
++++ coe_comp_of'

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Algebra/Category): API for Under R #19058
  By Dependent Issues (🤖). Happy coding!