GammaSpecAdjunction

📁 Source: Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

Statistics

Metric	Count
Definitions toToΓSpecMapBasicOpen, toΓSpec, toΓSpecBase, toΓSpecCApp, toΓSpecCBasicOpens, toΓSpecFun, toΓSpecMapBasicOpen, toΓSpecSheafedSpace, toSpecΓ, fullyFaithful, fullyFaithfulToLocallyRingedSpace, homEquiv, preimage, reflective, identityToΓSpec, instReflectiveLocallyRingedSpaceOppositeCommRingCatToLocallyRingedSpace, adjunction, locallyRingedSpaceAdjunction	18
Theorems coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, comp_ring_hom_ext, isUnit_res_toΓSpecMapBasicOpen, notMem_prime_iff_unit_in_stalk, toStalk_stalkMap_toΓSpec, toΓSpecCApp_iff, toΓSpecCApp_spec, toΓSpecCBasicOpens_app, toΓSpecMapBasicOpen_eq, toΓSpecSheafedSpace_app_eq, toΓSpecSheafedSpace_app_spec, toΓSpecSheafedSpace_app_spec_assoc, toΓSpecSheafedSpace_hom_c_app, toΓSpec_base, toΓSpec_continuous, toΓSpec_preimage_basicOpen_eq, toΓSpec_preimage_zeroLocus_eq, Γ_Spec_left_triangle, toSpecΓ_appTop, toSpecΓ_apply, toSpecΓ_base, toSpecΓ_naturality, toSpecΓ_naturality_assoc, toSpecΓ_preimage_basicOpen, faithful, full, homEquiv_apply, homEquiv_symm_apply, map_eq_id, map_inj, map_injective, map_preimage, map_preimage_unop, map_surjective, preimage_comp, preimage_comp_assoc, preimage_id, preimage_map, SpecMap_ΓSpecIso_hom, SpecMap_ΓSpecIso_inv_toSpecΓ, SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, instFaithfulOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace, instFullOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace, instIsRightAdjointCommRingCatOppositeLocallyRingedSpaceΓ, instIsRightAdjointCommRingCatOppositeSchemeΓ, toSpecΓ_SpecMap_ΓSpecIso_inv, toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, adjunction_counit_app, adjunction_counit_app', adjunction_homEquiv_apply, adjunction_homEquiv_symm_apply, adjunction_unit_app, isIso_adjunction_counit, isIso_locallyRingedSpaceAdjunction_counit, left_triangle, locallyRingedSpaceAdjunction_counit, locallyRingedSpaceAdjunction_counit_app, locallyRingedSpaceAdjunction_counit_app', locallyRingedSpaceAdjunction_homEquiv_apply, locallyRingedSpaceAdjunction_homEquiv_apply', locallyRingedSpaceAdjunction_unit, right_triangle, toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, toSpecΓ_of, toSpecΓ_unop, unop_locallyRingedSpaceAdjunction_counit_app', ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, ΓSpecIso_obj_hom, ΓSpec_adjunction_homEquiv_eq	69
Total	87

AlgebraicGeometry

Definitions

