Descent

📁 Source: Mathlib/AlgebraicGeometry/Morphisms/Descent.lean

Statistics

Metric	Count
Definitions	0
Theorems descendsAlong_of_affineAnd, descendsAlong, descendsAlong, descendsAlong_inf_quasiCompact, of_pullback_fst_of_isAffine, descendsAlong, descendsAlong_inf_quasiCompact, exists_hom_isAffine_of_isLocalAtSource, exists_hom_isAffine_of_isZariskiLocalAtSource, of_pullback_fst_Spec_of_codescendsAlong	10
Total	10

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_pullback_fst_Spec_of_codescendsAlong 📖	—	RingHom.CodescendsAlong CommRingCat.carrier CommRingCat.commRing CommRingCat.Hom.hom Spec Spec.map CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst	—	—	Scheme.Pullback.instHasPullback Spec.map_surjective RingHom.CodescendsAlong.algebraMap_tensorProduct CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.Iso.isIso_hom pullbackSpecIso_hom_fst

AlgebraicGeometry.HasAffineProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
descendsAlong_of_affineAnd 📖	mathematical	CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice AlgebraicGeometry.IsLocalIso AlgebraicGeometry.Surjective CommRingCat.carrier CommRingCat.commRing CommRingCat.Hom.hom RingHom.RespectsIso RingHom.CodescendsAlong	CategoryTheory.MorphismProperty.DescendsAlong AlgebraicGeometry.QuasiCompact	—	AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact instIsZariskiLocalAtTarget AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.isAffine_of_isAffineHom CategoryTheory.MorphismProperty.of_pullback_fst_of_descendsAlong affineAnd_le_isAffineHom AlgebraicGeometry.isAffine_Spec AlgebraicGeometry.of_pullback_fst_Spec_of_codescendsAlong CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion SpecMap_iff_of_affineAnd CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Limits.pullback.lift_fst CategoryTheory.Limits.pullback.map_isIso CategoryTheory.IsIso.id

AlgebraicGeometry.HasRingHomProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
descendsAlong 📖	mathematical	CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice AlgebraicGeometry.IsLocalIso AlgebraicGeometry.Surjective CommRingCat.carrier CommRingCat.commRing CommRingCat.Hom.hom RingHom.CodescendsAlong	CategoryTheory.MorphismProperty.DescendsAlong AlgebraicGeometry.QuasiCompact	—	AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact instIsZariskiLocalAtTarget AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.of_pullback_fst_Spec_of_codescendsAlong CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects instIsZariskiLocalAtSource Spec_iff AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Limits.pullback.lift_fst AlgebraicGeometry.IsZariskiLocalAtSource.comp AlgebraicGeometry.Scheme.pullback_map_isOpenImmersion AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.IsIso.id AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.Scheme.local_affine

AlgebraicGeometry.IsLocalAtTarget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
descendsAlong 📖	mathematical	AlgebraicGeometry.Spec	CategoryTheory.MorphismProperty.DescendsAlong AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong
descendsAlong_inf_quasiCompact 📖	mathematical	CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice AlgebraicGeometry.IsLocalIso AlgebraicGeometry.Surjective AlgebraicGeometry.Spec	CategoryTheory.MorphismProperty.DescendsAlong AlgebraicGeometry.QuasiCompact	—	AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact

AlgebraicGeometry.IsStableUnderBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_pullback_fst_of_isAffine 📖	—	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst	—	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Category.assoc CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.Iso.isIso_inv CategoryTheory.MorphismProperty.comp_mem CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso CategoryTheory.MorphismProperty.pullback_fst CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongCompOfHasPullbacksAlong CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks

AlgebraicGeometry.IsZariskiLocalAtTarget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
descendsAlong 📖	mathematical	AlgebraicGeometry.Spec	CategoryTheory.MorphismProperty.DescendsAlong AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.DescendsAlong.mk' CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange iff_of_openCover CategoryTheory.Limits.hasPullbackVertPaste CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.Category.comp_id CategoryTheory.Limits.pullbackAssoc_inv_fst_fst CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_fst CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd CategoryTheory.Limits.pullbackAssoc_inv_snd CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_snd_assoc CategoryTheory.MorphismProperty.pullback_snd CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.Iso.isIso_hom of_isPullback AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.instIsOpenImmersionF CategoryTheory.IsPullback.of_hasPullback AlgebraicGeometry.Scheme.local_affine
descendsAlong_inf_quasiCompact 📖	mathematical	CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice AlgebraicGeometry.IsLocalIso AlgebraicGeometry.Surjective AlgebraicGeometry.Spec	CategoryTheory.MorphismProperty.DescendsAlong AlgebraicGeometry.QuasiCompact	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback descendsAlong CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf AlgebraicGeometry.quasiCompact_isStableUnderBaseChange AlgebraicGeometry.Spec.map_surjective AlgebraicGeometry.quasiCompact_iff_compactSpace AlgebraicGeometry.quasiSeparatedSpace_of_isAffine AlgebraicGeometry.isAffine_Spec AlgebraicGeometry.Scheme.compactSpace_of_isAffine AlgebraicGeometry.Scheme.exists_hom_isAffine_of_isZariskiLocalAtSource AlgebraicGeometry.IsLocalIso.instIsZariskiLocalAtSource CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities AlgebraicGeometry.IsLocalIso.instIsMultiplicativeScheme CategoryTheory.Category.assoc CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.MorphismProperty.inf CategoryTheory.MorphismProperty.instRespectsOfRespectsLeftOfRespectsRight CategoryTheory.MorphismProperty.Respects.toRespectsLeft CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso CategoryTheory.MorphismProperty.Respects.toRespectsRight CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat CategoryTheory.Iso.isIso_inv CategoryTheory.MorphismProperty.comp_mem AlgebraicGeometry.instQuasiCompactOfIsAffineHom AlgebraicGeometry.isAffineHom_of_isAffine CategoryTheory.Limits.hasPullbackHorizPaste CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst CategoryTheory.MorphismProperty.pullback_fst CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongCompOfHasPullbacksAlong CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.instHasPullbacksAlongOfHasPullbacks CategoryTheory.MorphismProperty.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks

AlgebraicGeometry.Scheme

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_hom_isAffine_of_isLocalAtSource 📖	mathematical	—	AlgebraicGeometry.Surjective AlgebraicGeometry.IsAffine	—	exists_hom_isAffine_of_isZariskiLocalAtSource
exists_hom_isAffine_of_isZariskiLocalAtSource 📖	mathematical	—	AlgebraicGeometry.Surjective AlgebraicGeometry.IsAffine	—	IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete UnivLE.small UnivLE.self Cover.exists_eq instJointlySurjectivePrecoverage Hom.comp_apply CategoryTheory.Limits.Sigma.ι_desc AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover CategoryTheory.Limits.colimit.ι_desc AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion instIsOpenImmersionF AlgebraicGeometry.instIsAffineSigmaObjScheme Finite.of_fintype AlgebraicGeometry.instIsAffineXSchemeFiniteSubcover isAffine_affineCover

---

← Back to Index