Documentation Verification Report

Fiber

📁 Source: Mathlib/AlgebraicGeometry/Fiber.lean

Statistics

Metric	Count
Definitions `asFiber`, `asFiberHom`, `fiber`, `fiberHomeo`, `fiberOverSpecResidueField`, `fiberToSpecResidueField`, `fiberι`, `instCanonicallyOverFiber`	8
Theorems `isCompact_preimage_singleton`, `asFiberHom_apply`, `asFiberHom_fiberToSpecResidueField`, `asFiberHom_fiberToSpecResidueField_assoc`, `asFiberHom_fiberι`, `asFiberHom_fiberι_assoc`, `fiberHomeo_apply`, `fiberToSpecResidueField_apply`, `fiberι_asFiber`, `fiberι_fiberHomeo_symm`, `isCompact_preimage_singleton`, `range_asFiberHom`, `range_fiberι`, `instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact`, `instIsAffineFiberOfIsAffineHom`, `instIsPreimmersionAsFiberHom`, `instIsPreimmersionFiberι`, `instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType`	18
Total	26

AlgebraicGeometry

Definitions

Name	Category	Theorems
`instCanonicallyOverFiber` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact` 📖	mathematical	—	`CompactSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Scheme.Hom.fiber` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`HasAffineProperty.iff_of_isAffine` `instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat` `isAffine_Spec` `CategoryTheory.MorphismProperty.pullback_snd` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `quasiCompact_isStableUnderBaseChange`
`instIsAffineFiberOfIsAffineHom` 📖	mathematical	—	`IsAffine` `Scheme.Hom.fiber`	—	`isAffine_of_isAffineHom` `CategoryTheory.MorphismProperty.pullback_snd` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `isAffineHom_isStableUnderBaseChange` `isAffine_Spec`
`instIsPreimmersionAsFiberHom` 📖	mathematical	—	`IsPreimmersion` `Spec` `Scheme.residueField` `Scheme.Hom.fiber` `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'` `Scheme.Hom.asFiberHom`	—	`Scheme.instIsPreimmersionFromSpecResidueField` `Scheme.Hom.asFiberHom_fiberι` `IsPreimmersion.of_comp` `instIsPreimmersionFiberι`
`instIsPreimmersionFiberι` 📖	mathematical	—	`IsPreimmersion` `Scheme.Hom.fiber` `Scheme.Hom.fiberι`	—	`CategoryTheory.MorphismProperty.pullback_fst` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `IsPreimmersion.instIsStableUnderBaseChangeScheme` `Scheme.instIsPreimmersionFromSpecResidueField`
`instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType` 📖	mathematical	—	`JacobsonSpace` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Scheme.Hom.fiber` `SheafedSpace.instTopologicalSpaceCarrierCarrier`	—	`CategoryTheory.MorphismProperty.pullback_snd` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `locallyOfFiniteType_isStableUnderBaseChange` `LocallyOfFiniteType.jacobsonSpace` `instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier` `instIsJacobsonRingOfIsArtinianRing` `isArtinian_of_fg_of_artinian'` `CommRingCat.Colimits.hasColimits_commRingCat` `DivisionRing.instIsArtinianRing` `FiniteDimensional.finiteDimensional_self`