Name	Category	Theorems
identityToΓSpec 📖	CompOp	5 math math: ΓSpec.left_triangle, ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply', ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply, ΓSpec.locallyRingedSpaceAdjunction_unit, ΓSpec.right_triangle
instReflectiveLocallyRingedSpaceOppositeCommRingCatToLocallyRingedSpace 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SpecMap_ΓSpecIso_hom 📖	mathematical	—	Spec.map CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Spec TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.hom Scheme.ΓSpecIso Scheme.toSpecΓ	—	CategoryTheory.Adjunction.right_triangle_components CategoryTheory.Iso.isIso_inv CategoryTheory.IsIso.Iso.inv_inv instIsIsoSchemeMapOfCommRingCat Spec.map_inv CategoryTheory.Category.id_comp CategoryTheory.IsIso.eq_comp_inv
SpecMap_ΓSpecIso_inv_toSpecΓ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec 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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Spec.map CategoryTheory.Iso.inv Scheme.ΓSpecIso Scheme.toSpecΓ CategoryTheory.CategoryStruct.id	—	SpecMap_ΓSpecIso_hom Spec.map_comp CategoryTheory.Iso.hom_inv_id Spec.map_id
SpecMap_ΓSpecIso_inv_toSpecΓ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec 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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Spec.map CategoryTheory.Iso.inv Scheme.ΓSpecIso Scheme.toSpecΓ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' SpecMap_ΓSpecIso_inv_toSpecΓ
instFaithfulOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace 📖	mathematical	—	CategoryTheory.Functor.Faithful Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory LocallyRingedSpace LocallyRingedSpace.instCategory Spec.toLocallyRingedSpace	—	CategoryTheory.Functor.FullyFaithful.faithful
instFullOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace 📖	mathematical	—	CategoryTheory.Functor.Full Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory LocallyRingedSpace LocallyRingedSpace.instCategory Spec.toLocallyRingedSpace	—	CategoryTheory.Functor.FullyFaithful.full
instIsRightAdjointCommRingCatOppositeLocallyRingedSpaceΓ 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint CommRingCat CommRingCat.instCategory Opposite LocallyRingedSpace CategoryTheory.Category.opposite LocallyRingedSpace.instCategory LocallyRingedSpace.Γ	—	CategoryTheory.Adjunction.isRightAdjoint
instIsRightAdjointCommRingCatOppositeSchemeΓ 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint CommRingCat CommRingCat.instCategory Opposite Scheme CategoryTheory.Category.opposite Scheme.instCategory Scheme.Γ	—	CategoryTheory.Adjunction.isRightAdjoint
toSpecΓ_SpecMap_ΓSpecIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec 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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Scheme.toSpecΓ Spec.map CategoryTheory.Iso.inv Scheme.ΓSpecIso CategoryTheory.CategoryStruct.id	—	SpecMap_ΓSpecIso_hom Spec.map_comp CategoryTheory.Iso.inv_hom_id Spec.map_id
toSpecΓ_SpecMap_ΓSpecIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec 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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Scheme.toSpecΓ Spec.map CategoryTheory.Iso.inv Scheme.ΓSpecIso	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' toSpecΓ_SpecMap_ΓSpecIso_inv
ΓSpecIso_inv_ΓSpec_adjunction_homEquiv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Spec TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.inv Scheme.ΓSpecIso Scheme.Hom.appTop Scheme Scheme.instCategory Scheme.Spec DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.rightOp Scheme.Γ EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv ΓSpec.adjunction Quiver.Hom.op	—	Scheme.toSpecΓ_appTop Scheme.ΓSpecIso_naturality CategoryTheory.Iso.inv_hom_id_assoc
ΓSpecIso_obj_hom 📖	mathematical	—	CategoryTheory.Iso.hom CommRingCat CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Spec TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Scheme.ΓSpecIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Scheme.Opens.toScheme Scheme.Hom.appTop Spec.map CategoryTheory.Iso.inv Scheme.Opens.topIso Scheme.toSpecΓ	—	Scheme.Opens.instIsOpenImmersionι CategoryTheory.eqToHom_op Scheme.toSpecΓ_appTop Scheme.ΓSpecIso_naturality_assoc CategoryTheory.eqToHom_map_comp CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
ΓSpec_adjunction_homEquiv_eq 📖	mathematical	—	Scheme.Hom.appTop CategoryTheory.Functor.obj Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory Scheme Scheme.instCategory Scheme.Spec Opposite.op DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.rightOp Scheme.Γ EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv ΓSpec.adjunction Quiver.Hom.op TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.CategoryStruct.comp Spec CategoryTheory.Iso.hom Scheme.ΓSpecIso	—	CategoryTheory.Iso.inv_comp_eq ΓSpecIso_inv_ΓSpec_adjunction_homEquiv

AlgebraicGeometry.LocallyRingedSpace

Definitions

