Theorems · Definition · commutative algebra
RingHom.FaithfullyFlat
{R : Type u_3} → {S : Type u_4} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → PropA ring map f : R →+* S is faithfully flat if S is faithfully flat as an R-algebra.
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- RingHomstatement and proof · cited by 10,189
- Module.FaithfullyFlatproof · cited by 72
Cited by28
Results whose statement or proof uses this declaration.
- RingHom.FaithfullyFlat.iff_flat_and_comap_surjectivestatement and proof · cited by 5
- RingHom.faithfullyFlat_algebraMap_iffstatement · cited by 3
- CommRingCat.Opposite.regularEpiOfFaithfullyFlatstatement and proof · cited by 1
- CommRingCat.regularMonoOfFaithfullyFlatstatement and proof · cited by 1
- RingHom.FaithfullyFlat.codescendsAlong_injectivestatement and proof · cited by 1
- RingHom.FaithfullyFlat.codescendsAlong_surjectivestatement and proof · cited by 1
- RingHom.FaithfullyFlat.injectivestatement and proof · cited by 1
- RingHom.FaithfullyFlat.of_bijectivestatement · cited by 1
- RingHom.FaithfullyFlat.respectsIsostatement · cited by 1
- RingHom.FaithfullyFlat.stableUnderCompositionstatement and proof · cited by 1
- CommRingCat.isRegularMono_of_faithfullyFlatstatement and proof · cited by 1
- AlgebraicGeometry.HasRingHomProperty.descendsAlong_flatstatement and proof · cited by 0