Descent

📁 Source: Mathlib/RingTheory/Flat/FaithfullyFlat/Descent.lean

Statistics

Metric	Count
Definitions	0
Theorems bijective_of_tensorProduct, injective_of_tensorProduct, surjective_of_tensorProduct, codescendsAlong_bijective, codescendsAlong_injective, codescendsAlong_surjective	6
Total	6

Module.FaithfullyFlat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_of_tensorProduct 📖	—	Function.Bijective TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring Algebra.TensorProduct.instSemiring RingHom.instFunLike algebraMap Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	—	Algebra.to_smulCommClass injective_of_tensorProduct surjective_of_tensorProduct
injective_of_tensorProduct 📖	—	TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring Algebra.TensorProduct.instSemiring RingHom.instFunLike algebraMap Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	—	Algebra.to_smulCommClass IsScalarTower.to_smulCommClass IsScalarTower.right LinearMap.IsScalarTower.compatibleSMul TensorProduct.isScalarTower_left RingHomCompTriple.ids RingHomInvPair.ids TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.left TensorProduct.isScalarTower LinearMap.ext LinearMap.ext_ring map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_smul lTensor_injective_iff_injective LinearMap.IsScalarTower.compatibleSMul'
surjective_of_tensorProduct 📖	—	TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring Algebra.TensorProduct.instSemiring RingHom.instFunLike algebraMap Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	—	Algebra.to_smulCommClass IsScalarTower.to_smulCommClass IsScalarTower.right LinearMap.IsScalarTower.compatibleSMul TensorProduct.isScalarTower_left RingHomCompTriple.ids RingHomInvPair.ids TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.left TensorProduct.isScalarTower LinearMap.ext LinearMap.ext_ring map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_smul lTensor_surjective_iff_surjective LinearMap.IsScalarTower.compatibleSMul'

RingHom.FaithfullyFlat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codescendsAlong_bijective 📖	mathematical	—	RingHom.CodescendsAlong Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.FaithfullyFlat	—	RingHom.CodescendsAlong.and codescendsAlong_injective codescendsAlong_surjective
codescendsAlong_injective 📖	mathematical	—	RingHom.CodescendsAlong DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.FaithfullyFlat	—	RingHom.injective_respectsIso Algebra.to_smulCommClass Module.FaithfullyFlat.injective_of_tensorProduct RingHom.faithfullyFlat_algebraMap_iff
codescendsAlong_surjective 📖	mathematical	—	RingHom.CodescendsAlong DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.FaithfullyFlat	—	RingHom.surjective_respectsIso Algebra.to_smulCommClass Module.FaithfullyFlat.surjective_of_tensorProduct RingHom.faithfullyFlat_algebraMap_iff

---

← Back to Index