Documentation Verification Report

FaithfullyFlat

📁 Source: Mathlib/RingTheory/RingHom/FaithfullyFlat.lean

Statistics

Metric	Count
Definitions `FaithfullyFlat`, `FaithfullyFlat`	2
Theorems `eq_and`, `flat`, `iff_flat_and_comap_surjective`, `injective`, `isStableUnderBaseChange`, `of_bijective`, `respectsIso`, `stableUnderComposition`, `faithfullyFlat_algebraMap_iff`	9
Total	11

Module

Definitions

Name	Category	Theorems
`FaithfullyFlat` 📖	CompData	21 math math: `FaithfullyFlat.instOfNontrivialOfFree`, `FaithfullyFlat.iff_exact_iff_lTensor_exact`, `FaithfullyFlat.finsupp`, `FaithfullyFlat.instTensorProduct`, `faithfullyFlat_iff`, `FaithfullyFlat.iff_zero_iff_rTensor_zero`, `FaithfullyFlat.of_comap_surjective`, `FaithfullyFlat.of_linearEquiv`, `FaithfullyFlat.iff_exact_iff_rTensor_exact`, `FaithfullyFlat.iff_zero_iff_lTensor_zero`, `FaithfullyFlat.iff_flat_and_ideal_smul_eq_top`, `FaithfullyFlat.iff_flat_and_lTensor_reflects_triviality`, `FaithfullyFlat.of_flat_of_isLocalHom`, `RingHom.faithfullyFlat_algebraMap_iff`, `FaithfullyFlat.self`, `FaithfullyFlat.iff_flat_and_rTensor_faithful`, `FaithfullyFlat.trans`, `FaithfullyFlat.iff_flat_and_lTensor_faithful`, `FaithfullyFlat.of_specComap_surjective`, `FaithfullyFlat.iff_flat_and_proper_ideal`, `FaithfullyFlat.iff_flat_and_rTensor_reflects_triviality`

RingHom

Definitions

Name	Category	Theorems
`FaithfullyFlat` 📖	MathDef	15 math math: `FaithfullyFlat.of_bijective`, `FaithfullyFlat.stableUnderComposition`, `FaithfullyFlat.isStableUnderBaseChange`, `AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine`, `FiniteType.codescendsAlong_faithfullyFlat`, `FaithfullyFlat.codescendsAlong_surjective`, `FaithfullyFlat.respectsIso`, `FaithfullyFlat.iff_flat_and_comap_surjective`, `faithfullyFlat_algebraMap_iff`, `AlgebraicGeometry.flat_and_surjective_SpecMap_iff`, `FinitePresentation.codescendsAlong_faithfullyFlat`, `FaithfullyFlat.eq_and`, `Finite.codescendsAlong_faithfullyFlat`, `FaithfullyFlat.codescendsAlong_bijective`, `FaithfullyFlat.codescendsAlong_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`faithfullyFlat_algebraMap_iff` 📖	mathematical	—	`FaithfullyFlat` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Module.FaithfullyFlat` `Ring.toAddCommGroup` `CommRing.toRing` `Algebra.toModule`	—	`Algebra.algebra_ext`

RingHom.FaithfullyFlat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_and` 📖	mathematical	—	`RingHom.FaithfullyFlat` `RingHom.Flat` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.comap`	—	`iff_flat_and_comap_surjective`
`flat` 📖	mathematical	—	`RingHom.Flat`	—	`Module.FaithfullyFlat.toFlat`
`iff_flat_and_comap_surjective` 📖	mathematical	—	`RingHom.FaithfullyFlat` `RingHom.Flat` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.comap`	—	`RingHom.algebraMap_toAlgebra` `RingHom.faithfullyFlat_algebraMap_iff` `RingHom.flat_algebraMap_iff` `Module.FaithfullyFlat.toFlat` `PrimeSpectrum.comap_surjective_of_faithfullyFlat` `Module.FaithfullyFlat.of_comap_surjective`
`injective` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	—	`FaithfulSMul.algebraMap_injective` `Module.FaithfullyFlat.faithfulSMul`
`isStableUnderBaseChange` 📖	mathematical	—	`RingHom.IsStableUnderBaseChange` `RingHom.FaithfullyFlat`	—	`respectsIso` `Algebra.to_smulCommClass` `RingHom.faithfullyFlat_algebraMap_iff` `Module.FaithfullyFlat.instTensorProduct`
`of_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`RingHom.FaithfullyFlat`	—	`iff_flat_and_comap_surjective` `RingHom.Flat.of_bijective` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `RingHom.ext` `RingEquiv.injective` `RingEquiv.apply_symm_apply` `PrimeSpectrum.comap_comp_apply` `PrimeSpectrum.comap_id`
`respectsIso` 📖	mathematical	—	`RingHom.RespectsIso` `RingHom.FaithfullyFlat`	—	`RingHom.StableUnderComposition.respectsIso` `stableUnderComposition` `of_bijective` `RingEquiv.bijective`
`stableUnderComposition` 📖	mathematical	—	`RingHom.StableUnderComposition` `RingHom.FaithfullyFlat`	—	`IsScalarTower.of_algebraMap_eq'` `RingHom.algebraMap_toAlgebra` `RingHom.faithfullyFlat_algebraMap_iff` `Module.FaithfullyFlat.trans`

---

← Back to Index