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	Scheme.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SetLike.instMembership TopologicalSpace.Opens.instSetLike SheafedSpace.instTopologicalSpaceCarrierCarrier Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Preorder.toLE IsAffineOpen CategoryTheory.CategoryStruct.comp TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.germ CategoryTheory.Functor.map Quiver.Hom.op 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 Subring.instSubringClass Function.Injective.hasLeftInverse AddTorsor.nonempty SubringClass.toSubsemiringClass 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	Scheme.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SetLike.instMembership TopologicalSpace.Opens.instSetLike SheafedSpace.instTopologicalSpaceCarrierCarrier Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Subring CommRingCat.carrier TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.presheaf NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing CommRingCat.commRing Subring.instPartialOrder RingHom.range CommRingCat.Hom.hom CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory Opposite.op TopCat.Presheaf.germ	—	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 📖	mathematical	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.carrier 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.basicOpen 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.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SetLike.instMembership TopologicalSpace.Opens.instSetLike SheafedSpace.instTopologicalSpaceCarrierCarrier Quiver.Hom Scheme CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Scheme.instCategory Scheme.Opens.toScheme CategoryTheory.CategoryStruct.comp Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.presheaf Spec.map Scheme.fromSpecStalk 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 TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SetLike.instMembership TopologicalSpace.Opens.instSetLike SheafedSpace.instTopologicalSpaceCarrierCarrier Quiver.Hom Scheme CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Scheme.instCategory Scheme.Opens.toScheme CategoryTheory.CategoryStruct.comp Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat PresheafedSpace.presheaf 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 TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SetLike.instMembership TopologicalSpace.Opens.instSetLike SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct 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	Scheme.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SetLike.instMembership TopologicalSpace.Opens.instSetLike SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory 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	4 math math: AlgebraicGeometry.instIsGermInjectiveOfIsIntegral, IsGermInjective.of_openCover, 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	—	Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.IsAffineOpen CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens 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	Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace 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 📖	mathematical	AlgebraicGeometry.Scheme.IsGermInjective CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion	AlgebraicGeometry.Scheme.IsGermInjective	—	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.Scheme.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.IsAffineOpen CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens 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