Name	Category	Theorems
toToΓSpecMapBasicOpen 📖	CompOp	5 math math: isUnit_res_toΓSpecMapBasicOpen, toΓSpecSheafedSpace_app_spec, toΓSpecSheafedSpace_app_spec_assoc, toΓSpecCApp_spec, toΓSpecCApp_iff
toΓSpec 📖	CompOp	3 math math: Γ_Spec_left_triangle, toΓSpec_base, toΓSpec_preimage_zeroLocus_eq
toΓSpecBase 📖	CompOp	3 math math: toΓSpec_base, toΓSpecCBasicOpens_app, toΓSpecSheafedSpace_hom_c_app
toΓSpecCApp 📖	CompOp	4 math math: toΓSpecSheafedSpace_app_eq, toΓSpecCBasicOpens_app, toΓSpecCApp_spec, toΓSpecCApp_iff
toΓSpecCBasicOpens 📖	CompOp	2 math math: toΓSpecCBasicOpens_app, toΓSpecSheafedSpace_hom_c_app
toΓSpecFun 📖	CompOp	3 math math: notMem_prime_iff_unit_in_stalk, toΓSpec_continuous, toΓSpec_preimage_basicOpen_eq
toΓSpecMapBasicOpen 📖	CompOp	4 math math: isUnit_res_toΓSpecMapBasicOpen, toΓSpecMapBasicOpen_eq, toΓSpecCApp_spec, toΓSpecCApp_iff
toΓSpecSheafedSpace 📖	CompOp	6 math math: toΓSpecSheafedSpace_app_eq, coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, toStalk_stalkMap_toΓSpec, toΓSpecSheafedSpace_app_spec, toΓSpecSheafedSpace_app_spec_assoc, toΓSpecSheafedSpace_hom_c_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal 📖	mathematical	—	SetLike.coe Submodule CommRingCat.carrier CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory CommRingCat CommRingCat.instCategory Γ Opposite.op CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.setLike PrimeSpectrum.asIdeal DFunLike.coe ContinuousMap TopCat.carrier PrimeSpectrum TopCat.str PrimeSpectrum.zariskiTopology ContinuousMap.instFunLike TopCat.Hom.hom toTopCat AlgebraicGeometry.Spec.topObj AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.Spec.toSheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toΓSpecSheafedSpace Set.preimage TopologicalSpace.Opens AlgebraicGeometry.PresheafedSpace.carrier Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat RingHom RingHom.instFunLike CommRingCat.Hom.hom TopCat.Presheaf.Γgerm Ideal IsLocalRing.closedPoint instIsLocalRingCarrierStalkCommRingCatPresheaf	—	—
comp_ring_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.Spec.locallyRingedSpaceObj CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory Γ Opposite.op AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom toΓSpec AlgebraicGeometry.Spec.locallyRingedSpaceMap TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf TopologicalSpace.Opens.map PrimeSpectrum.basicOpen CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing CategoryTheory.Functor.map Opposite.unop AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.op AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace forgetToSheafedSpace Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.homOfLE le_top CommRingCat.of AlgebraicGeometry.PrimeSpectrum.Top CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c	—	—	le_top CategoryTheory.Functor.map_injective instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace AlgebraicGeometry.Spec.basicOpen_hom_ext AlgebraicGeometry.SheafedSpace.comp_hom_c_app PrimeSpectrum.continuous_comap AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc CategoryTheory.Category.assoc toΓSpecSheafedSpace_app_spec CategoryTheory.Functor.map_comp
isUnit_res_toΓSpecMapBasicOpen 📖	mathematical	—	IsUnit CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op toΓSpecMapBasicOpen MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing DFunLike.coe Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier toToΓSpecMapBasicOpen	—	toΓSpecMapBasicOpen_eq AlgebraicGeometry.RingedSpace.basicOpen_le CommRingCat.comp_apply CategoryTheory.Functor.map_comp RingHom.isUnit_map AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen
notMem_prime_iff_unit_in_stalk 📖	mathematical	—	CommRingCat.carrier CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory CommRingCat CommRingCat.instCategory Γ Opposite.op Ideal CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule PrimeSpectrum.asIdeal toΓSpecFun IsUnit TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.ConcreteCategory.hom RingHom RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier TopCat.Presheaf.Γgerm	—	CommRingCat.Colimits.hasColimits_commRingCat RingHom.instRingHomClass instIsLocalRingCarrierStalkCommRingCatPresheaf
toStalk_stalkMap_toΓSpec 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier Opposite.unop Opposite.op CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory Γ CommRingCat.commRing TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PrimeSpectrum.Top AlgebraicGeometry.structurePresheafInCommRingCat DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.Spec.toSheafedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toΓSpecSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.StructureSheaf.toStalk AlgebraicGeometry.PresheafedSpace.Hom.stalkMap TopCat.Presheaf.Γgerm	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.Hom.stalkMap.eq_1 PrimeSpectrum.basicOpen_one AlgebraicGeometry.StructureSheaf.algebraMap_germ CategoryTheory.Category.assoc TopCat.Presheaf.stalkFunctor_map_germ toΓSpecSheafedSpace_app_eq toΓSpecCApp_spec TopCat.Presheaf.Γgerm.eq_1 TopCat.Presheaf.stalkPushforward_germ TopCat.Presheaf.germ_res le_top
toΓSpecCApp_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory Γ Opposite.op CommRingCat.commRing TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring PrimeSpectrum.basicOpen AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf toΓSpecMapBasicOpen CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType toToΓSpecMapBasicOpen toΓSpecCApp	—	AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen CategoryTheory.ConcreteCategory.ext_iff isUnit_res_toΓSpecMapBasicOpen IsLocalization.Away.lift_comp CommRingCat.hom_ext IsLocalization.ringHom_ext
toΓSpecCApp_spec 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory Γ Opposite.op CommRingCat.commRing TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring PrimeSpectrum.basicOpen AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf toΓSpecMapBasicOpen CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType toΓSpecCApp toToΓSpecMapBasicOpen	—	toΓSpecCApp_iff
toΓSpecCBasicOpens_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.InducedCategory CommRingCat.carrier CategoryTheory.Functor.obj AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory CommRingCat CommRingCat.instCategory Γ Opposite.op TopologicalSpace.Opens PrimeSpectrum CommRing.toCommSemiring CommRingCat.commRing PrimeSpectrum.zariskiTopology PrimeSpectrum.basicOpen CategoryTheory.InducedCategory.instCategory Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.inducedFunctor CategoryTheory.Sheaf.val TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf AlgebraicGeometry.Spec.topObj TopCat.Sheaf toTopCat TopCat.instCategorySheaf TopCat.Sheaf.pushforward toΓSpecBase 𝒪 toΓSpecCBasicOpens toΓSpecCApp Opposite.unop	—	—
toΓSpecMapBasicOpen_eq 📖	mathematical	—	toΓSpecMapBasicOpen AlgebraicGeometry.RingedSpace.basicOpen toRingedSpace Top.top TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory Opposite.unop AlgebraicGeometry.PresheafedSpace CategoryTheory.Functor.obj Opposite AlgebraicGeometry.SheafedSpace CategoryTheory.Category.opposite AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.op AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace AlgebraicGeometry.LocallyRingedSpace instCategory forgetToSheafedSpace Opposite.op TopCat.str OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	TopologicalSpace.Opens.ext toΓSpec_preimage_basicOpen_eq
toΓSpecSheafedSpace_app_eq 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace CategoryTheory.Functor.obj CategoryTheory.Category.opposite AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.Spec.toSheafedSpace Opposite.op AlgebraicGeometry.LocallyRingedSpace instCategory Γ TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf TopCat.Presheaf toSheafedSpace TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toΓSpecSheafedSpace AlgebraicGeometry.PresheafedSpace.Hom.c PrimeSpectrum.basicOpen CommRingCat.carrier Opposite.unop CommRing.toCommSemiring CommRingCat.commRing toΓSpecCApp	—	TopCat.Sheaf.extend_hom_app
toΓSpecSheafedSpace_app_spec 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory Γ Opposite.op CommRingCat.commRing TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top Opposite.unop TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.Spec.toSheafedSpace PrimeSpectrum.basicOpen AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id TopCat.Presheaf toSheafedSpace TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toΓSpecSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c toToΓSpecMapBasicOpen	—	toΓSpecCApp_spec toΓSpecSheafedSpace_app_eq
toΓSpecSheafedSpace_app_spec_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory Γ Opposite.op CommRingCat.commRing TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.Spec.toSheafedSpace PrimeSpectrum.basicOpen AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType TopCat.Presheaf toSheafedSpace TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toΓSpecSheafedSpace AlgebraicGeometry.PresheafedSpace.presheaf CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c toToΓSpecMapBasicOpen	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toΓSpecSheafedSpace_app_spec
toΓSpecSheafedSpace_hom_c_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top CommRingCat.carrier CategoryTheory.Functor.obj AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory CommRingCat CommRingCat.instCategory Γ Opposite.op CommRingCat.commRing TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.Spec.structureSheaf TopCat.Sheaf toTopCat TopCat.instCategorySheaf AlgebraicGeometry.Spec.topObj TopCat.Sheaf.pushforward toΓSpecBase 𝒪 AlgebraicGeometry.PresheafedSpace.Hom.c AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.Spec.toSheafedSpace CategoryTheory.InducedCategory.Hom.hom AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces toΓSpecSheafedSpace CategoryTheory.Functor.preimage CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace.presheaf Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder PrimeSpectrum CommRing.toCommSemiring TopologicalSpace.Opens.map Opposite.unop CategoryTheory.yoneda CategoryTheory.Yoneda.yoneda_full CategoryTheory.Functor.comp TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward CategoryTheory.Functor.IsCoverDense.sheafYonedaHom CategoryTheory.InducedCategory PrimeSpectrum.basicOpen CategoryTheory.InducedCategory.instCategory CategoryTheory.inducedFunctor TopCat.Opens.coverDense_inducedFunctor toΓSpecCBasicOpens	—	—
toΓSpec_base 📖	mathematical	—	AlgebraicGeometry.PresheafedSpace.Hom.base CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.Spec.locallyRingedSpaceObj CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory Γ Opposite.op Hom.toHom toΓSpec toΓSpecBase	—	—
toΓSpec_continuous 📖	mathematical	—	Continuous TopCat.carrier toTopCat PrimeSpectrum CommRingCat.carrier CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory CommRingCat CommRingCat.instCategory Γ Opposite.op CommRing.toCommSemiring CommRingCat.commRing TopCat.str PrimeSpectrum.zariskiTopology toΓSpecFun	—	TopologicalSpace.IsTopologicalBasis.continuous_iff PrimeSpectrum.isTopologicalBasis_basic_opens toΓSpec_preimage_basicOpen_eq TopologicalSpace.Opens.is_open'
toΓSpec_preimage_basicOpen_eq 📖	mathematical	—	Set.preimage TopCat.carrier toTopCat PrimeSpectrum CommRingCat.carrier CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory CommRingCat CommRingCat.instCategory Γ Opposite.op CommRing.toCommSemiring CommRingCat.commRing toΓSpecFun SetLike.coe TopologicalSpace.Opens PrimeSpectrum.zariskiTopology TopologicalSpace.Opens.instSetLike PrimeSpectrum.basicOpen AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.RingedSpace.basicOpen Top.top Opposite.unop AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.op AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace forgetToSheafedSpace TopCat.str OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Set.ext CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.RingedSpace.mem_top_basicOpen notMem_prime_iff_unit_in_stalk
toΓSpec_preimage_zeroLocus_eq 📖	mathematical	—	Set.preimage TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.Spec.locallyRingedSpaceObj CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory Γ Opposite.op DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom toΓSpec PrimeSpectrum.zeroLocus CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AlgebraicGeometry.RingedSpace.zeroLocus toRingedSpace Top.top TopologicalSpace.Opens OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Set.preimage_compl TopologicalSpace.Opens.carrier_eq_coe toΓSpec_preimage_basicOpen_eq Set.iInter₂_congr Set.iInter_congr_Prop PrimeSpectrum.basicOpen_eq_zeroLocus_compl compl_compl PrimeSpectrum.zeroLocus_iUnion₂ Set.iUnion_congr_Prop Set.biUnion_of_singleton
Γ_Spec_left_triangle 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite instCategory Γ Opposite.op AlgebraicGeometry.Spec.toLocallyRingedSpace TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace toSheafedSpace AlgebraicGeometry.Spec.locallyRingedSpaceObj TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base Hom.toHom toΓSpec AlgebraicGeometry.PresheafedSpace.presheaf Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.toSpecΓ CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.CategoryStruct.id	—	toΓSpecSheafedSpace_app_spec CategoryTheory.Functor.map_id Mathlib.Tactic.DepRewrite.nddcongrArg PrimeSpectrum.basicOpen_one

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
toSpecΓ 📖	CompOp	41 math math: toSpecΓ_apply, IsQuasiAffine.toIsImmersion, Opens.toSpecΓ_SpecMap_presheaf_map_top, AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero_assoc, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, fromSpecStalk_toSpecΓ_assoc, isoSpec_inv_toSpecΓ, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, isoSpec_hom, toSpecΓ_naturality_assoc, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, toSpecΓ_isoSpec_inv_assoc, toSpecΓ_naturality, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ, toSpecΓ_preimage_zeroLocus, fromSpecStalk_toSpecΓ, ker_toSpecΓ, Opens.toSpecΓ_SpecMap_presheaf_map_top_assoc, AlgebraicGeometry.ΓSpecIso_obj_hom, AlgebraicGeometry.ΓSpec.adjunction_unit_app, Opens.toSpecΓ_top, instIsOpenImmersionToSpecΓOfIsQuasiAffine, isPullback_toSpecΓ_toSpecΓ, toSpecΓ_isoSpec_inv, toSpecΓ_appTop, AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat, preimage_opensRange_toSpecΓ, AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero, toSpecΓ_image_zeroLocus, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv_assoc, isoSpec_inv_toSpecΓ_assoc, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv, AlgebraicGeometry.instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, AlgebraicGeometry.IsAffine.affine, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ_assoc, AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, toSpecΓ_preimage_basicOpen, AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ, AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ_assoc, toSpecΓ_base

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSpecΓ_appTop 📖	mathematical	—	Hom.appTop AlgebraicGeometry.Spec 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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder toSpecΓ CategoryTheory.Iso.hom ΓSpecIso	—	CategoryTheory.Adjunction.left_triangle_components CategoryTheory.isIso_op CategoryTheory.Iso.isIso_inv CategoryTheory.Category.id_comp CategoryTheory.IsIso.eq_comp_inv CategoryTheory.op_inv CategoryTheory.IsIso.Iso.inv_inv
toSpecΓ_apply 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.Spec CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' toSpecΓ TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Spec.map TopCat.Presheaf.Γgerm IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf	—	—
toSpecΓ_base 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.Spec CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' toSpecΓ TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Spec.map TopCat.Presheaf.Γgerm IsLocalRing.closedPoint CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf	—	toSpecΓ_apply
toSpecΓ_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec 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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder toSpecΓ AlgebraicGeometry.Spec.map Hom.appTop	—	CategoryTheory.NatTrans.naturality
toSpecΓ_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct instCategory AlgebraicGeometry.Spec 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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder toSpecΓ AlgebraicGeometry.Spec.map Hom.appTop	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toSpecΓ_naturality
toSpecΓ_preimage_basicOpen 📖	mathematical	—	CategoryTheory.Functor.obj Opens AlgebraicGeometry.Spec 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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' toSpecΓ PrimeSpectrum.basicOpen CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing basicOpen	—	AlgebraicGeometry.basicOpen_eq_of_affine preimage_basicOpen Hom.appTop.eq_1 toSpecΓ_appTop CategoryTheory.Iso.inv_hom_id_apply

