Basic

📁 Source: Mathlib/AlgebraicGeometry/AlgClosed/Basic.lean

Statistics

Metric	Count
Definitions pointEquivClosedPoint, pointOfClosedPoint, residueFieldIsoBase	3
Theorems SpecMap_residueFieldIsoBase_inv, SpecMap_residueFieldIsoBase_inv_assoc, ext_of_apply_closedPoint_eq, ext_of_apply_eq, pointEquivClosedPoint_apply_coe, pointEquivClosedPoint_symm_apply_coe, pointOfClosedPoint_apply, pointOfClosedPoint_comp, pointOfClosedPoint_comp_assoc	9
Total	12

AlgebraicGeometry

Definitions

Name	Category	Theorems
pointEquivClosedPoint 📖	CompOp	2 math math: pointEquivClosedPoint_apply_coe, pointEquivClosedPoint_symm_apply_coe
pointOfClosedPoint 📖	CompOp	4 math math: pointOfClosedPoint_comp_assoc, pointOfClosedPoint_apply, pointEquivClosedPoint_symm_apply_coe, pointOfClosedPoint_comp
residueFieldIsoBase 📖	CompOp	2 math math: SpecMap_residueFieldIsoBase_inv, SpecMap_residueFieldIsoBase_inv_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SpecMap_residueFieldIsoBase_inv 📖	mathematical	—	Spec.map CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain Scheme.residueField CategoryTheory.Iso.inv CommRingCat CommRingCat.instCategory residueFieldIsoBase CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec Scheme.fromSpecResidueField	—	Spec.map_preimage
SpecMap_residueFieldIsoBase_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec Scheme.residueField CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain Spec.map CategoryTheory.Iso.inv CommRingCat CommRingCat.instCategory residueFieldIsoBase Scheme.fromSpecResidueField	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' SpecMap_residueFieldIsoBase_inv
ext_of_apply_closedPoint_eq 📖	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain CategoryTheory.CategoryStruct.id 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' IsLocalRing.closedPoint Semifield.toCommSemiring Field.toSemifield Field.instIsLocalRing	—	—	Field.instIsLocalRing Equiv.injective
ext_of_apply_eq 📖	—	IsLocallyClosed TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier Dense DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain	—	—	LocallyOfFiniteType.jacobsonSpace instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing instIsJacobsonRingOfKrullDimLEOfNatNat PrimeSpectrum.instKrullDimLEOfNatNat isArtinian_of_fg_of_artinian' DivisionRing.instIsArtinianRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self ext_of_fromSpecResidueField_eq dense_iff_closure_eq JacobsonSpace.closure_inter_closedPoints_eq_closure CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso instIsIsoSchemeMapOfCommRingCat CategoryTheory.Iso.isIso_hom ext_of_apply_closedPoint_eq CategoryTheory.Category.assoc SpecMap_residueFieldIsoBase_inv CategoryTheory.Iso.inv_hom_id Spec.map_id Field.instIsLocalRing Scheme.fromSpecResidueField_apply
pointEquivClosedPoint_apply_coe 📖	mathematical	—	TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Set Set.instMembership closedPoints SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe Equiv Quiver.Hom Scheme CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id Set.Elem EquivLike.toFunLike Equiv.instEquivLike pointEquivClosedPoint CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' IsLocalRing.closedPoint Semifield.toCommSemiring Field.toSemifield Field.instIsLocalRing	—	—
pointEquivClosedPoint_symm_apply_coe 📖	mathematical	—	Quiver.Hom Scheme CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.id DFunLike.coe Equiv Set.Elem TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace closedPoints SheafedSpace.instTopologicalSpaceCarrierCarrier EquivLike.toFunLike Equiv.instEquivLike Equiv.symm pointEquivClosedPoint pointOfClosedPoint Set Set.instMembership	—	—
pointOfClosedPoint_apply 📖	mathematical	—	DFunLike.coe PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' pointOfClosedPoint	—	Scheme.fromSpecResidueField_apply
pointOfClosedPoint_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain pointOfClosedPoint CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id Spec.map_id
pointOfClosedPoint_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain pointOfClosedPoint	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' pointOfClosedPoint_comp

---

← Back to Index