Basic

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

Statistics

Metric	Count
Definitions geometrically	1
Theorems fiber_of_geometrically, geometrically_eq_universally, geometrically_iff_forall_fiberToSpecResidueField, geometrically_iff_of_commRing, geometrically_iff_of_commRing_of_isClosedUnderIsomorphisms, geometrically_iff_of_isClosedUnderIsomorphisms, geometrically_inf, instIsStableUnderBaseChangeSchemeGeometrically, instIsZariskiLocalAtTargetGeometricallyOfIsClosedUnderIsomorphismsScheme, pullback_of_geometrically, pullback_of_geometrically', self_of_isIntegral_of_geometrically	12
Total	13

AlgebraicGeometry

Definitions

Name	Category	Theorems
geometrically 📖	CompOp	17 math math: GeometricallyIrreducible.geometrically_irreducibleSpace, instIsZariskiLocalAtTargetGeometricallyOfIsClosedUnderIsomorphismsScheme, geometrically_eq_universally, geometricallyReduced_iff, geometricallyIntegral_iff, GeometricallyReduced.geometrically_isReduced, GeometricallyIrreducible.eq_geometrically, geometricallyIrreducible_iff, instIsStableUnderBaseChangeSchemeGeometrically, geometrically_iff_forall_fiberToSpecResidueField, geometrically_inf, geometrically_iff_of_commRing_of_isClosedUnderIsomorphisms, geometrically_iff_of_commRing, GeometricallyIntegral.eq_geometrically, GeometricallyReduced.eq_geometrically, GeometricallyIntegral.geometrically_isIntegral, geometrically_iff_of_isClosedUnderIsomorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fiber_of_geometrically 📖	mathematical	geometrically	Scheme.Hom.fiber	—	pullback_of_geometrically CommRingCat.Colimits.hasColimits_commRingCat
geometrically_eq_universally 📖	mathematical	—	geometrically CategoryTheory.MorphismProperty.universally Scheme Scheme.instCategory	—	CategoryTheory.MorphismProperty.ext isField_of_isIntegral_of_subsingleton instIsAffineOfFiniteOfDiscreteTopologyCarrierCarrierCommRingCat Finite.of_subsingleton Subsingleton.discreteTopology CategoryTheory.IsPullback.of_iso CategoryTheory.IsPullback.flip CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id_assoc instIsIntegralSpecOfIsDomainCarrier instIsDomain Unique.instSubsingleton
geometrically_iff_forall_fiberToSpecResidueField 📖	mathematical	—	geometrically Scheme.Hom.fiber Spec Scheme.residueField Scheme.Hom.fiberToSpecResidueField	—	CategoryTheory.MorphismProperty.pullback_snd CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeSchemeGeometrically Equiv.surjective CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.Category.assoc CategoryTheory.IsPullback.flip CategoryTheory.IsPullback.of_bot Scheme.Pullback.instHasPullback CategoryTheory.Limits.limit.lift_π CategoryTheory.IsPullback.of_hasPullback
geometrically_iff_of_commRing 📖	mathematical	—	geometrically Spec CommRingCat.of	—	Spec.map_surjective
geometrically_iff_of_commRing_of_isClosedUnderIsomorphisms 📖	mathematical	—	geometrically Spec CommRingCat.of CategoryTheory.Limits.pullback Scheme Scheme.instCategory EuclideanDomain.toCommRing Field.toEuclideanDomain Spec.map CommRingCat.ofHom algebraMap CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Scheme.Pullback.instHasPullback	—	Scheme.Pullback.instHasPullback pullback_of_geometrically geometrically_iff_of_isClosedUnderIsomorphisms Spec.map_surjective
geometrically_iff_of_isClosedUnderIsomorphisms 📖	mathematical	—	geometrically CategoryTheory.Limits.pullback Scheme Scheme.instCategory Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain Scheme.Pullback.instHasPullback	—	Scheme.Pullback.instHasPullback pullback_of_geometrically CategoryTheory.ObjectProperty.prop_of_iso
geometrically_inf 📖	mathematical	—	geometrically CategoryTheory.ObjectProperty Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Pi.instMinForall_mathlib SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot Prop.instCompleteLinearOrder CategoryTheory.MorphismProperty CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	geometrically_eq_universally CategoryTheory.MorphismProperty.ext
instIsStableUnderBaseChangeSchemeGeometrically 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange Scheme Scheme.instCategory geometrically	—	geometrically_eq_universally CategoryTheory.MorphismProperty.universally_isStableUnderBaseChange
instIsZariskiLocalAtTargetGeometricallyOfIsClosedUnderIsomorphismsScheme 📖	mathematical	—	IsZariskiLocalAtTarget geometrically	—	geometrically_eq_universally universally_isZariskiLocalAtTarget IsIntegral.nonempty TopologicalSpace.IsOpenCover.exists_mem eq_top_iff CategoryTheory.ObjectProperty.prop_of_iso IsIntegral.of_isIso CategoryTheory.Iso.isIso_inv Equiv.subsingleton_congr CategoryTheory.Iso.isIso_hom
pullback_of_geometrically 📖	mathematical	geometrically	CategoryTheory.Limits.pullback Scheme Scheme.instCategory Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain Scheme.Pullback.instHasPullback	—	Scheme.Pullback.instHasPullback CategoryTheory.IsPullback.of_hasPullback
pullback_of_geometrically' 📖	mathematical	geometrically	CategoryTheory.Limits.pullback Scheme Scheme.instCategory Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain Scheme.Pullback.instHasPullback	—	Scheme.Pullback.instHasPullback CategoryTheory.IsPullback.flip CategoryTheory.IsPullback.of_hasPullback
self_of_isIntegral_of_geometrically 📖	—	geometrically	—	—	CategoryTheory.MorphismProperty.universally_le geometrically_eq_universally

---

← Back to Index