Documentation Verification Report

StandardSmooth

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

Statistics

Metric	Count
Definitions `IsStandardSmooth`, `IsStandardSmoothOfRelativeDimension`	2
Theorems `exists_etale_mvPolynomial`, `comp`, `exists_etale_mvPolynomial`, `toAlgebra`, `algebraMap_isLocalizationAway`, `comp`, `equiv`, `exists_etale_mvPolynomial`, `id`, `isStandardSmooth`, `toAlgebra`, `isStandardSmoothOfRelativeDimension_algebraMap`, `isStandardSmoothOfRelativeDimension_holdsForLocalizationAway`, `isStandardSmoothOfRelativeDimension_isStableUnderBaseChange`, `isStandardSmoothOfRelativeDimension_localizationPreserves`, `isStandardSmoothOfRelativeDimension_respectsIso`, `isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway`, `isStandardSmooth_algebraMap`, `isStandardSmooth_holdsForLocalizationAway`, `isStandardSmooth_isStableUnderBaseChange`, `isStandardSmooth_localizationPreserves`, `isStandardSmooth_respectsIso`, `isStandardSmooth_stableUnderComposition`, `isStandardSmooth_stableUnderCompositionWithLocalizationAway`	24
Total	26

Algebra.IsStandardSmoothOfRelativeDimension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_etale_mvPolynomial` 📖	mathematical	—	`RingHom.Etale` `MvPolynomial` `CommRing.toCommSemiring` `MvPolynomial.instCommRingMvPolynomial` `AlgHom.toRingHom` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id`	—	`out` `Subtype.finite` `Nat.card_coe_set_eq` `Set.ncard_compl` `Set.toFinite` `Set.ncard_range_of_injective` `Algebra.Presentation.dimension.eq_1` `MvPolynomial.isScalarTower` `IsScalarTower.right` `IsScalarTower.of_algebraMap_eq'` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `IsScalarTower.to₁₂₄` `Algebra.Generators.instIsScalarTowerRing` `IsScalarTower.left` `MvPolynomial.ringHom_ext'` `RingHom.ext` `MvPolynomial.iterToSum_X` `MvPolynomial.rename_X` `Algebra.Generators.algebraMap_apply` `MvPolynomial.aeval_X` `MvPolynomial.algHom_C` `MvPolynomial.iterToSum_C_C` `IsScalarTower.algebraMap_eq` `MvPolynomial.iterToSum_C_X` `Algebra.Generators.algebraMap_surjective` `AlgEquiv.surjective` `Set.range_comp` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.coe_ringEquiv` `AlgEquiv.symm_toRingEquiv` `Ideal.map_span` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Algebra.Presentation.span_range_relation_eq_ker` `Ideal.map_symm` `RingHom.instRingHomClass` `Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det` `RingHom.map_det` `Matrix.ext` `Algebra.PreSubmersivePresentation.jacobiMatrix_apply` `MvPolynomial.pderiv_sumToIter` `MvPolynomial.iterToSum_sumToIter` `MvPolynomial.pderiv_rename` `Equiv.injective` `MvPolynomial.rename_rename` `Equiv.self_comp_symm` `MvPolynomial.rename_id` `Algebra.SubmersivePresentation.jacobian_isUnit` `RingHom.etale_algebraMap` `Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero` `Nat.card_eq_fintype_card` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub`

RingHom

Definitions

Name	Category	Theorems
`IsStandardSmooth` 📖	MathDef	13 math math: `IsStandardSmooth.comp`, `isStandardSmooth_stableUnderComposition`, `isStandardSmooth_localizationPreserves`, `isStandardSmooth_respectsIso`, `isStandardSmooth_holdsForLocalizationAway`, `smooth_iff_locally_isStandardSmooth`, `isStandardSmooth_algebraMap`, `isStandardSmooth_isStableUnderBaseChange`, `AlgebraicGeometry.Smooth.exists_isStandardSmooth`, `Smooth.locally_isStandardSmooth`, `IsStandardSmoothOfRelativeDimension.isStandardSmooth`, `isStandardSmooth_stableUnderCompositionWithLocalizationAway`, `AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth`
`IsStandardSmoothOfRelativeDimension` 📖	MathDef	14 math math: `IsStandardSmoothOfRelativeDimension.equiv`, `isStandardSmoothOfRelativeDimension_localizationPreserves`, `AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension`, `etale_iff_isStandardSmoothOfRelativeDimension_zero`, `AlgebraicGeometry.instHasRingHomPropertySmoothOfRelativeDimensionLocallyIsStandardSmoothOfRelativeDimension`, `IsStandardSmoothOfRelativeDimension.id`, `isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway`, `isStandardSmoothOfRelativeDimension_algebraMap`, `IsStandardSmoothOfRelativeDimension.comp`, `isStandardSmoothOfRelativeDimension_respectsIso`, `AlgebraicGeometry.smoothOfRelativeDimension_iff`, `isStandardSmoothOfRelativeDimension_isStableUnderBaseChange`, `isStandardSmoothOfRelativeDimension_holdsForLocalizationAway`, `IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isStandardSmoothOfRelativeDimension_algebraMap` 📖	mathematical	—	`IsStandardSmoothOfRelativeDimension` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.IsStandardSmoothOfRelativeDimension`	—	`IsStandardSmoothOfRelativeDimension.eq_1` `toAlgebra_algebraMap`
`isStandardSmoothOfRelativeDimension_holdsForLocalizationAway` 📖	mathematical	—	`HoldsForLocalizationAway` `IsStandardSmoothOfRelativeDimension`	—	`IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway`
`isStandardSmoothOfRelativeDimension_isStableUnderBaseChange` 📖	mathematical	—	`IsStableUnderBaseChange` `IsStandardSmoothOfRelativeDimension`	—	`isStandardSmoothOfRelativeDimension_respectsIso` `IsScalarTower.Algebra.ext` `Algebra.smul_def` `IsStandardSmoothOfRelativeDimension.eq_1` `Algebra.to_smulCommClass` `Algebra.IsStandardSmoothOfRelativeDimension.baseChange`
`isStandardSmoothOfRelativeDimension_localizationPreserves` 📖	mathematical	—	`LocalizationPreserves` `IsStandardSmoothOfRelativeDimension`	—	`IsStableUnderBaseChange.localizationPreserves` `isStandardSmoothOfRelativeDimension_isStableUnderBaseChange`
`isStandardSmoothOfRelativeDimension_respectsIso` 📖	mathematical	—	`RespectsIso` `IsStandardSmoothOfRelativeDimension`	—	`zero_add` `IsStandardSmoothOfRelativeDimension.comp` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `IsStandardSmoothOfRelativeDimension.equiv` `add_zero`
`isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway` 📖	mathematical	—	`StableUnderCompositionWithLocalizationAway` `IsStandardSmoothOfRelativeDimension`	—	`IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway` `IsStandardSmoothOfRelativeDimension.comp` `add_zero` `zero_add`
`isStandardSmooth_algebraMap` 📖	mathematical	—	`IsStandardSmooth` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.IsStandardSmooth`	—	`IsStandardSmooth.eq_1` `toAlgebra_algebraMap`
`isStandardSmooth_holdsForLocalizationAway` 📖	mathematical	—	`HoldsForLocalizationAway` `IsStandardSmooth`	—	`IsStandardSmoothOfRelativeDimension.isStandardSmooth` `IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway`
`isStandardSmooth_isStableUnderBaseChange` 📖	mathematical	—	`IsStableUnderBaseChange` `IsStandardSmooth`	—	`isStandardSmooth_respectsIso` `IsScalarTower.Algebra.ext` `Algebra.smul_def` `IsStandardSmooth.eq_1` `Algebra.to_smulCommClass` `Algebra.IsStandardSmooth.baseChange`
`isStandardSmooth_localizationPreserves` 📖	mathematical	—	`LocalizationPreserves` `IsStandardSmooth`	—	`IsStableUnderBaseChange.localizationPreserves` `isStandardSmooth_isStableUnderBaseChange`
`isStandardSmooth_respectsIso` 📖	mathematical	—	`RespectsIso` `IsStandardSmooth`	—	`StableUnderComposition.respectsIso` `isStandardSmooth_stableUnderComposition` `IsStandardSmoothOfRelativeDimension.isStandardSmooth` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `IsStandardSmoothOfRelativeDimension.equiv`
`isStandardSmooth_stableUnderComposition` 📖	mathematical	—	`StableUnderComposition` `IsStandardSmooth`	—	`IsStandardSmooth.comp`
`isStandardSmooth_stableUnderCompositionWithLocalizationAway` 📖	mathematical	—	`StableUnderCompositionWithLocalizationAway` `IsStandardSmooth`	—	`StableUnderComposition.stableUnderCompositionWithLocalizationAway` `isStandardSmooth_stableUnderComposition` `isStandardSmooth_holdsForLocalizationAway`

RingHom.IsStandardSmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`RingHom.IsStandardSmooth` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`eq_1` `IsScalarTower.of_algebraMap_eq'` `Algebra.IsStandardSmooth.trans` `toAlgebra`
`exists_etale_mvPolynomial` 📖	mathematical	—	`RingHom.comp` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.C` `RingHom.Etale` `MvPolynomial.instCommRingMvPolynomial`	—	`RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial`
`toAlgebra` 📖	mathematical	—	`Algebra.IsStandardSmooth` `RingHom.toAlgebra` `CommRing.toCommSemiring`	—	—

RingHom.IsStandardSmoothOfRelativeDimension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_isLocalizationAway` 📖	mathematical	—	`RingHom.IsStandardSmoothOfRelativeDimension` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`IsScalarTower.Algebra.ext` `Algebra.smul_def` `eq_1` `Algebra.IsStandardSmoothOfRelativeDimension.localization_away`
`comp` 📖	mathematical	—	`RingHom.IsStandardSmoothOfRelativeDimension` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`eq_1` `IsScalarTower.of_algebraMap_eq'` `Algebra.IsStandardSmoothOfRelativeDimension.trans` `toAlgebra`
`equiv` 📖	mathematical	—	`RingHom.IsStandardSmoothOfRelativeDimension` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`	—	`Algebra.IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.bijective`
`exists_etale_mvPolynomial` 📖	mathematical	—	`RingHom.comp` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.C` `RingHom.Etale` `MvPolynomial.instCommRingMvPolynomial`	—	`Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial` `toAlgebra` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap`
`id` 📖	mathematical	—	`RingHom.IsStandardSmoothOfRelativeDimension` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Algebra.IsStandardSmoothOfRelativeDimension.id`
`isStandardSmooth` 📖	mathematical	—	`RingHom.IsStandardSmooth`	—	`Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth` `toAlgebra`
`toAlgebra` 📖	mathematical	—	`Algebra.IsStandardSmoothOfRelativeDimension` `RingHom.toAlgebra` `CommRing.toCommSemiring`	—	—

---

← Back to Index