Algebra

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

Statistics

Metric	Count
Definitions	0
Theorems comap_map_eq_self_of_faithfullyFlat, comap_surjective_of_faithfullyFlat, exists_isPrime_liesOver_of_faithfullyFlat, faithfulSMul, of_comap_surjective, of_flat_of_isLocalHom, of_specComap_surjective, tensorProduct_mk_injective, comap_surjective_of_faithfullyFlat, specComap_surjective_of_faithfullyFlat	10
Total	10

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_map_eq_self_of_faithfullyFlat 📖	mathematical	—	comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass map	—	le_antisymm RingHom.instRingHomClass IsScalarTower.right RingHomCompTriple.ids Algebra.to_smulCommClass LinearMap.IsScalarTower.compatibleSMul TensorProduct.isScalarTower_left Quotient.isScalarTower TensorProduct.smulCommClass_left smulCommClass_self LinearMap.coe_comp AlgEquiv.injective Module.FaithfullyFlat.tensorProduct_mk_injective instIsTwoSided_1 Quotient.eq_zero_iff_mem mem_comap TensorProduct.tmul_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass le_comap_map
comap_surjective_of_faithfullyFlat 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass	—	RingHom.instRingHomClass comap_map_eq_self_of_faithfullyFlat
exists_isPrime_liesOver_of_faithfullyFlat 📖	mathematical	—	IsPrime CommSemiring.toSemiring CommRing.toCommSemiring LiesOver	—	RingHom.instRingHomClass comap_map_eq_self_iff_of_isPrime comap_map_eq_self_of_faithfullyFlat

Module.FaithfullyFlat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithfulSMul 📖	mathematical	—	FaithfulSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring	—	tensorProduct_mk_injective TensorProduct.smulCommClass_left smulCommClass_self mul_one TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.left IsScalarTower.right
of_comap_surjective 📖	mathematical	PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.comap algebraMap CommSemiring.toSemiring	Module.FaithfullyFlat Ring.toAddCommGroup CommRing.toRing Algebra.toModule	—	Ideal.IsMaximal.isPrime IsScalarTower.left RingHom.instRingHomClass PrimeSpectrum.comap_asIdeal IsScalarTower.right Ideal.smul_top_eq_map Iff.ne Submodule.restrictScalars_eq_top_iff Ideal.IsPrime.ne_top PrimeSpectrum.isPrime top_le_iff Ideal.map_comap_le
of_flat_of_isLocalHom 📖	mathematical	—	Module.FaithfullyFlat Ring.toAddCommGroup CommRing.toRing Algebra.toModule CommRing.toCommSemiring CommSemiring.toSemiring	—	IsScalarTower.left IsScalarTower.right Ideal.smul_top_eq_map IsLocalRing.eq_maximalIdeal List.TFAE.out RingHom.instRingHomClass IsLocalRing.local_hom_TFAE Ideal.IsPrime.ne_top' Ideal.IsMaximal.isPrime' IsLocalRing.maximalIdeal.isMaximal Submodule.restrictScalars_eq_top_iff top_le_iff
of_specComap_surjective 📖	mathematical	PrimeSpectrum CommRing.toCommSemiring PrimeSpectrum.comap algebraMap CommSemiring.toSemiring	Module.FaithfullyFlat Ring.toAddCommGroup CommRing.toRing Algebra.toModule	—	of_comap_surjective
tensorProduct_mk_injective 📖	mathematical	—	TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid Algebra.toModule CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	TensorProduct.smulCommClass_left smulCommClass_self lTensor_injective_iff_injective RingHomCompTriple.ids RingHomInvPair.ids TensorProduct.ext' LinearMap.coe_comp LinearEquiv.coe_coe EmbeddingLike.comp_injective EquivLike.toEmbeddingLike Algebra.TensorProduct.mk_one_injective_of_isScalarTower Algebra.to_smulCommClass TensorProduct.isScalarTower_left IsScalarTower.right

PrimeSpectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_surjective_of_faithfullyFlat 📖	mathematical	—	PrimeSpectrum CommRing.toCommSemiring comap algebraMap CommSemiring.toSemiring	—	RingHom.instRingHomClass mem_range_comap_iff Ideal.comap_map_eq_self_of_faithfullyFlat
specComap_surjective_of_faithfullyFlat 📖	mathematical	—	PrimeSpectrum CommRing.toCommSemiring comap algebraMap CommSemiring.toSemiring	—	comap_surjective_of_faithfullyFlat

---

← Back to Index