Structures · Algebra
Module.FaithfullyFlat
A module M over a commutative ring R is faithfully flat if it is flat and,
for all R-linear maps f : N → N' such that id ⊗ f = 0, we have f = 0.
- Shape
- 2 explicit arguments · adds submodule_ne_top
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by61
- Module.FaithfullyFlat.zero_iff_lTensor_zero
- Module.FaithfullyFlat.lTensor_injective_iff_injective
- Module.FaithfullyFlat.rTensor_reflects_triviality
- Ideal.comap_map_eq_self_of_faithfullyFlat
- Module.FaithfullyFlat.lTensor_surjective_iff_surjective
- Algebra.FiniteType.of_finiteType_tensorProduct_of_faithfullyFlat
- Submodule.baseChangeOrderEmbedding
- Module.FaithfullyFlat.lTensor_reflects_triviality
- Algebra.FormallyUnramified.of_formallyUnramified_tensorProduct_of_faithfullyFlat
- Module.FaithfullyFlat.lTensor_reflects_exact
- Module.FaithfullyFlat.subsingleton_tensorProduct_iff_right
- Module.FaithfullyFlat.rTensor_reflects_exact
- Module.FaithfullyFlat.surjective_of_tensorProduct
- Module.FaithfullyFlat.trans
- Algebra.Smooth.of_smooth_tensorProduct_of_faithfullyFlat
- Module.Flat.of_flat_tensorProduct
- Module.Finite.of_finite_tensorProduct_of_faithfullyFlat
- Algebra.FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlat
- Module.FaithfullyFlat.lTensor_exact_iff_exact
- Module.FaithfullyFlat.injective_of_tensorProduct
- Submodule.IsArtinian.of_isArtinian_tensorProduct_of_faithfullyFlat
- PrimeSpectrum.comap_surjective_of_faithfullyFlat
- Module.FaithfullyFlat.zero_iff_rTensor_zero
- Module.FaithfullyFlat.of_linearEquiv
- Module.FaithfullyFlat.rTensor_exact_iff_exact
- Ideal.FG.of_FG_map_of_faithfullyFlat
- Module.FaithfullyFlat.subsingleton_tensorProduct_iff_left
- Module.FaithfullyFlat.one_tmul_eq_zero_iff
- Algebra.IsEffective.of_isEffective_tensorProduct_of_faithfullyFlat
- Algebra.Etale.of_etale_tensorProduct_of_faithfullyFlat
- Submodule.IsNoetherian.of_isNoetherian_tensorProduct_of_faithfullyFlat
- Module.FaithfullyFlat.lTensor_bijective_iff_bijective
- IsBaseChange.map_smul_top_ne_top_iff_of_faithfullyFlat
- Module.FaithfullyFlat.range_le_ker_of_exact_rTensor
- Algebra.IsEffective.of_faithfullyFlat
- Module.FaithfullyFlat.tensorProduct_mk_injective
- Submodule.baseChange_inj
- RingTheory.Sequence.IsRegular.of_faithfullyFlat_of_isBaseChange
- Module.FaithfullyFlat.isLocalRing
- Ideal.exists_isPrime_liesOver_of_faithfullyFlat
- Algebra.codRestrictEqLocusPushoutCocone.bijective_of_faithfullyFlat
- Module.FaithfullyFlat.bijective_of_tensorProduct
- Module.FaithfullyFlat.instTensorProduct
- Module.FaithfullyFlat.nontrivial_tensorProduct_iff_right
- Module.FaithfullyFlat.faithfulSMul
- Module.FaithfullyFlat.lTensor_nontrivial
- Submodule.baseChangeOrderEmbedding_apply
- Module.Flat.iff_flat_tensorProduct
- Ideal.comap_surjective_of_faithfullyFlat
- Submodule.baseChange_injective