Documentation Verification Report

FunctionField

📁 Source: Mathlib/AlgebraicGeometry/FunctionField.lean

Statistics

Metric	Count
Definitions `functionField`, `germToFunctionField`, `instAlgebraCarrierFunctionFieldSpec`, `instAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensFunctionFieldOfNonemptyToScheme`, `instFieldCarrierFunctionField`, `stalkFunctionFieldAlgebra`	6
Theorems `primeIdealOf_genericPoint`, `germToFunctionField_injective`, `functionField_isFractionRing_of_affine`, `functionField_isFractionRing_of_isAffineOpen`, `functionField_isScalarTower`, `genericPoint_eq_bot_of_affine`, `genericPoint_eq_of_isOpenImmersion`, `germ_injective_of_isIntegral`, `instIsAffineXSchemeAffineCover`, `instIsDomainCarrierStalkCommRingCatPresheafOfIsIntegral`, `instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField`, `instIsIntegralToSchemeOfNonemptyCarrierCarrierCommRingCat`	12
Total	18

AlgebraicGeometry

Definitions

Name	Category	Theorems
`instAlgebraCarrierFunctionFieldSpec` 📖	CompOp	1 math math: `functionField_isFractionRing_of_affine`
`instAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensFunctionFieldOfNonemptyToScheme` 📖	CompOp	2 math math: `functionField_isFractionRing_of_isAffineOpen`, `functionField_isScalarTower`
`instFieldCarrierFunctionField` 📖	CompOp	3 math math: `functionField_isFractionRing_of_isAffineOpen`, `functionField_isFractionRing_of_affine`, `instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField`
`stalkFunctionFieldAlgebra` 📖	CompOp	2 math math: `functionField_isScalarTower`, `instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`functionField_isFractionRing_of_affine` 📖	mathematical	—	`IsFractionRing` `CommRingCat.carrier` `CommRing.toCommSemiring` `CommRingCat.commRing` `Scheme.functionField` `Spec` `instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier` `Semifield.toCommSemiring` `Field.toSemifield` `instFieldCarrierFunctionField` `instIsIntegralSpecOfIsDomainCarrier` `instAlgebraCarrierFunctionFieldSpec`	—	`instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier` `instIsIntegralSpecOfIsDomainCarrier` `CommRingCat.Colimits.hasColimits_commRingCat` `instQuasiSoberCarrierCarrierCommRingCat` `PrimeSpectrum.isPrime` `genericPoint_eq_bot_of_affine` `Submonoid.ext` `mem_nonZeroDivisors_iff_ne_zero` `IsDomain.to_noZeroDivisors` `IsDomain.toNontrivial` `StructureSheaf.IsLocalization.to_stalk`
`functionField_isFractionRing_of_isAffineOpen` 📖	mathematical	—	`IsFractionRing` `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` `CommRing.toCommSemiring` `CommRingCat.commRing` `Scheme.functionField` `irreducibleSpace_of_isIntegral` `Semifield.toCommSemiring` `Field.toSemifield` `instFieldCarrierFunctionField` `instAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensFunctionFieldOfNonemptyToScheme`	—	`irreducibleSpace_of_isIntegral` `CommRingCat.Colimits.hasColimits_commRingCat` `instQuasiSoberCarrierCarrierCommRingCat` `IsGenericPoint.mem_open_set_iff` `genericPoint_spec` `TopologicalSpace.Opens.isOpen` `Set.univ_inter` `PrimeSpectrum.isPrime` `instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier` `IsIntegral.component_integral` `IsAffineOpen.primeIdealOf_genericPoint` `genericPoint_eq_bot_of_affine` `Submonoid.ext` `mem_nonZeroDivisors_iff_ne_zero` `IsDomain.to_noZeroDivisors` `Scheme.component_nontrivial` `IsAffineOpen.isLocalization_stalk`
`functionField_isScalarTower` 📖	mathematical	—	`IsScalarTower` `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` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Scheme.functionField` `Algebra.toSMul` `CommRing.toCommSemiring` `CommRingCat.commRing` `CommSemiring.toSemiring` `TopCat.Presheaf.algebra_section_stalk` `stalkFunctionFieldAlgebra` `instAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensFunctionFieldOfNonemptyToScheme`	—	`IsScalarTower.of_algebraMap_eq'` `CommRingCat.Colimits.hasColimits_commRingCat` `instQuasiSoberCarrierCarrierCommRingCat` `Specializes.mem_open` `TopologicalSpace.Opens.isOpen` `TopCat.Presheaf.germ_stalkSpecializes`
`genericPoint_eq_bot_of_affine` 📖	mathematical	—	`genericPoint` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Spec` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `instQuasiSoberCarrierCarrierCommRingCat` `instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier` `Bot.bot` `PrimeSpectrum` `CommRingCat.carrier` `CommRing.toCommSemiring` `CommRingCat.commRing` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `PrimeSpectrum.instPartialOrder` `PrimeSpectrum.instOrderBotOfIsDomain`	—	`IsGenericPoint.eq` `instQuasiSoberCarrierCarrierCommRingCat` `instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier` `instT0SpaceCarrierCarrierCommRingCat` `genericPoint_spec` `isGenericPoint_def` `PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure` `PrimeSpectrum.vanishingIdeal_singleton` `PrimeSpectrum.zeroLocus_singleton_zero`
`genericPoint_eq_of_isOpenImmersion` 📖	mathematical	—	`DFunLike.coe` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `genericPoint` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `instQuasiSoberCarrierCarrierCommRingCat`	—	`instQuasiSoberCarrierCarrierCommRingCat` `IsGenericPoint.eq` `instT0SpaceCarrierCarrierCommRingCat` `genericPoint_spec` `Set.univ_subset_iff` `Set.univ_inter` `Set.image_univ` `subset_closure_inter_of_isPreirreducible_of_isOpen` `PreirreducibleSpace.isPreirreducible_univ` `IrreducibleSpace.toPreirreducibleSpace` `Topology.IsOpenEmbedding.isOpen_range` `Scheme.Hom.isOpenEmbedding` `IrreducibleSpace.toNonempty` `Set.mem_range_self` `IsGenericPoint.image` `Scheme.Hom.continuous`
`germ_injective_of_isIntegral` 📖	mathematical	`TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	`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` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `TopCat.Presheaf.germ`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `TopCat.Presheaf.germ_eq` `CommRingCat.FilteredColimits.forget_preservesFilteredColimits` `RingHom.map_zero` `Preorder.subsingleton_hom` `map_injective_of_isIntegral`
`instIsAffineXSchemeAffineCover` 📖	mathematical	—	`IsAffine` `CategoryTheory.PreZeroHypercover.X` `Scheme` `Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `Scheme.precoverage` `IsOpenImmersion` `Scheme.affineCover`	—	`isAffine_Spec` `Scheme.local_affine`
`instIsDomainCarrierStalkCommRingCatPresheafOfIsIntegral` 📖	mathematical	—	`IsDomain` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `PresheafedSpace.carrier` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `PresheafedSpace.presheaf` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`Function.Injective.isDomain` `irreducibleSpace_of_isIntegral` `CommRingCat.Colimits.hasColimits_commRingCat` `instIsDomain` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsFractionRing.injective` `instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField`
`instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField` 📖	mathematical	—	`IsFractionRing` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `PresheafedSpace.carrier` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `PresheafedSpace.presheaf` `CommRing.toCommSemiring` `CommRingCat.commRing` `Scheme.functionField` `irreducibleSpace_of_isIntegral` `Semifield.toCommSemiring` `Field.toSemifield` `instFieldCarrierFunctionField` `stalkFunctionFieldAlgebra`	—	`Scheme.instJointlySurjectivePrecoverage` `Scheme.instIsOpenImmersionF` `isAffineOpen_opensRange` `instIsAffineXSchemeAffineCover` `Scheme.Cover.covers` `PrimeSpectrum.isPrime` `CommRingCat.Colimits.hasColimits_commRingCat` `IsAffineOpen.isLocalization_stalk` `irreducibleSpace_of_isIntegral` `functionField_isFractionRing_of_isAffineOpen` `functionField_isScalarTower` `IsFractionRing.isFractionRing_of_isDomain_of_isLocalization` `IsIntegral.component_integral`
`instIsIntegralToSchemeOfNonemptyCarrierCarrierCommRingCat` 📖	mathematical	—	`IsIntegral` `Scheme.Opens.toScheme`	—	`isIntegral_of_isOpenImmersion` `Scheme.Opens.instIsOpenImmersionι`

