Smooth

📁 Source: Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

Statistics

Metric	Count
Definitions `IsSmooth`, `IsSmoothOfRelativeDimension`, `smoothLocus`, `Smooth`, `SmoothOfRelativeDimension`	5
Theorems `isSmooth`, `dense_smoothLocus_of_perfectField`, `genericPoint_mem_smoothLocus_of_perfectField`, `isOpen_smoothLocus`, `mem_smoothLocus`, `preimage_smoothLocus_eq`, `smoothLocus_eq_top`, `smoothLocus_eq_top_iff`, `smooth_appLE`, `exists_isStandardSmooth`, `iff_forall_exists_isStandardSmooth`, `smooth_appLE`, `exists_isStandardSmoothOfRelativeDimension`, `smooth`, `exists_smooth_of_formallySmooth_stalk`, `formallySmooth_stalkMap_iff`, `instFlatOfSmooth`, `instHasRingHomPropertySmoothOfRelativeDimensionLocallyIsStandardSmoothOfRelativeDimension`, `instHasRingHomPropertySmoothSmooth`, `instIsMultiplicativeSchemeSmoothOfRelativeDimensionOfNatNat`, `instIsReducedToScheme_1`, `instIsStableUnderCompositionSchemeSmooth`, `instLocallyOfFinitePresentationOfSmooth`, `instRespectsSchemeSmoothIsOpenImmersion`, `instSmoothFstScheme`, `instSmoothMorphismRestrict`, `instSmoothOfIsOpenImmersion`, `instSmoothOfRelativeDimensionOfNatNatCompScheme`, `instSmoothOfRelativeDimensionOfNatNatOfIsOpenImmersion`, `instSmoothResLE`, `instSmoothSndScheme`, `isSmoothOfRelativeDimension_isStableUnderBaseChange`, `isSmooth_isStableUnderBaseChange`, `smoothOfRelativeDimension_comp`, `smoothOfRelativeDimension_iff`, `smoothOfRelativeDimension_isStableUnderBaseChange`, `smooth_comp`, `smooth_iff`, `smooth_isStableUnderBaseChange`	39
Total	44

AlgebraicGeometry

Definitions

