Commit 2024-11-26 11:45 841cc90f

View on Github →

feat(Algebra/Category): API for Under R (#19058) We provide API for Under R where R : CommRingCat. We also add some simp lemmas for the various ring categories.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean

Modified Mathlib/Algebra/Category/Ring/Basic.lean

added theorem CommRingCat.coe_comp_of'

added theorem CommSemiRingCat.coe_comp_of'

added theorem RingCat.coe_comp_of'

added theorem SemiRingCat.coe_comp_of'

Modified Mathlib/Algebra/Category/Ring/Constructions.lean

added theorem CommRingCat.isPushout_tensorProduct

Created Mathlib/Algebra/Category/Ring/Under/Basic.lean

added def AlgEquiv.toUnder

added theorem AlgEquiv.toUnder_hom_right_apply

added theorem AlgEquiv.toUnder_inv_right_apply

added theorem AlgEquiv.toUnder_trans

added def AlgHom.toUnder

added theorem AlgHom.toUnder_comp

added theorem AlgHom.toUnder_right

added def CommRingCat.mkUnder

added theorem CommRingCat.mkUnder_ext

added theorem CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right

added theorem CommRingCat.pushout_inr_tensorProdObjIsoPushoutObj_inv_right

added def CommRingCat.tensorProd

added def CommRingCat.tensorProdIsoPushout

added theorem CommRingCat.tensorProdIsoPushout_app

added def CommRingCat.tensorProdObjIsoPushoutObj

added def CommRingCat.toAlgHom

added theorem CommRingCat.toAlgHom_apply

added theorem CommRingCat.toAlgHom_comp

added theorem CommRingCat.toAlgHom_id

Modified Mathlib/CategoryTheory/Comma/Over.lean

added theorem CategoryTheory.Over.hom_left_inv_left

added theorem CategoryTheory.Over.inv_left_hom_left

added theorem CategoryTheory.Under.hom_right_inv_right

added theorem CategoryTheory.Under.inv_right_hom_right

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

added theorem Algebra.TensorProduct.map_comp_id

added theorem Algebra.TensorProduct.map_id_comp