Fiber

📁 Source: Mathlib/AlgebraicGeometry/Fiber.lean

Statistics

Metric	Count
Definitions asFiber, asFiberHom, fiber, fiberHomeo, fiberOverSpecResidueField, fiberToSpecResidueField, fiberι, fiberToSpecResidueFieldIso, instCanonicallyOverFiber	9
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, isPullback_fiberToSpecResidueField_of_isPullback	19
Total	28

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' DivisionRing.instIsArtinianRing FiniteDimensional.finiteDimensional_self
isPullback_fiberToSpecResidueField_of_isPullback 📖	mathematical	CategoryTheory.IsPullback Scheme Scheme.instCategory	CategoryTheory.IsPullback Scheme Scheme.instCategory CategoryTheory.Limits.pullback Spec Scheme.residueField Scheme.fromSpecResidueField Scheme.Pullback.instHasPullback 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' CategoryTheory.Limits.pullback.map Spec.map Scheme.Hom.residueFieldMap Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq Scheme.Hom.fiberToSpecResidueField	—	CategoryTheory.IsPullback.of_right Scheme.Pullback.instHasPullback CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.Limits.limit.lift_π Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField CategoryTheory.IsPullback.paste_horiz CategoryTheory.IsPullback.of_hasPullback

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	12 math math: AlgebraicGeometry.GeometricallyIrreducible.iff_geometricallyIrreducible_fiber, AlgebraicGeometry.isPullback_fiberToSpecResidueField_of_isPullback, 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 CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap.instFunLike 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 CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap.instFunLike 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

AlgebraicGeometry.Spec

Definitions

Name	Category	Theorems
fiberToSpecResidueFieldIso 📖	CompOp	—

---

← Back to Index