Name	Category	Theorems
`IsSmooth` 📖	MathDef	—
`IsSmoothOfRelativeDimension` 📖	MathDef	—
`Smooth` 📖	CompData	19 math math: `Scheme.Hom.smoothLocus_eq_top_iff`, `instIsStableUnderCompositionSchemeSmooth`, `isSmooth_isStableUnderBaseChange`, `IsSmoothOfRelativeDimension.isSmooth`, `smooth_of_grpObj_of_isAlgClosed`, `instSmoothOfIsOpenImmersion`, `smooth_comp`, `instSmoothResLE`, `smooth_isStableUnderBaseChange`, `smooth_iff`, `SmoothOfRelativeDimension.smooth`, `Smooth.of_smooth_fiberToSpecResidueField`, `instSmoothMorphismRestrict`, `instHasRingHomPropertySmoothSmooth`, `Etale.instSmooth`, `instRespectsSchemeSmoothIsOpenImmersion`, `instSmoothSndScheme`, `instSmoothFstScheme`, `Smooth.iff_forall_exists_isStandardSmooth`
`SmoothOfRelativeDimension` 📖	CompData	11 math math: `instSmoothOfRelativeDimensionOfNatNatCompScheme`, `instHasRingHomPropertySmoothOfRelativeDimensionLocallyIsStandardSmoothOfRelativeDimension`, `instSmoothOfRelativeDimensionOfNatNatOfIsOpenImmersion`, `Etale.instSmoothOfRelativeDimensionOfNatNat`, `smoothOfRelativeDimension_comp`, `smoothOfRelativeDimension_isStableUnderBaseChange`, `smoothOfRelativeDimension_iff`, `instIsMultiplicativeSchemeSmoothOfRelativeDimensionOfNatNat`, `Etale.iff_smoothOfRelativeDimension_zero`, `isSmoothOfRelativeDimension_isStableUnderBaseChange`, `Etale.eq_smoothOfRelativeDimension_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_smooth_of_formallySmooth_stalk` 📖	mathematical	—	`Scheme.Opens` `IsAffineOpen` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `RingHom.Smooth` `CommRingCat.carrier` `Opposite` `CategoryTheory.Category.opposite` `PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.appLE`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `Scheme.isBasis_affineOpens` `Set.mem_univ` `isOpen_univ` `IsOpen.preimage` `Scheme.Hom.continuous` `TopologicalSpace.Opens.is_open'` `Scheme.Hom.finitePresentation_appLE` `formallySmooth_stalkMap_iff` `Algebra.IsSmoothAt.exists_notMem_smooth` `PrimeSpectrum.isPrime` `IsAffineOpen.basicOpen` `LE.le.trans` `Scheme.basicOpen_le` `IsAffineOpen.toSpecΓ_fromSpec` `IsAffineOpen.isoSpec_hom` `Scheme.Hom.comp_apply` `Scheme.Hom.mem_preimage` `IsAffineOpen.fromSpec_preimage_basicOpen` `IsAffineOpen.primeIdealOf.eq_1` `PrimeSpectrum.mem_basicOpen` `IsAffineOpen.isLocalization_basicOpen` `Localization.isLocalization` `RingHom.ext` `IsScalarTower.algebraMap_apply` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `IsLocalization.map_eq` `RingHomCompTriple.comp_apply` `RingHomCompTriple.right_ids` `Scheme.Hom.appLE_map` `RingHom.PropertyIsLocal.respectsIso` `RingHom.Smooth.propertyIsLocal` `RingHom.smooth_algebraMap`
`formallySmooth_stalkMap_iff` 📖	mathematical	`Scheme.Opens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`RingHom.FormallySmooth` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `PresheafedSpace.carrier` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `PresheafedSpace.presheaf` `DFunLike.coe` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.stalkMap` `PrimeSpectrum` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `Scheme.Opens` `CommRing.toCommSemiring` `Set` `Set.instMembership` `Algebra.smoothLocus` `RingHom.toAlgebra` `Scheme.Hom.appLE` `IsAffineOpen.primeIdealOf` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`IsAffineOpen.comap_primeIdealOf_appLE` `CommRingCat.Colimits.hasColimits_commRingCat` `PrimeSpectrum.isPrime` `RingHom.formallySmooth_algebraMap` `RingHom.RespectsIso.arrow_mk_iso_iff` `RingHom.FormallySmooth.respectsIso` `Algebra.FormallySmooth.iff_restrictScalars` `Localization.AtPrime.instIsScalarTower` `IsScalarTower.left` `Algebra.FormallyEtale.instLocalization` `Algebra.Etale.formallyEtale` `Algebra.instEtaleOfIsStandardSmoothOfRelativeDimensionOfNatNat` `Algebra.IsStandardSmoothOfRelativeDimension.id`
`instFlatOfSmooth` 📖	mathematical	—	`Flat`	—	`RingHom.Smooth.flat` `Scheme.Hom.smooth_appLE`
`instHasRingHomPropertySmoothOfRelativeDimensionLocallyIsStandardSmoothOfRelativeDimension` 📖	mathematical	—	`HasRingHomProperty` `SmoothOfRelativeDimension` `RingHom.Locally` `RingHom.IsStandardSmoothOfRelativeDimension`	—	`HasRingHomProperty.locally_of_iff` `RingHom.LocalizationPreserves.away` `RingHom.isStandardSmoothOfRelativeDimension_localizationPreserves` `RingHom.isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway` `smoothOfRelativeDimension_iff`
`instHasRingHomPropertySmoothSmooth` 📖	mathematical	—	`HasRingHomProperty` `Smooth` `RingHom.Smooth`	—	`RingHom.Smooth.propertyIsLocal` `CategoryTheory.MorphismProperty.ext` `smooth_iff` `affineLocally_iff_forall_isAffineOpen`
`instIsMultiplicativeSchemeSmoothOfRelativeDimensionOfNatNat` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `Scheme` `Scheme.instCategory` `SmoothOfRelativeDimension`	—	`instSmoothOfRelativeDimensionOfNatNatOfIsOpenImmersion` `IsOpenImmersion.of_isIso` `CategoryTheory.IsIso.id` `instSmoothOfRelativeDimensionOfNatNatCompScheme`
`instIsReducedToScheme_1` 📖	mathematical	—	`IsReduced` `Scheme.Opens.toScheme`	—	`isReduced_of_isOpenImmersion` `Scheme.Opens.instIsOpenImmersionι`
`instIsStableUnderCompositionSchemeSmooth` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `Scheme` `Scheme.instCategory` `Smooth`	—	`HasRingHomProperty.stableUnderComposition` `instHasRingHomPropertySmoothSmooth` `RingHom.Smooth.stableUnderComposition`
`instLocallyOfFinitePresentationOfSmooth` 📖	mathematical	—	`LocallyOfFinitePresentation`	—	`HasRingHomProperty.eq_affineLocally` `instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation` `affineLocally_le` `RingHom.Smooth.finitePresentation` `instHasRingHomPropertySmoothSmooth`
`instRespectsSchemeSmoothIsOpenImmersion` 📖	mathematical	—	`CategoryTheory.MorphismProperty.Respects` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Smooth` `IsOpenImmersion`	—	`HasRingHomProperty.respects_isOpenImmersion` `instHasRingHomPropertySmoothSmooth` `RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway` `RingHom.Smooth.stableUnderComposition` `RingHom.Smooth.holdsForLocalizationAway`
`instSmoothFstScheme` 📖	mathematical	—	`Smooth` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.fst`	—	`CategoryTheory.MorphismProperty.pullback_fst` `Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `smooth_isStableUnderBaseChange`
`instSmoothMorphismRestrict` 📖	mathematical	—	`Smooth` `Scheme.Opens.toScheme` `CategoryTheory.Functor.obj` `Scheme.Opens` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.str` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `morphismRestrict`	—	`IsZariskiLocalAtTarget.restrict` `HasRingHomProperty.instIsZariskiLocalAtTarget` `instHasRingHomPropertySmoothSmooth`
`instSmoothOfIsOpenImmersion` 📖	mathematical	—	`Smooth`	—	`SmoothOfRelativeDimension.smooth` `instSmoothOfRelativeDimensionOfNatNatOfIsOpenImmersion`
`instSmoothOfRelativeDimensionOfNatNatCompScheme` 📖	mathematical	—	`SmoothOfRelativeDimension` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory`	—	—
`instSmoothOfRelativeDimensionOfNatNatOfIsOpenImmersion` 📖	mathematical	—	`SmoothOfRelativeDimension`	—	`HasRingHomProperty.of_isOpenImmersion` `instHasRingHomPropertySmoothOfRelativeDimensionLocallyIsStandardSmoothOfRelativeDimension` `RingHom.HoldsForLocalizationAway.containsIdentities` `RingHom.locally_holdsForLocalizationAway` `RingHom.isStandardSmoothOfRelativeDimension_holdsForLocalizationAway`
`instSmoothResLE` 📖	mathematical	`Scheme.Opens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	`Smooth` `Scheme.Opens.toScheme` `Scheme.Hom.resLE`	—	`smooth_comp` `instSmoothOfIsOpenImmersion` `instIsOpenImmersionHomOfLE` `instSmoothMorphismRestrict`
`instSmoothSndScheme` 📖	mathematical	—	`Smooth` `CategoryTheory.Limits.pullback` `Scheme` `Scheme.instCategory` `Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.MorphismProperty.pullback_snd` `Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `smooth_isStableUnderBaseChange`
`isSmoothOfRelativeDimension_isStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `Scheme` `Scheme.instCategory` `SmoothOfRelativeDimension`	—	`smoothOfRelativeDimension_isStableUnderBaseChange`
`isSmooth_isStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `Scheme` `Scheme.instCategory` `Smooth`	—	`smooth_isStableUnderBaseChange`
`smoothOfRelativeDimension_comp` 📖	mathematical	—	`SmoothOfRelativeDimension` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory`	—	`SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension` `exists_basicOpen_le_appLE_of_appLE_of_isAffine` `RingHom.isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway` `RingHom.LocalizationPreserves.away` `RingHom.isStandardSmoothOfRelativeDimension_localizationPreserves` `le_trans` `Scheme.Hom.preimage_mono` `Scheme.basicOpen_le` `RingHom.algebraMap_toAlgebra` `CommRingCat.ofHom_hom` `LE.le.trans` `Scheme.Hom.appLE_map_assoc` `Scheme.Hom.appLE_comp_appLE` `IsAffineOpen.basicOpen` `RingHom.IsStandardSmoothOfRelativeDimension.comp` `IsAffineOpen.isLocalization_basicOpen`
`smoothOfRelativeDimension_iff` 📖	mathematical	—	`SmoothOfRelativeDimension` `Scheme.Opens` `IsAffineOpen` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `RingHom.IsStandardSmoothOfRelativeDimension` `CommRingCat.carrier` `Opposite` `CategoryTheory.Category.opposite` `PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.appLE`	—	—
`smoothOfRelativeDimension_isStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `Scheme` `Scheme.instCategory` `SmoothOfRelativeDimension`	—	`HasRingHomProperty.isStableUnderBaseChange` `instHasRingHomPropertySmoothOfRelativeDimensionLocallyIsStandardSmoothOfRelativeDimension` `RingHom.locally_isStableUnderBaseChange` `RingHom.isStandardSmoothOfRelativeDimension_respectsIso` `RingHom.isStandardSmoothOfRelativeDimension_isStableUnderBaseChange`
`smooth_comp` 📖	mathematical	—	`Smooth` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory`	—	`CategoryTheory.MorphismProperty.comp_mem` `instIsStableUnderCompositionSchemeSmooth`
`smooth_iff` 📖	mathematical	—	`Smooth` `RingHom.Smooth` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `PresheafedSpace.presheaf` `Opposite.op` `Scheme.Opens` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.appLE`	—	—
`smooth_isStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `Scheme` `Scheme.instCategory` `Smooth`	—	`HasRingHomProperty.isStableUnderBaseChange` `instHasRingHomPropertySmoothSmooth` `RingHom.Smooth.isStableUnderBaseChange`