AlgebraicGeometry.Spec

Definitions

Name	Category	Theorems
fullyFaithful 📖	CompOp	1 math math: map_preimage_unop
fullyFaithfulToLocallyRingedSpace 📖	CompOp	—
homEquiv 📖	CompOp	2 math math: homEquiv_apply, homEquiv_symm_apply
preimage 📖	CompOp	6 math math: preimage_id, preimage_comp_assoc, homEquiv_apply, preimage_map, map_preimage, preimage_comp
reflective 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Spec	—	CategoryTheory.Functor.FullyFaithful.faithful
full 📖	mathematical	—	CategoryTheory.Functor.Full Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Spec	—	CategoryTheory.Functor.FullyFaithful.full
homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat CommRingCat.instCategory EquivLike.toFunLike Equiv.instEquivLike homEquiv preimage	—	—
homEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv map	—	—
map_eq_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat CommRingCat.instCategory	—	map_id
map_inj 📖	mathematical	—	map	—	CategoryTheory.Functor.map_injective faithful
map_injective 📖	mathematical	—	Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec map	—	—
map_preimage 📖	mathematical	—	map preimage	—	CategoryTheory.Functor.map_preimage full
map_preimage_unop 📖	mathematical	—	map Opposite.unop CommRingCat Opposite.op Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.FullyFaithful.preimage Opposite CategoryTheory.Category.opposite AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Spec fullyFaithful	—	CategoryTheory.Functor.FullyFaithful.map_preimage
map_surjective 📖	mathematical	—	Quiver.Hom CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec map	—	map_preimage
preimage_comp 📖	mathematical	—	preimage CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat CommRingCat.instCategory	—	map_injective map_preimage map_comp
preimage_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory preimage AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' preimage_comp
preimage_id 📖	mathematical	—	preimage CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat CommRingCat.instCategory	—	map_injective map_preimage map_id
preimage_map 📖	mathematical	—	preimage map	—	map_injective map_preimage