AlgebraicGeometry.IsAffineOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`primeIdealOf_genericPoint` 📖	mathematical	—	`primeIdealOf` `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` `genericPoint` `AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat` `AlgebraicGeometry.irreducibleSpace_of_isIntegral` `Set` `Set.instMembership` `SetLike.coe` `TopologicalSpace.Opens` `Set.Nonempty` `Set.instInter` `Set.univ` `IsGenericPoint.mem_open_set_iff` `genericPoint_spec` `TopologicalSpace.Opens.isOpen` `AlgebraicGeometry.Spec` `CategoryTheory.Functor.obj` `Opposite` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier` `AlgebraicGeometry.IsIntegral.component_integral`	—	`AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat` `AlgebraicGeometry.irreducibleSpace_of_isIntegral` `IsGenericPoint.mem_open_set_iff` `genericPoint_spec` `TopologicalSpace.Opens.isOpen` `AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier` `AlgebraicGeometry.IsIntegral.component_integral` `TopologicalSpace.Opens.isOpenEmbedding` `TopologicalSpace.Opens.isOpenEmbedding_obj_top` `AlgebraicGeometry.instIsIntegralToSchemeOfNonemptyCarrierCarrierCommRingCat` `AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion` `AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι` `AlgebraicGeometry.IsOpenImmersion.comp` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Iso.isIso_hom` `AlgebraicGeometry.instIsIsoSchemeMapOfCommRingCat` `CategoryTheory.Functor.map_isIso` `CategoryTheory.isIso_op` `CategoryTheory.instIsIsoEqToHom`

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
`functionField` 📖	CompOp	5 math math: `AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen`, `AlgebraicGeometry.functionField_isFractionRing_of_affine`, `AlgebraicGeometry.functionField_isScalarTower`, `germToFunctionField_injective`, `AlgebraicGeometry.instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField`
`germToFunctionField` 📖	CompOp	1 math math: `germToFunctionField_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`germToFunctionField_injective` 📖	mathematical	—	`CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Opens` `functionField` `AlgebraicGeometry.irreducibleSpace_of_isIntegral` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `germToFunctionField`	—	`AlgebraicGeometry.germ_injective_of_isIntegral` `AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat` `AlgebraicGeometry.irreducibleSpace_of_isIntegral`

---

← Back to Index