Documentation Verification Report

StandardSmooth

📁 Source: Mathlib/RingTheory/Smooth/StandardSmooth.lean

Statistics

Metric	Count
Definitions `IsStandardSmooth`, `relativeDimension`, `IsStandardSmoothOfRelativeDimension`	3
Theorems `baseChange`, `finitePresentation`, `localization_away`, `of_algEquiv`, `out`, `trans`, `baseChange`, `id`, `isStandardSmooth`, `localization_away`, `of_algEquiv`, `of_algebraMap_bijective`, `out`, `trans`, `isStandardSmooth`, `isStandardSmoothOfRelativeDimension`, `instIsStandardSmoothOfRelativeDimensionOfNatNatOfSubsingleton`, `instIsStandardSmoothOfSubsingleton`	18
Total	21

Algebra

Definitions

Name	Category	Theorems
`IsStandardSmooth` 📖	CompData	13 math math: `IsSmoothAt.exists_notMem_isStandardSmooth`, `IsStandardSmooth.of_basis_kaehlerDifferential`, `IsStandardSmooth.of_algEquiv`, `SubmersivePresentation.isStandardSmooth`, `IsStandardSmooth.baseChange`, `Smooth.exists_span_eq_top_isStandardSmooth`, `instIsStandardSmoothOfSubsingleton`, `RingHom.IsStandardSmooth.toAlgebra`, `IsStandardSmooth.localization_away`, `RingHom.isStandardSmooth_algebraMap`, `IsStandardSmooth.iff_exists_basis_kaehlerDifferential`, `IsStandardSmoothOfRelativeDimension.isStandardSmooth`, `IsStandardSmooth.trans`
`IsStandardSmoothOfRelativeDimension` 📖	CompData	13 math math: `IsStandardSmoothOfRelativeDimension.baseChange`, `IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth`, `RingHom.IsStandardSmoothOfRelativeDimension.toAlgebra`, `instIsStandardSmoothOfRelativeDimensionOfNatNatOfSubsingleton`, `SubmersivePresentation.isStandardSmoothOfRelativeDimension`, `IsStandardSmoothOfRelativeDimension.id`, `Etale.iff_isStandardSmoothOfRelativeDimension_zero`, `IsStandardSmoothOfRelativeDimension.trans`, `IsStandardSmoothOfRelativeDimension.of_algEquiv`, `IsStandardSmoothOfRelativeDimension.localization_away`, `RingHom.isStandardSmoothOfRelativeDimension_algebraMap`, `IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective`, `IsStandardSmoothOfRelativeDimension.exists_subalgebra_fg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsStandardSmoothOfRelativeDimensionOfNatNatOfSubsingleton` 📖	mathematical	—	`IsStandardSmoothOfRelativeDimension`	—	`Finite.of_fintype` `Nat.card_eq_fintype_card` `Fintype.card_unique` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub`
`instIsStandardSmoothOfSubsingleton` 📖	mathematical	—	`IsStandardSmooth`	—	`Finite.of_fintype`

Algebra.IsStandardSmooth

Definitions

Name	Category	Theorems
`relativeDimension` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baseChange` 📖	mathematical	—	`Algebra.IsStandardSmooth` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	—	`Algebra.to_smulCommClass`
`finitePresentation` 📖	mathematical	—	`Algebra.FinitePresentation` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`Algebra.Presentation.finitePresentation_of_isFinite`
`localization_away` 📖	mathematical	—	`Algebra.IsStandardSmooth`	—	`Finite.of_fintype`
`of_algEquiv` 📖	mathematical	—	`Algebra.IsStandardSmooth`	—	`Algebra.SubmersivePresentation.isStandardSmooth`
`out` 📖	mathematical	—	`Finite` `Algebra.SubmersivePresentation`	—	—
`trans` 📖	mathematical	—	`Algebra.IsStandardSmooth`	—	`Finite.instSum`

Algebra.IsStandardSmoothOfRelativeDimension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baseChange` 📖	mathematical	—	`Algebra.IsStandardSmoothOfRelativeDimension` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass`	—	`Algebra.to_smulCommClass`
`id` 📖	mathematical	—	`Algebra.IsStandardSmoothOfRelativeDimension` `Algebra.id` `CommRing.toCommSemiring`	—	`of_algebraMap_bijective` `Function.bijective_id`
`isStandardSmooth` 📖	mathematical	—	`Algebra.IsStandardSmooth`	—	`out`
`localization_away` 📖	mathematical	—	`Algebra.IsStandardSmoothOfRelativeDimension`	—	`Finite.of_fintype` `Algebra.Presentation.localizationAway_dimension_zero`
`of_algEquiv` 📖	mathematical	—	`Algebra.IsStandardSmoothOfRelativeDimension`	—	`Algebra.SubmersivePresentation.isStandardSmoothOfRelativeDimension`
`of_algebraMap_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	`Algebra.IsStandardSmoothOfRelativeDimension`	—	`Finite.of_fintype` `Algebra.Presentation.ofBijectiveAlgebraMap_dimension`
`out` 📖	mathematical	—	`Algebra.Presentation.dimension` `Algebra.PreSubmersivePresentation.toPresentation` `Algebra.SubmersivePresentation.toPreSubmersivePresentation`	—	—
`trans` 📖	mathematical	—	`Algebra.IsStandardSmoothOfRelativeDimension`	—	`Finite.instSum` `Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension`

Algebra.SubmersivePresentation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isStandardSmooth` 📖	mathematical	—	`Algebra.IsStandardSmooth`	—	`Finite.of_fintype`
`isStandardSmoothOfRelativeDimension` 📖	mathematical	`Algebra.Presentation.dimension` `Algebra.PreSubmersivePresentation.toPresentation` `toPreSubmersivePresentation`	`Algebra.IsStandardSmoothOfRelativeDimension`	—	`Finite.of_fintype` `Algebra.Presentation.dimension_reindex`

---

← Back to Index