AlgebraicGeometry.ΓSpec

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	9 math math: isIso_adjunction_counit, adjunction_counit_app', adjunction_counit_app, adjunction_unit_app, AlgebraicGeometry.instIsIsoSchemeAppUnitOppositeCommRingCatAdjunctionOfIsAffine, adjunction_homEquiv_apply, AlgebraicGeometry.ΓSpecIso_inv_ΓSpec_adjunction_homEquiv, adjunction_homEquiv_symm_apply, AlgebraicGeometry.ΓSpec_adjunction_homEquiv_eq
locallyRingedSpaceAdjunction 📖	CompOp	12 math math: locallyRingedSpaceAdjunction_counit_app, adjunction_counit_app', locallyRingedSpaceAdjunction_counit_app', toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app, locallyRingedSpaceAdjunction_homEquiv_apply', unop_locallyRingedSpaceAdjunction_counit_app', isIso_locallyRingedSpaceAdjunction_counit, adjunction_homEquiv_apply, locallyRingedSpaceAdjunction_homEquiv_apply, locallyRingedSpaceAdjunction_unit, adjunction_homEquiv_symm_apply, locallyRingedSpaceAdjunction_counit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjunction_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Spec CategoryTheory.Functor.rightOp AlgebraicGeometry.Scheme.Γ CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adjunction Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Spec TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.ΓSpecIso	—	—
adjunction_counit_app' 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Spec CategoryTheory.Functor.rightOp AlgebraicGeometry.Scheme.Γ CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adjunction AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.Spec.toLocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.Γ locallyRingedSpaceAdjunction	—	—
adjunction_homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Opposite CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CommRingCat.instCategory CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.rightOp AlgebraicGeometry.Scheme.Γ AlgebraicGeometry.Scheme.Spec EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv adjunction AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.Γ AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Spec.toLocallyRingedSpace locallyRingedSpaceAdjunction	—	—
adjunction_homEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.obj Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory AlgebraicGeometry.Scheme.Spec CategoryTheory.Functor.rightOp AlgebraicGeometry.Scheme.Γ EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Adjunction.homEquiv adjunction AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Spec.toLocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.Γ locallyRingedSpaceAdjunction AlgebraicGeometry.Scheme.Hom.toLRSHom	—	—
adjunction_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory CategoryTheory.Functor.rightOp AlgebraicGeometry.Scheme.Γ AlgebraicGeometry.Scheme.Spec CategoryTheory.Adjunction.unit adjunction AlgebraicGeometry.Scheme.toSpecΓ	—	—
isIso_adjunction_counit 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Spec CategoryTheory.Functor.rightOp AlgebraicGeometry.Scheme.Γ CategoryTheory.Functor.id CategoryTheory.Adjunction.counit adjunction	—	CategoryTheory.NatIso.isIso_of_isIso_app adjunction_counit_app CategoryTheory.isIso_op CategoryTheory.Iso.isIso_inv
isIso_locallyRingedSpaceAdjunction_counit 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory CategoryTheory.Functor.category CategoryTheory.Functor.comp AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.Spec.toLocallyRingedSpace CategoryTheory.Functor.rightOp AlgebraicGeometry.LocallyRingedSpace.Γ CategoryTheory.Functor.id CategoryTheory.Adjunction.counit locallyRingedSpaceAdjunction	—	CategoryTheory.Iso.isIso_inv
left_triangle 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.id Opposite AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.opposite AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.Γ Opposite.op CategoryTheory.Functor.comp CategoryTheory.Functor.rightOp AlgebraicGeometry.Spec.toLocallyRingedSpace TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom CategoryTheory.NatTrans.app AlgebraicGeometry.identityToΓSpec AlgebraicGeometry.PresheafedSpace.presheaf Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity AlgebraicGeometry.PresheafedSpace.Hom.c CategoryTheory.CategoryStruct.id	—	AlgebraicGeometry.LocallyRingedSpace.Γ_Spec_left_triangle
locallyRingedSpaceAdjunction_counit 📖	mathematical	—	CategoryTheory.Adjunction.counit AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory CategoryTheory.Functor.rightOp AlgebraicGeometry.LocallyRingedSpace.Γ AlgebraicGeometry.Spec.toLocallyRingedSpace locallyRingedSpaceAdjunction CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.op CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.NatIso.op AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity	—	—
locallyRingedSpaceAdjunction_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.Spec.toLocallyRingedSpace CategoryTheory.Functor.rightOp AlgebraicGeometry.LocallyRingedSpace.Γ CategoryTheory.Functor.id CategoryTheory.Adjunction.counit locallyRingedSpaceAdjunction Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.of CommRingCat.carrier CommRingCat.commRing CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top Opposite.unop TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring Opposite.op AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.op AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType	—	—
locallyRingedSpaceAdjunction_counit_app' 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.Spec.toLocallyRingedSpace CategoryTheory.Functor.rightOp AlgebraicGeometry.LocallyRingedSpace.Γ CategoryTheory.Functor.id CategoryTheory.Adjunction.counit locallyRingedSpaceAdjunction Opposite.op CommRingCat.of Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top CommRingCat.carrier Opposite.unop CommRingCat.commRing TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.op AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType	—	—
locallyRingedSpaceAdjunction_homEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Opposite CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CommRingCat.instCategory CategoryTheory.Functor.obj AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory CategoryTheory.Functor.rightOp AlgebraicGeometry.LocallyRingedSpace.Γ AlgebraicGeometry.Spec.toLocallyRingedSpace EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv locallyRingedSpaceAdjunction CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.id CategoryTheory.Functor.comp AlgebraicGeometry.Spec.locallyRingedSpaceObj Opposite.unop CategoryTheory.NatTrans.app AlgebraicGeometry.identityToΓSpec AlgebraicGeometry.Spec.locallyRingedSpaceMap Quiver.Hom.unop	—	—
locallyRingedSpaceAdjunction_homEquiv_apply' 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Opposite CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CommRingCat.instCategory CategoryTheory.Functor.obj AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory CategoryTheory.Functor.rightOp AlgebraicGeometry.LocallyRingedSpace.Γ Opposite.op CommRingCat.of AlgebraicGeometry.Spec.toLocallyRingedSpace EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv locallyRingedSpaceAdjunction Opposite.unop CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.id CategoryTheory.Functor.comp AlgebraicGeometry.Spec.locallyRingedSpaceObj CategoryTheory.NatTrans.app AlgebraicGeometry.identityToΓSpec AlgebraicGeometry.Spec.locallyRingedSpaceMap	—	—
locallyRingedSpaceAdjunction_unit 📖	mathematical	—	CategoryTheory.Adjunction.unit AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory CategoryTheory.Functor.rightOp AlgebraicGeometry.LocallyRingedSpace.Γ AlgebraicGeometry.Spec.toLocallyRingedSpace locallyRingedSpaceAdjunction AlgebraicGeometry.identityToΓSpec	—	—
right_triangle 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.LocallyRingedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.LocallyRingedSpace.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.id Opposite CommRingCat CategoryTheory.Category.opposite CommRingCat.instCategory AlgebraicGeometry.Spec.toLocallyRingedSpace Opposite.op CategoryTheory.Functor.comp CategoryTheory.Functor.rightOp AlgebraicGeometry.LocallyRingedSpace.Γ CategoryTheory.NatTrans.app AlgebraicGeometry.identityToΓSpec CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity CategoryTheory.CategoryStruct.id	—	AlgebraicGeometry.LocallyRingedSpace.comp_ring_hom_ext TopCat.ext PrimeSpectrum.ext Ideal.ext CommRingCat.Colimits.hasColimits_commRingCat IsLocalization.AtPrime.isLocalRing PrimeSpectrum.isPrime AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk IsLocalization.AtPrime.to_map_mem_maximal_iff le_top
toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top CommRingCat.carrier Opposite.unop Opposite.op CommRingCat.commRing TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.Spec.toLocallyRingedSpace TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.rightOp AlgebraicGeometry.LocallyRingedSpace.Γ EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv locallyRingedSpaceAdjunction AlgebraicGeometry.PresheafedSpace.presheaf CommRingCat.ofHom algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType CategoryTheory.NatTrans.app AlgebraicGeometry.PresheafedSpace.Hom.c AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.op AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace TopologicalSpace.Opens.map Quiver.Hom.unop CategoryTheory.Functor.map Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Quiver.Hom.op CategoryTheory.homOfLE le_top	—	le_top AlgebraicGeometry.StructureSheaf.algebraMap_self_map CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality unop_locallyRingedSpaceAdjunction_counit_app' CategoryTheory.Functor.rightOp_map_unop CategoryTheory.unop_comp CategoryTheory.Adjunction.homEquiv_counit Equiv.symm_apply_apply
toSpecΓ_of 📖	mathematical	—	AlgebraicGeometry.toSpecΓ CommRingCat.of CommRingCat.ofHom CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top CommRingCat.carrier Opposite.unop CommRingCat Opposite.op CommRingCat.commRing TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.PresheafedSpace.carrier CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.op AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace AlgebraicGeometry.Spec.toLocallyRingedSpace Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType	—	—
toSpecΓ_unop 📖	mathematical	—	AlgebraicGeometry.toSpecΓ Opposite.unop CommRingCat CommRingCat.ofHom CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top Opposite.op CommRingCat.commRing TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.PresheafedSpace.carrier CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.op AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace AlgebraicGeometry.Spec.toLocallyRingedSpace Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType	—	—
unop_locallyRingedSpaceAdjunction_counit_app' 📖	mathematical	—	Quiver.Hom.unop CommRingCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp AlgebraicGeometry.LocallyRingedSpace AlgebraicGeometry.LocallyRingedSpace.instCategory AlgebraicGeometry.Spec.toLocallyRingedSpace CategoryTheory.Functor.rightOp AlgebraicGeometry.LocallyRingedSpace.Γ Opposite.op CommRingCat.of CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit locallyRingedSpaceAdjunction CommRingCat.ofHom TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PrimeSpectrum.Top CommRingCat.carrier Opposite.unop CommRingCat.commRing TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.types CategoryTheory.Sheaf.val Opens.grothendieckTopology AlgebraicGeometry.structureSheafInType Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.SheafedSpace AlgebraicGeometry.SheafedSpace.instCategory AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.op AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.instCommRingObjOppositeOpensCarrierTopValStructureSheafInType Algebra.id algebraMap AlgebraicGeometry.instAlgebraObjOppositeOpensCarrierTopValStructureSheafInType	—	—

---

← Back to Index