Documentation Verification Report

Descent

📁 Source: Mathlib/RingTheory/Finiteness/Descent.lean

Statistics

Metric	Count
Definitions	0
Theorems `of_finitePresentation_tensorProduct_of_faithfullyFlat`, `of_finiteType_tensorProduct_of_faithfullyFlat`, `of_FG_map_of_faithfullyFlat`, `of_finite_tensorProduct_of_faithfullyFlat`, `codescendsAlong_faithfullyFlat`, `codescendsAlong_faithfullyFlat`, `codescendsAlong_faithfullyFlat`	7
Total	7

Algebra.FinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_finitePresentation_tensorProduct_of_faithfullyFlat` 📖	mathematical	—	`Algebra.FinitePresentation` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`Algebra.to_smulCommClass` `Algebra.FiniteType.of_finiteType_tensorProduct_of_faithfullyFlat` `Algebra.FiniteType.of_finitePresentation` `Algebra.FiniteType.iff_quotient_mvPolynomial''` `Module.FaithfullyFlat.of_linearEquiv` `Module.FaithfullyFlat.instTensorProduct` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `of_surjective` `Ideal.FG.of_FG_map_of_faithfullyFlat` `RingHom.instRingHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsScalarTower.left` `Algebra.TensorProduct.lTensor_ker` `ker_fG_of_surjective` `Algebra.FiniteType.baseChangeAux_surj` `baseChange` `mvPolynomial` `self` `Finite.of_fintype`

Algebra.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_finiteType_tensorProduct_of_faithfullyFlat` 📖	mathematical	—	`Algebra.FiniteType` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`Algebra.to_smulCommClass` `out` `TensorProduct.exists_sum_tmul_eq` `of_surjective` `instMvPolynomialOfFinite` `Finite.instSigma` `Finite.of_fintype` `of_finitePresentation` `Algebra.FinitePresentation.self` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `AlgHom.range_eq_top` `eq_top_iff` `Algebra.adjoin_le_iff` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Finset.sum_congr` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `MvPolynomial.aeval_X` `Module.FaithfullyFlat.lTensor_surjective_iff_surjective`

Ideal.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_FG_map_of_faithfullyFlat` 📖	—	`Ideal.FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	—	`Module.Finite.iff_fg` `Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `RingHomCompTriple.ids` `RingHomInvPair.ids` `smulCommClass_self` `TensorProduct.smulCommClass_left` `IsScalarTower.to_smulCommClass'` `EquivLike.toEmbeddingLike` `RingHomSurjective.ids` `le_antisymm` `RingHom.instRingHomClass` `Ideal.map_le_iff_le_comap` `Algebra.smul_def` `mul_one` `TensorProduct.induction_on` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Algebra.mul_smul_comm` `Ideal.mul_mem_left` `Ideal.mem_map_of_mem` `map_add` `SemilinearMapClass.toAddHomClass` `RingHomSurjective.invPair` `Module.Finite.equiv_iff` `Module.Finite.of_finite_tensorProduct_of_faithfullyFlat`

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_finite_tensorProduct_of_faithfullyFlat` 📖	mathematical	—	`Module.Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Algebra.to_smulCommClass` `exists_fin` `RingHomInvPair.ids` `smulCommClass_self` `Finite.instSigma` `Finite.of_fintype` `of_surjective` `RingHomSurjective.ids` `pi` `self` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `TensorProduct.smulCommClass_left` `IsScalarTower.to_smulCommClass'` `LinearMap.range_eq_top` `eq_top_iff` `Submodule.span_le` `Set.range_subset_iff` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_congr` `Module.Basis.constr_apply_fintype` `Module.Basis.equivFun_self` `ite_smul` `one_smul` `zero_smul` `Finset.sum_ite_eq` `Module.FaithfullyFlat.lTensor_surjective_iff_surjective` `TensorProduct.exists_sum_tmul_eq`

RingHom.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codescendsAlong_faithfullyFlat` 📖	mathematical	—	`RingHom.CodescendsAlong` `RingHom.Finite` `RingHom.FaithfullyFlat`	—	`RingHom.finite_respectsIso` `Algebra.to_smulCommClass` `RingHom.finite_algebraMap` `Module.Finite.of_finite_tensorProduct_of_faithfullyFlat` `RingHom.faithfullyFlat_algebraMap_iff`

RingHom.FinitePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codescendsAlong_faithfullyFlat` 📖	mathematical	—	`RingHom.CodescendsAlong` `RingHom.FinitePresentation` `RingHom.FaithfullyFlat`	—	`RingHom.finitePresentation_respectsIso` `Algebra.to_smulCommClass` `RingHom.finitePresentation_algebraMap` `Algebra.FinitePresentation.of_finitePresentation_tensorProduct_of_faithfullyFlat` `RingHom.faithfullyFlat_algebraMap_iff`

RingHom.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codescendsAlong_faithfullyFlat` 📖	mathematical	—	`RingHom.CodescendsAlong` `RingHom.FiniteType` `RingHom.FaithfullyFlat`	—	`RingHom.finiteType_respectsIso` `Algebra.to_smulCommClass` `RingHom.finiteType_algebraMap` `Algebra.FiniteType.of_finiteType_tensorProduct_of_faithfullyFlat` `RingHom.faithfullyFlat_algebraMap_iff`

---

← Back to Index