AlgebraicGeometry.IsSmoothOfRelativeDimension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSmooth` 📖	mathematical	—	`AlgebraicGeometry.Smooth`	—	`AlgebraicGeometry.SmoothOfRelativeDimension.smooth`

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
`smoothLocus` 📖	CompOp	6 math math: `smoothLocus_eq_top_iff`, `preimage_smoothLocus_eq`, `genericPoint_mem_smoothLocus_of_perfectField`, `mem_smoothLocus`, `dense_smoothLocus_of_perfectField`, `smoothLocus_eq_top`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dense_smoothLocus_of_perfectField` 📖	mathematical	—	`Dense` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.coe` `AlgebraicGeometry.Scheme.Opens` `TopologicalSpace.Opens.instSetLike` `smoothLocus` `AlgebraicGeometry.Spec` `CommRingCat.of` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`AlgebraicGeometry.LocallyOfFiniteType.isLocallyNoetherian` `AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation` `AlgebraicGeometry.instIsLocallyNoetherianSpecOfIsNoetherianRingCarrier` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `dense_iff_closure_eq` `Set.eq_univ_iff_forall` `Set.sUnion_eq_biUnion` `isOpen_compl_iff` `Set.Finite.isClosed_biUnion` `Set.Finite.diff` `TopologicalSpace.NoetherianSpace.finite_irreducibleComponents` `AlgebraicGeometry.IsNoetherian.noetherianSpace` `isClosed_of_mem_irreducibleComponents` `closure_sUnion_irreducibleComponents_diff_singleton` `irreducibleComponent_mem_irreducibleComponents` `isIrreducible_iff_irreducibleSpace` `isIrreducible_iff_closure` `isIrreducible_irreducibleComponent` `AlgebraicGeometry.isIntegral_of_irreducibleSpace_of_isReduced` `AlgebraicGeometry.instIsReducedToScheme_1` `AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat` `AlgebraicGeometry.irreducibleSpace_of_isIntegral` `AlgebraicGeometry.locallyOfFinitePresentation_comp` `AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι` `genericPoint_mem_smoothLocus_of_perfectField` `mem_preimage` `preimage_smoothLocus_eq` `Specializes.mem_closed` `IsGenericPoint.specializes` `IsGenericPoint.image` `genericPoint_spec` `continuous` `Set.image_univ` `AlgebraicGeometry.Scheme.Opens.range_ι` `mem_irreducibleComponent` `isClosed_closure` `subset_closure` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `AlgebraicGeometry.Scheme.isBasis_affineOpens` `Set.mem_univ` `isOpen_univ` `isCompact_iff_compactSpace` `AlgebraicGeometry.IsAffineOpen.isCompact` `AlgebraicGeometry.Scheme.Opens.ι_apply` `Set.mem_preimage` `IsOpenMap.preimage_closure_eq_closure_preimage` `Topology.IsOpenEmbedding.isOpenMap` `isOpenEmbedding` `coe_preimage`
`genericPoint_mem_smoothLocus_of_perfectField` 📖	mathematical	—	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `smoothLocus` `AlgebraicGeometry.Spec` `CommRingCat.of` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `genericPoint` `AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat` `AlgebraicGeometry.irreducibleSpace_of_isIntegral`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat` `AlgebraicGeometry.irreducibleSpace_of_isIntegral` `AlgebraicGeometry.LocallyOfFiniteType.stalkMap` `AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation` `mem_smoothLocus` `PrimeSpectrum.isPrime` `AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Algebra.IsAlgebraic.of_injective` `AlgEquiv.injective` `Algebra.IsSeparable.isAlgebraic` `EuclideanDomain.toNontrivial` `Algebra.isSeparable_self` `MulEquiv.isField` `Field.toIsField` `Algebra.IsAlgebraic.perfectField` `Algebra.FormallySmooth.of_perfectField`
`isOpen_smoothLocus` 📖	mathematical	—	`IsOpen` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `setOf` `RingHom.FormallySmooth` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.PresheafedSpace.presheaf` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `CommRingCat.commRing` `CommRingCat.Hom.hom` `stalkMap`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `isOpen_iff_forall_mem_open` `AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk` `AlgebraicGeometry.formallySmooth_stalkMap_iff` `Algebra.FormallySmooth.instLocalization` `Algebra.Smooth.formallySmooth` `RingHom.Smooth.toAlgebra` `TopologicalSpace.Opens.is_open'`
`mem_smoothLocus` 📖	mathematical	—	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `smoothLocus` `RingHom.FormallySmooth` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.PresheafedSpace.presheaf` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `CommRingCat.commRing` `CommRingCat.Hom.hom` `stalkMap`	—	—
`preimage_smoothLocus_eq` 📖	mathematical	—	`CategoryTheory.Functor.obj` `AlgebraicGeometry.Scheme.Opens` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `smoothLocus` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.locallyOfFinitePresentation_comp` `AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion`	—	`TopologicalSpace.Opens.ext` `AlgebraicGeometry.locallyOfFinitePresentation_comp` `AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion` `Set.ext` `CommRingCat.Colimits.hasColimits_commRingCat` `RingHom.RespectsIso.cancel_right_isIso` `RingHom.FormallySmooth.respectsIso` `AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap` `CommRingCat.hom_comp` `stalkMap_comp`
`smoothLocus_eq_top` 📖	mathematical	—	`smoothLocus` `AlgebraicGeometry.instLocallyOfFinitePresentationOfSmooth` `Top.top` `AlgebraicGeometry.Scheme.Opens` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`AlgebraicGeometry.instLocallyOfFinitePresentationOfSmooth` `top_le_iff` `TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open` `AlgebraicGeometry.Scheme.isBasis_affineOpens` `Set.mem_univ` `isOpen_univ` `IsOpen.preimage` `continuous` `TopologicalSpace.Opens.is_open'` `smooth_appLE` `CommRingCat.Colimits.hasColimits_commRingCat` `mem_smoothLocus` `AlgebraicGeometry.formallySmooth_stalkMap_iff` `Algebra.FormallySmooth.instLocalization` `Algebra.Smooth.formallySmooth` `RingHom.Smooth.toAlgebra`
`smoothLocus_eq_top_iff` 📖	mathematical	—	`smoothLocus` `Top.top` `AlgebraicGeometry.Scheme.Opens` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `AlgebraicGeometry.Smooth`	—	`AlgebraicGeometry.IsZariskiLocalAtSource.iff_exists_resLE` `AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource` `AlgebraicGeometry.instHasRingHomPropertySmoothSmooth` `AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtTarget` `CategoryTheory.MorphismProperty.Respects.toRespectsRight` `AlgebraicGeometry.instRespectsSchemeSmoothIsOpenImmersion` `AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk` `Eq.ge` `Set.mem_univ` `AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine` `RingHom.RespectsIso.arrow_mk_iso_iff` `RingHom.PropertyIsLocal.respectsIso` `RingHom.Smooth.propertyIsLocal` `smoothLocus_eq_top`
`smooth_appLE` 📖	mathematical	`AlgebraicGeometry.Scheme.Opens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'`	`RingHom.Smooth` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.Scheme.Opens` `CommRingCat.commRing` `CommRingCat.Hom.hom` `appLE`	—	`AlgebraicGeometry.Smooth.smooth_appLE`

AlgebraicGeometry.Smooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isStandardSmooth` 📖	mathematical	—	`AlgebraicGeometry.Scheme.Opens` `AlgebraicGeometry.IsAffineOpen` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `RingHom.IsStandardSmooth` `CommRingCat.carrier` `Opposite` `CategoryTheory.Category.opposite` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE`	—	`iff_forall_exists_isStandardSmooth`
`iff_forall_exists_isStandardSmooth` 📖	mathematical	—	`AlgebraicGeometry.Smooth` `AlgebraicGeometry.Scheme.Opens` `AlgebraicGeometry.IsAffineOpen` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `RingHom.IsStandardSmooth` `CommRingCat.carrier` `Opposite` `CategoryTheory.Category.opposite` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE`	—	`RingHom.smooth_iff_locally_isStandardSmooth` `AlgebraicGeometry.instHasRingHomPropertySmoothSmooth` `AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally` `RingHom.isStandardSmooth_stableUnderCompositionWithLocalizationAway` `RingHom.isStandardSmooth_respectsIso`
`smooth_appLE` 📖	mathematical	`AlgebraicGeometry.Scheme.Opens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'`	`RingHom.Smooth` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.Scheme.Opens` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE`	—	—

AlgebraicGeometry.SmoothOfRelativeDimension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isStandardSmoothOfRelativeDimension` 📖	mathematical	—	`AlgebraicGeometry.Scheme.Opens` `AlgebraicGeometry.IsAffineOpen` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `RingHom.IsStandardSmoothOfRelativeDimension` `CommRingCat.carrier` `Opposite` `CategoryTheory.Category.opposite` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE`	—	—
`smooth` 📖	mathematical	—	`AlgebraicGeometry.Smooth`	—	`AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth` `exists_isStandardSmoothOfRelativeDimension` `RingHom.IsStandardSmoothOfRelativeDimension.isStandardSmooth`

---

← Back to Index