SpreadingOut

📁 Source: Mathlib/AlgebraicGeometry/SpreadingOut.lean

Statistics

Metric	Count
Definitions IsGermInjective, IsGermInjectiveAt	2
Theorems of_openCover, cond, exists_germ_injective, exists_le_and_germ_injective, exists_lift_of_germInjective, exists_lift_of_germInjective_aux, injective_germ_basicOpen, instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion, instIsGermInjectiveOfIsIntegral, instIsGermInjectiveOfIsLocallyNoetherian, isGermInjectiveAt_iff_of_isOpenImmersion, spread_out_of_isGermInjective, spread_out_of_isGermInjective', spread_out_unique_of_isGermInjective, spread_out_unique_of_isGermInjective'	15
Total	17

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lift_of_germInjective 📖	mathematical	TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.presheaf CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op TopCat.Presheaf.germ	IsAffineOpen CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver LE.le.hom	—	CommRingCat.Colimits.hasColimits_commRingCat exists_lift_of_germInjective_aux Scheme.exists_le_and_germ_injective TopCat.Presheaf.germ_res Set.range_comp_subset_range Function.Injective.hasLeftInverse AddTorsor.nonempty SubringClass.toSubsemiringClass Subring.instSubringClass LE.le.trans CommRingCat.hom_ext RingHom.ext RingEquiv.apply_symm_apply RingEquiv.injective TopCat.Presheaf.germ_res_apply
exists_lift_of_germInjective_aux 📖	mathematical	TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopologicalSpace.Opens TopCat.str SetLike.instMembership TopologicalSpace.Opens.instSetLike CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.presheaf CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op Scheme.Opens TopCat.Presheaf.germ	Preorder.toLE SheafedSpace.instTopologicalSpaceCarrierCarrier Subring CommRingCat.carrier CommRing.toRing CommRingCat.commRing Subring.instPartialOrder RingHom.range CommRingCat.Hom.hom	—	CommRingCat.Colimits.hasColimits_commRingCat SetLike.mem_coe TopologicalSpace.Opens.coe_inf TopologicalSpace.Opens.coe_finset_inf Finset.inf_set_eq_iInter Set.iInter_congr_Prop inf_le_right DFunLike.congr_fun TopCat.Presheaf.germ_res_apply Algebra.map_top AlgHom.map_adjoin Algebra.adjoin_le_iff LE.le.trans inf_le_left Finset.inf_le TopCat.Presheaf.germ_exist CommRingCat.FilteredColimits.forget_preservesFilteredColimits
injective_germ_basicOpen 📖	—	TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike SheafedSpace.instTopologicalSpaceCarrierCarrier Scheme.basicOpen CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier TopCat.Presheaf.germ	—	—	CommRingCat.Colimits.hasColimits_commRingCat RingHom.instRingHomClass RingHom.injective_iff_ker_eq_bot RingHom.ker_eq_bot_iff_eq_zero IsAffineOpen.isLocalization_basicOpen IsLocalization.exists_mk'_eq Scheme.basicOpen_le TopCat.Presheaf.germ_res_apply RingHom.algebraMap_toAlgebra RingHom.mem_ker Ideal.mul_unit_mem_iff_mem isUnit_of_invertible IsLocalization.mk'_eq_mul_mk'_one IsLocalization.mk'_zero
instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion 📖	mathematical	—	Scheme.IsGermInjectiveAt 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'	—	CommRingCat.Colimits.hasColimits_commRingCat Scheme.exists_germ_injective IsAffineOpen.image_of_isOpenImmersion CategoryTheory.MorphismProperty.cancel_right_of_respectsIso CategoryTheory.MorphismProperty.injective_respectsIso IsOpenImmersion.instIsIsoCommRingCatStalkMap CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.Iso.isIso_inv Scheme.Hom.preimage_image_eq Scheme.Hom.germ_stalkMap Scheme.Hom.appIso_inv_app_assoc CategoryTheory.eqToHom_op TopCat.Presheaf.germ_res'
instIsGermInjectiveOfIsIntegral 📖	mathematical	—	Scheme.IsGermInjective	—	CommRingCat.Colimits.hasColimits_commRingCat Scheme.instJointlySurjectivePrecoverage Scheme.instIsOpenImmersionF Scheme.Cover.covers isAffineOpen_opensRange Scheme.isAffine_affineCover PrimeSpectrum.isPrime IsAffineOpen.isLocalization_stalk IsLocalization.injective Ideal.primeCompl_le_nonZeroDivisors IsDomain.to_noZeroDivisors IsIntegral.component_integral
instIsGermInjectiveOfIsLocallyNoetherian 📖	mathematical	—	Scheme.IsGermInjective	—	Scheme.IsGermInjective.Spec RingHom.instRingHomClass IsLocalization.map_eq_zero_iff Localization.isLocalization isNoetherianRing_iff_ideal_fg Ideal.subset_span pow_one mul_comm smul_eq_mul Submodule.mem_annihilator_span_singleton SetLike.le_def instIsConcreteLE Ideal.span_le SetLike.mem_coe Submonoid.coe_finset_prod Ideal.mem_of_dvd Finset.dvd_prod_of_mem Finset.mem_attach Scheme.IsGermInjective.of_openCover isLocallyNoetherian_Spec isLocallyNoetherian_of_isOpenImmersion Scheme.AffineOpenCover.instIsOpenImmersionF
isGermInjectiveAt_iff_of_isOpenImmersion 📖	mathematical	—	Scheme.IsGermInjectiveAt 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'	—	CommRingCat.Colimits.hasColimits_commRingCat Scheme.exists_le_and_germ_injective OrderIso.surjective CategoryTheory.MorphismProperty.cancel_right_of_respectsIso CategoryTheory.MorphismProperty.injective_respectsIso IsOpenImmersion.instIsIsoCommRingCatStalkMap CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.Iso.isIso_inv Scheme.Hom.preimage_image_eq Scheme.Hom.germ_stalkMap Scheme.Hom.appIso_inv_app_assoc CategoryTheory.eqToHom_op TopCat.Presheaf.germ_res' Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding Scheme.Hom.isOpenEmbedding instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion
spread_out_of_isGermInjective 📖	mathematical	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.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.presheaf Scheme.Hom.stalkMap TopCat.Presheaf.stalkSpecializes Inseparable.specializes SheafedSpace.instTopologicalSpaceCarrierCarrier Inseparable.of_eq	Scheme Scheme.instCategory Spec Spec.map Scheme.fromSpecStalk Scheme.Opens.toScheme Scheme.Opens.fromSpecStalkOfMem Scheme.Opens.ι	—	CommRingCat.Colimits.hasColimits_commRingCat Inseparable.specializes Inseparable.of_eq TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open Scheme.isBasis_affineOpens Set.mem_univ isOpen_univ TopologicalSpace.Opens.is_open' Scheme.Hom.appLE.eq_1 CategoryTheory.Category.assoc TopCat.Presheaf.germ_res_assoc Scheme.Hom.germ_stalkMap_assoc Specializes.mem_open TopologicalSpace.Opens.isOpen TopCat.Presheaf.germ_stalkSpecializes_assoc Scheme.Hom.germ_stalkMap exists_lift_of_germInjective Scheme.Hom.finiteType_appLE Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc Spec.map_comp_assoc Spec.map_comp IsAffineOpen.fromSpecStalk.eq_1 IsAffineOpen.fromSpecStalk_eq_fromSpecStalk IsAffineOpen.SpecMap_appLE_fromSpec IsAffineOpen.isoSpec_hom CategoryTheory.Iso.eq_inv_comp IsAffineOpen.isoSpec_inv_ι_assoc
spread_out_of_isGermInjective' 📖	mathematical	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace PresheafedSpace.presheaf Scheme.fromSpecStalk	Scheme.Opens.toScheme Scheme.Opens.fromSpecStalkOfMem Scheme.Opens.ι	—	CommRingCat.Colimits.hasColimits_commRingCat LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf spread_out_of_isGermInjective Scheme.Hom.comp_apply Scheme.fromSpecStalk_closedPoint Spec.map_injective Inseparable.specializes Inseparable.of_eq CategoryTheory.cancel_mono IsPreimmersion.instMonoScheme instIsPreimmersionFromSpecStalk Spec.map_comp CategoryTheory.Category.assoc Scheme.SpecMap_stalkMap_fromSpecStalk Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc Scheme.SpecMap_stalkSpecializes_fromSpecStalk Scheme.Spec_stalkClosedPointTo_fromSpecStalk
spread_out_unique_of_isGermInjective 📖	mathematical	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.stalkMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.presheaf TopCat.Presheaf.stalkSpecializes Inseparable.specializes SheafedSpace.instTopologicalSpaceCarrierCarrier Inseparable.of_eq	Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike Scheme Scheme.instCategory Scheme.Opens.toScheme Scheme.Opens.ι	—	CommRingCat.Colimits.hasColimits_commRingCat Inseparable.specializes Inseparable.of_eq TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open Scheme.isBasis_affineOpens Set.mem_univ isOpen_univ Scheme.exists_le_and_germ_injective LE.le.trans inf_le_left Scheme.Hom.resLE_comp_ι inf_le_right CategoryTheory.ConcreteCategory.mono_of_injective CategoryTheory.cancel_mono CategoryTheory.Category.assoc TopCat.Presheaf.germ_res' Specializes.mem_open TopologicalSpace.Opens.isOpen TopCat.Presheaf.germ_stalkSpecializes_assoc Scheme.Hom.germ_stalkMap IsOpenImmersion.mono IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_hom Scheme.Opens.instIsOpenImmersionι Scheme.Hom.le_resLE_preimage_iff le_rfl Scheme.toSpecΓ_naturality Scheme.Hom.app_eq_appLE Scheme.Hom.resLE_appLE Scheme.Hom.image_top_eq_opensRange Scheme.Opens.opensRange_ι
spread_out_unique_of_isGermInjective' 📖	mathematical	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.carrier SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace PresheafedSpace.presheaf Scheme.fromSpecStalk	TopCat.carrier Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike SheafedSpace.instTopologicalSpaceCarrierCarrier Scheme.Opens.toScheme Scheme.Opens.ι	—	CommRingCat.Colimits.hasColimits_commRingCat spread_out_unique_of_isGermInjective LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf Scheme.fromSpecStalk_closedPoint Spec.map_injective Inseparable.specializes Inseparable.of_eq CategoryTheory.cancel_mono IsPreimmersion.instMonoScheme instIsPreimmersionFromSpecStalk Scheme.SpecMap_stalkMap_fromSpecStalk Spec.map_comp CategoryTheory.Category.assoc Scheme.SpecMap_stalkSpecializes_fromSpecStalk

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
IsGermInjective 📖	MathDef	3 math math: AlgebraicGeometry.instIsGermInjectiveOfIsIntegral, IsGermInjective.Spec, AlgebraicGeometry.instIsGermInjectiveOfIsLocallyNoetherian
IsGermInjectiveAt 📖	CompData	2 math math: AlgebraicGeometry.instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion, AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_germ_injective 📖	mathematical	—	AlgebraicGeometry.IsAffineOpen CommRingCat.carrier 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 TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier TopCat.Presheaf.germ	—	IsGermInjectiveAt.cond
exists_le_and_germ_injective 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	AlgebraicGeometry.IsAffineOpen Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier TopCat.Presheaf.germ	—	CommRingCat.Colimits.hasColimits_commRingCat IsGermInjectiveAt.cond AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le AlgebraicGeometry.IsAffineOpen.basicOpen AlgebraicGeometry.injective_germ_basicOpen

AlgebraicGeometry.Scheme.IsGermInjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_openCover 📖	—	AlgebraicGeometry.Scheme.IsGermInjective CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion	—	—	AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage AlgebraicGeometry.Scheme.Cover.covers AlgebraicGeometry.instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion AlgebraicGeometry.Scheme.instIsOpenImmersionF

AlgebraicGeometry.Scheme.IsGermInjectiveAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cond 📖	mathematical	—	AlgebraicGeometry.IsAffineOpen CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier TopCat.Presheaf.germ	—	—

---

← Back to Index