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	18 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, 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	—	TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike SheafedSpace.instTopologicalSpaceCarrierCarrier RingHom.Smooth CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder 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.Colimits.hasColimits_commRingCat PresheafedSpace.presheaf DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier CommRingCat.commRing CommRingCat.Hom.hom Scheme.Hom.stalkMap PrimeSpectrum Opposite CategoryTheory.Category.opposite Opposite.op CommRing.toCommSemiring Set Set.instMembership Algebra.smoothLocus RingHom.toAlgebra Scheme.Hom.appLE IsAffineOpen.primeIdealOf	—	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 Algebra.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	—	smoothOfRelativeDimension_comp
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 RingHom.IsStandardSmoothOfRelativeDimension 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	—	—
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 Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommRingCat.commRing CommRingCat.Hom.hom appLE	—	AlgebraicGeometry.Smooth.smooth_appLE

AlgebraicGeometry.Smooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isStandardSmooth 📖	mathematical	—	RingHom.IsStandardSmooth 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	—	iff_forall_exists_isStandardSmooth
iff_forall_exists_isStandardSmooth 📖	mathematical	—	AlgebraicGeometry.Smooth RingHom.IsStandardSmooth 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	—	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 Opposite CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommRingCat.commRing CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.appLE	—	—

AlgebraicGeometry.SmoothOfRelativeDimension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isStandardSmoothOfRelativeDimension 📖	mathematical	—	RingHom.IsStandardSmoothOfRelativeDimension 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	—	—
smooth 📖	mathematical	—	AlgebraicGeometry.Smooth	—	AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth exists_isStandardSmoothOfRelativeDimension RingHom.IsStandardSmoothOfRelativeDimension.isStandardSmooth

---

← Back to Index