Documentation Verification Report

SmoothFiber

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

Statistics

MetricCount
Definitions0
Theoremsof_smooth_fiberToSpecResidueField
1
Total1

AlgebraicGeometry.Smooth

Theorems

NameKindAssumesProvesValidatesDepends On
of_smooth_fiberToSpecResidueField 📖mathematicalAlgebraicGeometry.Smooth
AlgebraicGeometry.Scheme.Hom.fiber
AlgebraicGeometry.Spec
AlgebraicGeometry.Scheme.residueField
AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField		AlgebraicGeometry.Smooth—AlgebraicGeometry.Spec.map_surjective
AlgebraicGeometry.instHasRingHomPropertySmoothSmooth
Algebra.Smooth.of_formallySmooth_fiber
AlgebraicGeometry.Flat.instHasRingHomPropertyFlat
AlgebraicGeometry.instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation
Algebra.to_smulCommClass
RingHom.formallySmooth_algebraMap
RingHom.Smooth.formallySmooth
CommRingCat.hom_ofHom
AlgebraicGeometry.HasRingHomProperty.Spec_iff
PrimeSpectrum.isPrime
CategoryTheory.MorphismProperty.arrow_mk_iso_iff
CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects
AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource
AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover
AlgebraicGeometry.Scheme.Pullback.instHasPullback
AlgebraicGeometry.locallyOfFinitePresentation_comp
AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion
AlgebraicGeometry.Scheme.instIsOpenImmersionF
AlgebraicGeometry.Flat.comp
AlgebraicGeometry.Flat.instOfIsOpenImmersion
AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField.eq_1
CategoryTheory.Limits.hasPullbackHorizPaste
CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd
AlgebraicGeometry.smooth_comp
AlgebraicGeometry.instSmoothOfIsOpenImmersion
AlgebraicGeometry.IsOpenImmersion.of_isIso
CategoryTheory.Iso.isIso_inv
AlgebraicGeometry.instSmoothSndScheme
AlgebraicGeometry.Scheme.local_affine
AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange
AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion
AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange
AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover
AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtTarget
AlgebraicGeometry.instLocallyOfFinitePresentationSndScheme
AlgebraicGeometry.Flat.instSndScheme
CategoryTheory.MorphismProperty.of_isPullback
AlgebraicGeometry.smooth_isStableUnderBaseChange
CategoryTheory.CommSq.w
CategoryTheory.IsPullback.toCommSq
CategoryTheory.IsPullback.of_hasPullback
AlgebraicGeometry.isPullback_fiberToSpecResidueField_of_isPullback

---

← Back to Index