Documentation Verification Report

ValuativeCriterion

📁 Source: Mathlib/AlgebraicGeometry/ValuativeCriterion.lean

Statistics

Metric	Count
Definitions `ValuativeCommSq`, `K`, `R`, `algebra`, `commRing`, `i₁`, `i₂`, `ValuativeCriterion`, `Existence`	9
Theorems `eq_valuativeCriterion`, `of_valuativeCriterion`, `eq_valuativeCriterion`, `of_valuativeCriterion`, `valuativeCriterion`, `eq_valuativeCriterion`, `of_valuativeCriterion`, `commSq`, `domain`, `isFractionRing`, `valuationRing`, `eq`, `instIsLocalHomCarrierRingHomHomHomCommRingCat`, `of_specializingMap`, `specializingMap`, `stableUnderBaseChange`, `eq`, `existence`, `iff`, `uniqueness`	20
Total	29

AlgebraicGeometry

Definitions

Name	Category	Theorems
`ValuativeCommSq` 📖	CompData	—
`ValuativeCriterion` 📖	CompOp	3 math math: `ValuativeCriterion.iff`, `IsProper.eq_valuativeCriterion`, `ValuativeCriterion.eq`

AlgebraicGeometry.IsProper

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_valuativeCriterion` 📖	mathematical	—	`AlgebraicGeometry.IsProper` `CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `AlgebraicGeometry.ValuativeCriterion` `AlgebraicGeometry.QuasiCompact` `AlgebraicGeometry.QuasiSeparated` `AlgebraicGeometry.LocallyOfFiniteType`	—	`AlgebraicGeometry.isProper_eq` `AlgebraicGeometry.IsSeparated.eq_valuativeCriterion` `AlgebraicGeometry.ValuativeCriterion.eq` `AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion` `inf_assoc`
`of_valuativeCriterion` 📖	mathematical	`AlgebraicGeometry.ValuativeCriterion`	`AlgebraicGeometry.IsProper`	—	`eq_valuativeCriterion`