AlgebraicGeometry.QuasiCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCompact_preimage_singleton` 📖	mathematical	—	`IsCompact` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set.preimage` `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'` `Set` `Set.instSingletonSet`	—	`AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton`

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
`asFiber` 📖	CompOp	5 math math: `range_asFiberHom`, `asFiberHom_apply`, `fiberι_asFiber`, `quasiFiniteAt_iff_isOpen_singleton_asFiber`, `QuasiFiniteAt.isClopen_singleton_asFiber`
`asFiberHom` 📖	CompOp	7 math math: `range_asFiberHom`, `asFiberHom_fiberι_assoc`, `asFiberHom_apply`, `asFiberHom_fiberι`, `asFiberHom_fiberToSpecResidueField`, `AlgebraicGeometry.instIsPreimmersionAsFiberHom`, `asFiberHom_fiberToSpecResidueField_assoc`
`fiber` 📖	CompOp	32 math math: `fiberHomeo_apply`, `range_fiberι`, `AlgebraicGeometry.instIsIntegralFiberOfGeometricallyIntegral`, `AlgebraicGeometry.GeometricallyIrreducible.iff_geometricallyIrreducible_fiber`, `AlgebraicGeometry.instIsReducedFiberOfGeometricallyReduced`, `range_asFiberHom`, `AlgebraicGeometry.instGeometricallyReducedFiberToSpecResidueField`, `AlgebraicGeometry.instIsFiniteFiberToSpecResidueFieldOfLocallyQuasiFiniteOfQuasiCompact`, `asFiberHom_fiberι_assoc`, `AlgebraicGeometry.instGeometricallyIntegralFiberToSpecResidueField`, `AlgebraicGeometry.locallyQuasiFinite_iff_isFinite_fiber`, `asFiberHom_apply`, `AlgebraicGeometry.fiber_of_geometrically`, `AlgebraicGeometry.instIsAffineFiberOfIsAffineHom`, `AlgebraicGeometry.instIsArtinianSchemeFiberOfLocallyQuasiFiniteOfQuasiCompact`, `asFiberHom_fiberι`, `AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible`, `fiberι_asFiber`, `AlgebraicGeometry.instIsLocallyArtinianFiberOfLocallyQuasiFinite`, `AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType`, `quasiFiniteAt_iff_isOpen_singleton_asFiber`, `AlgebraicGeometry.geometrically_iff_forall_fiberToSpecResidueField`, `AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact`, `AlgebraicGeometry.GeometricallyIntegral.iff_geometricallyIntegral_fiber`, `asFiberHom_fiberToSpecResidueField`, `QuasiFiniteAt.isClopen_singleton_asFiber`, `AlgebraicGeometry.instIsPreimmersionAsFiberHom`, `AlgebraicGeometry.instIsPreimmersionFiberι`, `fiberToSpecResidueField_apply`, `fiberι_fiberHomeo_symm`, `AlgebraicGeometry.instGeometricallyIrreducibleFiberToSpecResidueField`, `asFiberHom_fiberToSpecResidueField_assoc`
`fiberHomeo` 📖	CompOp	2 math math: `fiberHomeo_apply`, `fiberι_fiberHomeo_symm`
`fiberOverSpecResidueField` 📖	CompOp	—
`fiberToSpecResidueField` 📖	CompOp	11 math math: `AlgebraicGeometry.GeometricallyIrreducible.iff_geometricallyIrreducible_fiber`, `AlgebraicGeometry.instGeometricallyReducedFiberToSpecResidueField`, `AlgebraicGeometry.instIsFiniteFiberToSpecResidueFieldOfLocallyQuasiFiniteOfQuasiCompact`, `AlgebraicGeometry.instGeometricallyIntegralFiberToSpecResidueField`, `AlgebraicGeometry.locallyQuasiFinite_iff_isFinite_fiber`, `AlgebraicGeometry.geometrically_iff_forall_fiberToSpecResidueField`, `AlgebraicGeometry.GeometricallyIntegral.iff_geometricallyIntegral_fiber`, `asFiberHom_fiberToSpecResidueField`, `fiberToSpecResidueField_apply`, `AlgebraicGeometry.instGeometricallyIrreducibleFiberToSpecResidueField`, `asFiberHom_fiberToSpecResidueField_assoc`
`fiberι` 📖	CompOp	7 math math: `fiberHomeo_apply`, `range_fiberι`, `asFiberHom_fiberι_assoc`, `asFiberHom_fiberι`, `fiberι_asFiber`, `AlgebraicGeometry.instIsPreimmersionFiberι`, `fiberι_fiberHomeo_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asFiberHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.residueField` `fiber` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `asFiberHom` `asFiber`	—	`Topology.IsEmbedding.injective` `isEmbedding` `AlgebraicGeometry.instIsPreimmersionFiberι` `asFiberHom_fiberι` `AlgebraicGeometry.Scheme.fromSpecResidueField_apply` `fiberι_asFiber`
`asFiberHom_fiberToSpecResidueField` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.residueField` `fiber` `DFunLike.coe` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `asFiberHom` `fiberToSpecResidueField` `AlgebraicGeometry.Spec.map` `residueFieldMap`	—	`CategoryTheory.Limits.pullback.lift_snd`
`asFiberHom_fiberToSpecResidueField_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.residueField` `fiber` `DFunLike.coe` `ContinuousMap` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `ContinuousMap.instFunLike` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `asFiberHom` `fiberToSpecResidueField` `AlgebraicGeometry.Spec.map` `residueFieldMap`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `asFiberHom_fiberToSpecResidueField`
`asFiberHom_fiberι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.residueField` `fiber` `DFunLike.coe` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `asFiberHom` `fiberι` `AlgebraicGeometry.Scheme.fromSpecResidueField`	—	`CategoryTheory.Limits.pullback.lift_fst`
`asFiberHom_fiberι_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.residueField` `fiber` `DFunLike.coe` `ContinuousMap` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `ContinuousMap.instFunLike` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `asFiberHom` `fiberι` `AlgebraicGeometry.Scheme.fromSpecResidueField`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `asFiberHom_fiberι`
`fiberHomeo_apply` 📖	mathematical	—	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `Set` `Set.instMembership` `Set.preimage` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `Set.instSingletonSet` `Homeomorph` `fiber` `Set.Elem` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `instTopologicalSpaceSubtype` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `fiberHomeo` `fiberι`	—	—
`fiberToSpecResidueField_apply` 📖	mathematical	—	`DFunLike.coe` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `fiber` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.residueField` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `fiberToSpecResidueField` `IsLocalRing.closedPoint` `CommRingCat.carrier` `Semifield.toCommSemiring` `Field.toSemifield` `AlgebraicGeometry.Scheme.instFieldCarrierResidueField` `Field.instIsLocalRing`	—	`Unique.instSubsingleton` `Field.instIsLocalRing`
`fiberι_asFiber` 📖	mathematical	—	`DFunLike.coe` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `fiber` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `fiberι` `asFiber`	—	`fiberι_fiberHomeo_symm`
`fiberι_fiberHomeo_symm` 📖	mathematical	—	`DFunLike.coe` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `fiber` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `fiberι` `Homeomorph` `Set.Elem` `Set.preimage` `Set` `Set.instSingletonSet` `instTopologicalSpaceSubtype` `Set.instMembership` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `fiberHomeo`	—	`Homeomorph.apply_symm_apply`
`isCompact_preimage_singleton` 📖	mathematical	—	`IsCompact` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Set.preimage` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `Set` `Set.instSingletonSet`	—	`isCompact_range` `AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact` `continuous` `range_fiberι`
`range_asFiberHom` 📖	mathematical	—	`Set.range` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `fiber` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Scheme.residueField` `asFiberHom` `Set` `Set.instSingletonSet` `asFiber`	—	`AlgebraicGeometry.instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier` `EuclideanDomain.toNontrivial` `asFiberHom_apply`
`range_fiberι` 📖	mathematical	—	`Set.range` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `fiber` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `fiberι` `Set.preimage` `Set` `Set.instSingletonSet`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.Scheme.Pullback.range_fst` `AlgebraicGeometry.Scheme.range_fromSpecResidueField`

---

← Back to Index