Documentation Verification Report

Flat

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

Statistics

Metric	Count
Definitions `Flat`	1
Theorems `inl_injective_of_flat`, `inr_injective_of_flat`, `comp`, `containsIdentities`, `generalizingMap_comap`, `holdsForLocalizationAway`, `id`, `isStableUnderBaseChange`, `localRingHom`, `ofLocalizationPrime`, `ofLocalizationSpanTarget`, `of_bijective`, `of_isField`, `propertyIsLocal`, `respectsIso`, `stableUnderComposition`, `flat_algebraMap_iff`	17
Total	18

CommRingCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inl_injective_of_flat` 📖	mathematical	`carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CommRingCat` `instCategory` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier`	`CategoryTheory.Limits.pushout` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `Colimits.hasColimits_commRingCat` `CategoryTheory.Limits.span` `CategoryTheory.Limits.pushout.inl`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `Colimits.hasColimits_commRingCat` `isPushout_tensorProduct` `CategoryTheory.IsPushout.inl_isoPushout_hom` `RingEquiv.injective` `Algebra.TensorProduct.includeLeft_injective` `smulCommClass_self`
`inr_injective_of_flat` 📖	mathematical	`carrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CommRingCat` `instCategory` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `RingHom.instFunLike` `instConcreteCategoryRingHomCarrier`	`CategoryTheory.Limits.pushout` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.WalkingSpan` `CategoryTheory.Limits.WidePushoutShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `Colimits.hasColimits_commRingCat` `CategoryTheory.Limits.span` `CategoryTheory.Limits.pushout.inr`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `Colimits.hasColimits_commRingCat` `isPushout_tensorProduct` `CategoryTheory.IsPushout.inr_isoPushout_hom` `RingEquiv.injective` `Algebra.TensorProduct.includeRight_injective`

RingHom

Definitions

Name	Category	Theorems
`Flat` 📖	MathDef	25 math math: `Flat.isStableUnderBaseChange`, `Smooth.flat`, `Flat.comp`, `AlgebraicGeometry.Flat.instHasRingHomPropertyFlat`, `FaithfullyFlat.flat`, `Flat.of_isField`, `Flat.respectsIso`, `AlgebraicGeometry.Flat.flat_of_affine_subset`, `AlgebraicGeometry.Flat.flat_appLE`, `AlgebraicGeometry.Flat.stalkMap`, `Flat.ofLocalizationPrime`, `FaithfullyFlat.iff_flat_and_comap_surjective`, `Flat.localRingHom`, `Flat.id`, `Flat.propertyIsLocal`, `AlgebraicGeometry.Flat.iff_flat_stalkMap`, `flat_algebraMap_iff`, `Flat.ofLocalizationSpanTarget`, `Flat.holdsForLocalizationAway`, `Flat.stableUnderComposition`, `AlgebraicGeometry.Scheme.Hom.flat_appLE`, `FaithfullyFlat.eq_and`, `Flat.containsIdentities`, `Flat.of_bijective`, `AlgebraicGeometry.flat_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flat_algebraMap_iff` 📖	mathematical	—	`Flat` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Module.Flat` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`Flat.eq_1` `toAlgebra_algebraMap`

RingHom.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`RingHom.Flat` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsScalarTower.of_algebraMap_eq'` `Module.Flat.trans`
`containsIdentities` 📖	mathematical	—	`RingHom.ContainsIdentities` `RingHom.Flat`	—	`id`
`generalizingMap_comap` 📖	mathematical	—	`GeneralizingMap` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.zariskiTopology` `PrimeSpectrum.comap`	—	`Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap` `Algebra.HasGoingDown.of_flat`
`holdsForLocalizationAway` 📖	mathematical	—	`RingHom.HoldsForLocalizationAway` `RingHom.Flat`	—	`IsLocalization.flat` `eq_1` `IsScalarTower.Algebra.ext` `Algebra.smul_def`
`id` 📖	mathematical	—	`RingHom.Flat` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Module.Flat.self`
`isStableUnderBaseChange` 📖	mathematical	—	`RingHom.IsStableUnderBaseChange` `RingHom.Flat`	—	`respectsIso` `Algebra.to_smulCommClass` `RingHom.flat_algebraMap_iff` `Module.Flat.baseChange`
`localRingHom` 📖	mathematical	`Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass`	`RingHom.Flat` `Localization.AtPrime` `OreLocalization.instCommRing` `Ideal.primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Localization.localRingHom`	—	`RingHom.instRingHomClass` `IsScalarTower.right` `IsScalarTower.of_algebraMap_eq` `Localization.localRingHom_to_map` `eq_1` `Module.flat_iff_of_isLocalization` `Localization.isLocalization` `Module.Flat.trans` `OreLocalization.instIsScalarTower` `Localization.flat` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.self`
`ofLocalizationPrime` 📖	mathematical	—	`RingHom.OfLocalizationPrime` `RingHom.Flat`	—	`eq_1` `Module.flat_of_isLocalized_maximal` `IsScalarTower.right` `Ideal.IsMaximal.isPrime'` `OreLocalization.instIsScalarTower` `instIsLocalizedModuleLinearMapOfIsLocalization` `Localization.isLocalization` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `IsScalarTower.of_algebraMap_eq` `Localization.localRingHom_to_map` `Module.Flat.trans` `Localization.flat` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.self`
`ofLocalizationSpanTarget` 📖	mathematical	—	`RingHom.OfLocalizationSpanTarget` `RingHom.Flat`	—	`Module.flat_of_isLocalized_span` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `instIsLocalizedModuleLinearMapOfIsLocalization` `Localization.isLocalization` `Module.ext` `Algebra.smul_def`
`of_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`RingHom.Flat`	—	`Module.Flat.of_linearEquiv` `Module.FaithfullyFlat.toFlat` `Module.FaithfullyFlat.self` `RingHomInvPair.ids`
`of_isField` 📖	mathematical	`IsField` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`RingHom.Flat`	—	`RingHom.algebraMap_toAlgebra` `RingHom.flat_algebraMap_iff` `Module.Flat.of_free` `Module.Free.of_divisionRing`
`propertyIsLocal` 📖	mathematical	—	`RingHom.PropertyIsLocal` `RingHom.Flat`	—	`RingHom.LocalizationPreserves.away` `RingHom.IsStableUnderBaseChange.localizationPreserves` `isStableUnderBaseChange` `ofLocalizationSpanTarget` `RingHom.OfLocalizationSpanTarget.ofLocalizationSpan` `RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway` `stableUnderComposition` `holdsForLocalizationAway`
`respectsIso` 📖	mathematical	—	`RingHom.RespectsIso` `RingHom.Flat`	—	`RingHom.StableUnderComposition.respectsIso` `stableUnderComposition` `of_bijective` `RingEquiv.bijective`
`stableUnderComposition` 📖	mathematical	—	`RingHom.StableUnderComposition` `RingHom.Flat`	—	`comp`

---

← Back to Index