AlgebraicGeometry.IsSeparated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_valuativeCriterion` 📖	mathematical	—	`AlgebraicGeometry.IsSeparated` `CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `AlgebraicGeometry.ValuativeCriterion.Uniqueness` `AlgebraicGeometry.QuasiSeparated`	—	`valuativeCriterion` `instQuasiSeparated` `of_valuativeCriterion`
`of_valuativeCriterion` 📖	mathematical	`AlgebraicGeometry.ValuativeCriterion.Uniqueness`	`AlgebraicGeometry.IsSeparated`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.CommSq.w_assoc` `AlgebraicGeometry.ValuativeCommSq.commSq` `CategoryTheory.Limits.pullback.diagonal_fst_assoc` `AlgebraicGeometry.ValuativeCommSq.domain` `AlgebraicGeometry.ValuativeCommSq.valuationRing` `AlgebraicGeometry.ValuativeCommSq.isFractionRing` `CategoryTheory.Limits.pullback.diagonal_fst` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.pullback.diagonal_snd` `CategoryTheory.Limits.pullback.condition` `CategoryTheory.IsPullback.hom_ext` `CategoryTheory.IsPullback.of_hasPullback` `AlgebraicGeometry.UniversallyClosed.of_valuativeCriterion` `AlgebraicGeometry.QuasiSeparated.quasiCompact_diagonal` `AlgebraicGeometry.IsClosedImmersion.of_isPreimmersion` `AlgebraicGeometry.IsImmersion.toIsPreimmersion` `AlgebraicGeometry.IsImmersion.instDiagonalScheme` `IsClosedMap.isClosed_range` `AlgebraicGeometry.Scheme.Hom.isClosedMap`
`valuativeCriterion` 📖	mathematical	—	`AlgebraicGeometry.ValuativeCriterion.Uniqueness`	—	`AlgebraicGeometry.ValuativeCommSq.commSq` `CategoryTheory.CommSq.LiftStruct.ext` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.pullback_snd` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange` `diagonal_isClosedImmersion` `AlgebraicGeometry.HasAffineProperty.iff_of_isAffine` `AlgebraicGeometry.IsClosedImmersion.hasAffineProperty` `AlgebraicGeometry.isAffine_Spec` `CategoryTheory.IsPullback.hom_ext` `CategoryTheory.IsPullback.of_hasPullback` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.pullback.diagonal_fst` `CategoryTheory.Category.comp_id` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Limits.pullback.diagonal_snd` `CategoryTheory.Limits.pullback.lift_snd` `RingHom.toMorphismProperty_respectsIso_iff` `RingHom.injective_respectsIso` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `FaithfulSMul.algebraMap_injective` `IsFractionRing.instFaithfulSMul` `AlgebraicGeometry.ValuativeCommSq.isFractionRing` `Function.Injective.of_comp` `AlgebraicGeometry.Scheme.Hom.comp_appTop` `AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop` `CategoryTheory.ConcreteCategory.isIso_iff_bijective` `CommRingCat.forgetReflectIsos` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Limits.pullback.lift_fst` `CategoryTheory.Limits.pullback.condition_assoc`

AlgebraicGeometry.UniversallyClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_valuativeCriterion` 📖	mathematical	—	`AlgebraicGeometry.UniversallyClosed` `CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `AlgebraicGeometry.ValuativeCriterion.Existence` `AlgebraicGeometry.QuasiCompact`	—	`AlgebraicGeometry.universallyClosed_eq_universallySpecializing` `AlgebraicGeometry.ValuativeCriterion.Existence.eq`
`of_valuativeCriterion` 📖	mathematical	`AlgebraicGeometry.ValuativeCriterion.Existence`	`AlgebraicGeometry.UniversallyClosed`	—	`eq_valuativeCriterion`

AlgebraicGeometry.ValuativeCommSq

Definitions

Name	Category	Theorems
`K` 📖	CompOp	2 math math: `isFractionRing`, `commSq`
`R` 📖	CompOp	4 math math: `isFractionRing`, `valuationRing`, `commSq`, `domain`
`algebra` 📖	CompOp	2 math math: `isFractionRing`, `commSq`
`commRing` 📖	CompOp	4 math math: `isFractionRing`, `valuationRing`, `commSq`, `domain`
`i₁` 📖	CompOp	1 math math: `commSq`
`i₂` 📖	CompOp	1 math math: `commSq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commSq` 📖	mathematical	—	`CategoryTheory.CommSq` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Spec` `CommRingCat.of` `K` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `field` `R` `commRing` `i₁` `AlgebraicGeometry.Spec.map` `CommRingCat.ofHom` `algebraMap` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `algebra` `i₂`	—	—
`domain` 📖	mathematical	—	`IsDomain` `R` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing`	—	—
`isFractionRing` 📖	mathematical	—	`IsFractionRing` `R` `CommRing.toCommSemiring` `commRing` `K` `Semifield.toCommSemiring` `Field.toSemifield` `field` `algebra`	—	—
`valuationRing` 📖	mathematical	—	`ValuationRing` `R` `commRing` `domain`	—	—

AlgebraicGeometry.ValuativeCriterion

Definitions

Name	Category	Theorems
`Existence` 📖	CompOp	8 math math: `iff`, `AlgebraicGeometry.Proj.valuativeCriterion_existence`, `Existence.eq`, `Existence.stableUnderBaseChange`, `Existence.of_specializingMap`, `existence`, `AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion`, `eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	mathematical	—	`AlgebraicGeometry.ValuativeCriterion` `CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `Existence` `Uniqueness`	—	`CategoryTheory.MorphismProperty.ext` `iff`
`existence` 📖	mathematical	`AlgebraicGeometry.ValuativeCriterion`	`Existence`	—	`iff`
`iff` 📖	mathematical	—	`AlgebraicGeometry.ValuativeCriterion` `Existence` `Uniqueness`	—	`AlgebraicGeometry.ValuativeCommSq.commSq`
`uniqueness` 📖	mathematical	`AlgebraicGeometry.ValuativeCriterion`	`Uniqueness`	—	`iff`

AlgebraicGeometry.ValuativeCriterion.Existence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq` 📖	mathematical	—	`AlgebraicGeometry.ValuativeCriterion.Existence` `CategoryTheory.MorphismProperty.universally` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.topologically` `SpecializingMap`	—	`CategoryTheory.MorphismProperty.ext` `CategoryTheory.MorphismProperty.universally_mono` `specializingMap` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.universally_eq` `stableUnderBaseChange` `of_specializingMap`
`instIsLocalHomCarrierRingHomHomHomCommRingCat` 📖	mathematical	—	`IsLocalHom` `CommRingCat.carrier` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom.instFunLike` `CommRingCat.Hom.hom` `CategoryTheory.Iso.hom` `CommRingCat` `CommRingCat.instCategory`	—	`isLocalHom_of_isIso` `CategoryTheory.Iso.isIso_hom`
`of_specializingMap` 📖	mathematical	`CategoryTheory.MorphismProperty.universally` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.topologically` `SpecializingMap`	`AlgebraicGeometry.ValuativeCriterion.Existence`	—	`AlgebraicGeometry.ValuativeCommSq.commSq` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.IsPullback.of_hasPullback` `ValuationRing.isLocalRing` `EuclideanDomain.toNontrivial` `ValuationRing.toPreValuationRing` `instIsDomain` `ValuationRing.of_field` `IsDomain.toNontrivial` `IsLocalRing.specializes_closedPoint` `CommRingCat.Colimits.hasColimits_commRingCat` `Inseparable.of_eq` `isLocalHom_of_isIso` `CategoryTheory.Iso.isIso_hom` `RingHom.isLocalHom_comp` `AlgebraicGeometry.Scheme.Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap` `AlgebraicGeometry.stalkClosedPointIso_inv` `CategoryTheory.Category.assoc` `Specializes.mem_open` `TopologicalSpace.Opens.isOpen` `TopCat.Presheaf.germ_stalkSpecializes_assoc` `AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc` `AlgebraicGeometry.Scheme.preimage_eq_top_of_closedPoint_mem` `AlgebraicGeometry.Scheme.germ_stalkClosedPointTo` `AlgebraicGeometry.Scheme.Hom.comp_app_assoc` `CategoryTheory.Limits.pullback.lift_fst` `CategoryTheory.Functor.mapIso_refl` `CategoryTheory.Iso.refl_trans` `AlgebraicGeometry.Scheme.ΓSpecIso_naturality` `CategoryTheory.Iso.inv_hom_id_assoc` `bijective_rangeRestrict_comp_of_valuationRing` `AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf` `CommRingCat.hom_ext_iff` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `CommRingCat.hom_ext` `RingHom.ext` `RingEquiv.symm_apply_apply` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.hom_inv_id` `RingEquiv.apply_symm_apply` `AlgebraicGeometry.Spec.map_comp` `AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk` `AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk_assoc` `AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc` `CategoryTheory.Limits.limit.lift_π` `AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc` `AlgebraicGeometry.Spec.map_comp_assoc` `AlgebraicGeometry.Spec_stalkClosedPointIso` `CategoryTheory.Iso.inv_hom_id` `AlgebraicGeometry.Spec.map_id` `CategoryTheory.Category.id_comp`
`specializingMap` 📖	mathematical	`AlgebraicGeometry.ValuativeCriterion.Existence`	`SpecializingMap` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `IsLocalRing.exists_factor_valuationRing` `AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `ValuationSubring.instSubringClass` `AlgebraicGeometry.Scheme.fromSpecResidueField.eq_1` `CategoryTheory.Category.assoc` `AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk` `AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk` `ValuationSubring.instIsDomainSubtypeMem` `ValuationSubring.instValuationRingSubtypeMem` `ValuationSubring.instIsFractionRingSubtypeMem` `AlgebraicGeometry.ValuativeCommSq.commSq` `CategoryTheory.CommSq.HasLift.exists_lift` `ValuationSubring.isLocalRing` `ValuationRing.isLocalRing` `EuclideanDomain.toNontrivial` `ValuationRing.toPreValuationRing` `instIsDomain` `ValuationRing.of_field` `AlgebraicGeometry.Scheme.fromSpecResidueField_apply` `Specializes.map` `IsLocalRing.specializes_closedPoint` `AlgebraicGeometry.Scheme.Hom.continuous` `AlgebraicGeometry.Scheme.Hom.comp_apply` `IsLocalRing.comap_closedPoint` `AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint`
`stableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.ValuativeCriterion.Existence`	—	`AlgebraicGeometry.ValuativeCommSq.domain` `AlgebraicGeometry.ValuativeCommSq.valuationRing` `AlgebraicGeometry.ValuativeCommSq.isFractionRing` `CategoryTheory.Category.assoc` `CategoryTheory.CommSq.w` `CategoryTheory.IsPullback.toCommSq` `Mathlib.Tactic.Reassoc.eq_whisker'` `AlgebraicGeometry.ValuativeCommSq.commSq` `CategoryTheory.CommSq.HasLift.exists_lift` `CategoryTheory.IsPullback.hom_ext` `CategoryTheory.IsPullback.lift_fst` `CategoryTheory.IsPullback.lift_snd`

---

← Back to Index