PullbackCarrier

📁 Source: Mathlib/AlgebraicGeometry/PullbackCarrier.lean

Statistics

Metric	Count
Definitions SpecOfPoint, Triplet, SpecTensorTo, mk', ofPoint, s, tensor, tensorCongr, tensorInl, tensorInr, x, y, carrierEquiv, ofPointTensor	14
Theorems SpecTensorTo_SpecOfPoint, SpecMap_tensorInl_fromSpecResidueField, Spec_map_tensorInl_fromSpecResidueField, Spec_map_tensor_isPullback, Spec_ofPointTensor_SpecTensorTo, exists_preimage, ext, ext_iff, fst_SpecTensorTo_apply, hx, hy, instNontrivialCarrierTensor, isPullback_SpecMap_tensor, mk'_s, mk'_x, mk'_y, ofPoint_SpecTensorTo, ofPoint_s, ofPoint_x, ofPoint_y, snd_SpecTensorTo_apply, specTensorTo_base_fst, specTensorTo_base_snd, specTensorTo_fst, specTensorTo_fst_assoc, specTensorTo_snd, specTensorTo_snd_assoc, tensorCongr_inv, tensorCongr_refl, tensorCongr_symm, tensorCongr_trans, tensorCongr_trans_hom, tensorCongr_trans_hom_assoc, carrierEquiv_eq_iff, carrierEquiv_symm_fst, carrierEquiv_symm_snd, exists_preimage_pullback, forget_comparison_surjective, ofPointTensor_SpecTensorTo, ofPointTensor_SpecTensorTo_assoc, range_fst, range_fst_comp, range_map, range_snd, range_snd_comp, residueFieldCongr_inv_residueFieldMap_ofPoint, tensorCongr_SpecTensorTo, tensorCongr_SpecTensorTo_assoc, exists_preimage_of_isPullback, image_preimage_eq_of_isPullback, isEmpty_pullback_iff, isJointlySurjectivePreserving, pullbackComparison_forget_surjective, instFstScheme, instIsStableUnderBaseChangeScheme, instSndScheme	56
Total	70

AlgebraicGeometry.Scheme

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_preimage_of_isPullback 📖	—	CategoryTheory.IsPullback AlgebraicGeometry.Scheme instCategory DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom'	—	—	Pullback.instHasPullback Pullback.exists_preimage_pullback CategoryTheory.IsPullback.isoPullback_inv_fst CategoryTheory.IsPullback.isoPullback_inv_snd
image_preimage_eq_of_isPullback 📖	mathematical	CategoryTheory.IsPullback AlgebraicGeometry.Scheme instCategory	Set.image TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' Set.preimage	—	subset_antisymm Set.instAntisymmSubset Set.image_subset_iff Set.preimage_comp TopCat.coe_comp Hom.comp_base CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq Set.image_comp Set.image_mono Set.image_preimage_subset exists_preimage_of_isPullback
isEmpty_pullback_iff 📖	mathematical	—	IsEmpty TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme instCategory Pullback.instHasPullback Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom'	—	Pullback.instHasPullback Set.disjoint_iff_forall_ne Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq Pullback.exists_preimage_pullback isEmpty_pullback
isJointlySurjectivePreserving 📖	mathematical	—	IsJointlySurjectivePreserving	—	Pullback.instHasPullback Pullback.exists_preimage_pullback
pullbackComparison_forget_surjective 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme instCategory CategoryTheory.types forget CategoryTheory.Limits.pullback Pullback.instHasPullback CategoryTheory.Functor.map CategoryTheory.Limits.Types.hasLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.cospan CategoryTheory.Limits.pullbackComparison	—	Function.Surjective.of_comp_left CategoryTheory.Limits.Types.hasLimit UnivLE.small univLE_of_max UnivLE.self Pullback.instHasPullback Pullback.exists_preimage_pullback CategoryTheory.Limits.Types.pullbackIsoPullback_hom_fst CategoryTheory.types_comp_apply CategoryTheory.Limits.pullbackComparison_comp_fst CategoryTheory.Limits.Types.pullbackIsoPullback_hom_snd CategoryTheory.Limits.pullbackComparison_comp_snd CategoryTheory.injective_of_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom

AlgebraicGeometry.Scheme.Pullback

Definitions

Name	Category	Theorems
SpecOfPoint 📖	CompOp	1 math math: SpecTensorTo_SpecOfPoint
Triplet 📖	CompData	10 math math: Triplet.tensorCongr_trans_hom, carrierEquiv_eq_iff, carrierEquiv_symm_fst, carrierEquiv_symm_snd, Triplet.tensorCongr_trans, Triplet.tensorCongr_trans_hom_assoc, Triplet.Spec_ofPointTensor_SpecTensorTo, Triplet.tensorCongr_symm, Triplet.tensorCongr_refl, Triplet.tensorCongr_inv
carrierEquiv 📖	CompOp	2 math math: carrierEquiv_symm_fst, carrierEquiv_symm_snd
ofPointTensor 📖	CompOp	3 math math: ofPointTensor_SpecTensorTo_assoc, ofPointTensor_SpecTensorTo, Triplet.Spec_ofPointTensor_SpecTensorTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SpecTensorTo_SpecOfPoint 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Spec Triplet.tensor Triplet.ofPoint CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory instHasPullback TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' Triplet.SpecTensorTo SpecOfPoint	—	instHasPullback ofPointTensor_SpecTensorTo AlgebraicGeometry.Scheme.fromSpecResidueField_apply
carrierEquiv_eq_iff 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Spec Triplet.tensor Triplet TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.Spec.map CategoryTheory.Iso.inv Triplet.tensorCongr	—	AlgebraicGeometry.Spec.map_id
carrierEquiv_symm_fst 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory instHasPullback TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.fst Equiv Triplet AlgebraicGeometry.Spec Triplet.tensor EquivLike.toFunLike Equiv.instEquivLike Equiv.symm carrierEquiv Triplet.x	—	instHasPullback Triplet.fst_SpecTensorTo_apply
carrierEquiv_symm_snd 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory instHasPullback TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.snd Equiv Triplet AlgebraicGeometry.Spec Triplet.tensor EquivLike.toFunLike Equiv.instEquivLike Equiv.symm carrierEquiv Triplet.y	—	instHasPullback Triplet.snd_SpecTensorTo_apply
exists_preimage_pullback 📖	mathematical	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory instHasPullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	Triplet.exists_preimage
forget_comparison_surjective 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.types AlgebraicGeometry.Scheme.forget CategoryTheory.Limits.pullback instHasPullback CategoryTheory.Functor.map CategoryTheory.Limits.Types.hasLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.cospan CategoryTheory.Limits.pullbackComparison	—	AlgebraicGeometry.Scheme.pullbackComparison_forget_surjective
ofPointTensor_SpecTensorTo 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.residueField CategoryTheory.Limits.pullback instHasPullback Triplet.tensor Triplet.ofPoint AlgebraicGeometry.Spec.map ofPointTensor Triplet.SpecTensorTo AlgebraicGeometry.Scheme.fromSpecResidueField	—	instHasPullback CategoryTheory.Limits.pullback.hom_ext AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField CategoryTheory.Category.assoc Triplet.specTensorTo_fst Triplet.hx Triplet.hy CategoryTheory.Limits.hasPushoutVertPaste CategoryTheory.Limits.instHasPushoutComp CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CommRingCat.Colimits.hasColimits_commRingCat residueFieldCongr_inv_residueFieldMap_ofPoint CategoryTheory.Limits.pushout.inl_desc AlgebraicGeometry.Spec.map_comp Triplet.specTensorTo_snd CategoryTheory.Limits.pushout.inr_desc
ofPointTensor_SpecTensorTo_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.residueField CategoryTheory.Limits.pullback instHasPullback Triplet.tensor Triplet.ofPoint AlgebraicGeometry.Spec.map ofPointTensor Triplet.SpecTensorTo AlgebraicGeometry.Scheme.fromSpecResidueField	—	instHasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ofPointTensor_SpecTensorTo
range_fst 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory instHasPullback DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.fst Set.preimage	—	Set.ext instHasPullback CategoryTheory.Limits.pullback.condition Triplet.exists_preimage
range_fst_comp 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory instHasPullback DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.fst Set Set.instInter	—	instHasPullback Set.range_comp range_fst Set.image_preimage_eq_range_inter
range_map 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback instHasPullback DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.map Set Set.instInter Set.preimage CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd	—	Set.ext instHasPullback AlgebraicGeometry.Scheme.Hom.comp_apply CategoryTheory.Limits.limit.lift_π Triplet.exists_preimage CategoryTheory.Limits.hasLimitOfHasLimitsOfShape instHasPullbacks CategoryTheory.IsPullback.instHasPullbackFst CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv CategoryTheory.Iso.hom_inv_id_assoc
range_snd 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory instHasPullback DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.snd Set.preimage	—	Set.ext instHasPullback Triplet.exists_preimage
range_snd_comp 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory instHasPullback DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.snd Set Set.instInter	—	instHasPullback CategoryTheory.Limits.pullback.condition range_fst_comp
residueFieldCongr_inv_residueFieldMap_ofPoint 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory AlgebraicGeometry.Scheme.residueField Triplet.s Triplet.ofPoint Triplet.x CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory instHasPullback DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.residueFieldCongr Triplet.hx AlgebraicGeometry.Scheme.Hom.residueFieldMap CategoryTheory.Limits.pullback.fst Triplet.y Triplet.hy CategoryTheory.Limits.pullback.snd	—	instHasPullback Triplet.hx Triplet.hy CategoryTheory.Limits.pullback.condition CategoryTheory.Category.id_comp AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr CategoryTheory.Category.assoc
tensorCongr_SpecTensorTo 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec Triplet.tensor CategoryTheory.Limits.pullback instHasPullback AlgebraicGeometry.Spec.map CategoryTheory.Iso.hom CommRingCat CommRingCat.instCategory Triplet.tensorCongr Triplet.SpecTensorTo	—	instHasPullback AlgebraicGeometry.Spec.map_id CategoryTheory.Category.id_comp
tensorCongr_SpecTensorTo_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec Triplet.tensor AlgebraicGeometry.Spec.map CategoryTheory.Iso.hom CommRingCat CommRingCat.instCategory Triplet.tensorCongr CategoryTheory.Limits.pullback instHasPullback Triplet.SpecTensorTo	—	instHasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorCongr_SpecTensorTo

AlgebraicGeometry.Scheme.Pullback.Triplet

Definitions

Name	Category	Theorems
SpecTensorTo 📖	CompOp	15 math math: specTensorTo_fst, AlgebraicGeometry.Scheme.Pullback.SpecTensorTo_SpecOfPoint, specTensorTo_base_snd, AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo, snd_SpecTensorTo_apply, specTensorTo_fst_assoc, specTensorTo_snd, specTensorTo_snd_assoc, AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo_assoc, AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo_assoc, specTensorTo_base_fst, AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo, fst_SpecTensorTo_apply, Spec_ofPointTensor_SpecTensorTo, ofPoint_SpecTensorTo
mk' 📖	CompOp	3 math math: mk'_s, mk'_x, mk'_y
ofPoint 📖	CompOp	9 math math: ofPoint_x, AlgebraicGeometry.Scheme.Pullback.SpecTensorTo_SpecOfPoint, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo_assoc, AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo, Spec_ofPointTensor_SpecTensorTo, ofPoint_s, ofPoint_y, ofPoint_SpecTensorTo
s 📖	CompOp	7 math math: mk'_s, isPullback_SpecMap_tensor, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, hy, Spec_map_tensor_isPullback, hx, ofPoint_s
tensor 📖	CompOp	29 math math: specTensorTo_fst, tensorCongr_trans_hom, AlgebraicGeometry.Scheme.Pullback.SpecTensorTo_SpecOfPoint, isPullback_SpecMap_tensor, specTensorTo_base_snd, AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_eq_iff, snd_SpecTensorTo_apply, specTensorTo_fst_assoc, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst, Spec_map_tensor_isPullback, specTensorTo_snd, specTensorTo_snd_assoc, AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo_assoc, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd, tensorCongr_trans, AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo_assoc, tensorCongr_trans_hom_assoc, specTensorTo_base_fst, AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo, fst_SpecTensorTo_apply, Spec_ofPointTensor_SpecTensorTo, ofPoint_SpecTensorTo, Spec_map_tensorInl_fromSpecResidueField, tensorCongr_symm, tensorCongr_refl, tensorCongr_inv, SpecMap_tensorInl_fromSpecResidueField, instNontrivialCarrierTensor
tensorCongr 📖	CompOp	10 math math: tensorCongr_trans_hom, AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_eq_iff, tensorCongr_trans, AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo_assoc, tensorCongr_trans_hom_assoc, Spec_ofPointTensor_SpecTensorTo, tensorCongr_symm, tensorCongr_refl, tensorCongr_inv
tensorInl 📖	CompOp	6 math math: specTensorTo_fst, isPullback_SpecMap_tensor, specTensorTo_fst_assoc, Spec_map_tensor_isPullback, Spec_map_tensorInl_fromSpecResidueField, SpecMap_tensorInl_fromSpecResidueField
tensorInr 📖	CompOp	6 math math: isPullback_SpecMap_tensor, Spec_map_tensor_isPullback, specTensorTo_snd, specTensorTo_snd_assoc, Spec_map_tensorInl_fromSpecResidueField, SpecMap_tensorInl_fromSpecResidueField
x 📖	CompOp	15 math math: specTensorTo_fst, ofPoint_x, isPullback_SpecMap_tensor, specTensorTo_fst_assoc, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst, Spec_map_tensor_isPullback, hx, mk'_x, specTensorTo_base_fst, fst_SpecTensorTo_apply, ext_iff, exists_preimage, Spec_map_tensorInl_fromSpecResidueField, SpecMap_tensorInl_fromSpecResidueField
y 📖	CompOp	15 math math: isPullback_SpecMap_tensor, specTensorTo_base_snd, snd_SpecTensorTo_apply, AlgebraicGeometry.Scheme.Pullback.residueFieldCongr_inv_residueFieldMap_ofPoint, hy, Spec_map_tensor_isPullback, specTensorTo_snd, specTensorTo_snd_assoc, AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd, ext_iff, exists_preimage, ofPoint_y, Spec_map_tensorInl_fromSpecResidueField, SpecMap_tensorInl_fromSpecResidueField, mk'_y

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SpecMap_tensorInl_fromSpecResidueField 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec tensor AlgebraicGeometry.Scheme.residueField x AlgebraicGeometry.Spec.map tensorInl AlgebraicGeometry.Scheme.fromSpecResidueField y tensorInr	—	hx hy CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.residueFieldCongr_fromSpecResidueField CategoryTheory.Limits.pushout.condition
Spec_map_tensorInl_fromSpecResidueField 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec tensor AlgebraicGeometry.Scheme.residueField x AlgebraicGeometry.Spec.map tensorInl AlgebraicGeometry.Scheme.fromSpecResidueField y tensorInr	—	SpecMap_tensorInl_fromSpecResidueField
Spec_map_tensor_isPullback 📖	mathematical	—	CategoryTheory.IsPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec tensor AlgebraicGeometry.Scheme.residueField x y s AlgebraicGeometry.Spec.map tensorInl tensorInr CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.residueFieldCongr hx AlgebraicGeometry.Scheme.Hom.residueFieldMap hy	—	isPullback_SpecMap_tensor
Spec_ofPointTensor_SpecTensorTo 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.residueField tensor CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Pullback.instHasPullback DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' SpecTensorTo AlgebraicGeometry.Spec.map AlgebraicGeometry.Scheme.Hom.residueFieldMap ofPoint AlgebraicGeometry.Scheme.Pullback.ofPointTensor CategoryTheory.Iso.hom tensorCongr AlgebraicGeometry.Scheme.Pullback.Triplet ofPoint_SpecTensorTo AlgebraicGeometry.Scheme.fromSpecResidueField	—	CategoryTheory.IsPullback.hom_ext hx hy isPullback_SpecMap_tensor AlgebraicGeometry.Scheme.Pullback.instHasPullback ofPoint_SpecTensorTo CategoryTheory.cancel_mono AlgebraicGeometry.IsPreimmersion.instMonoScheme AlgebraicGeometry.Scheme.instIsPreimmersionFromSpecResidueField CategoryTheory.Category.assoc specTensorTo_fst AlgebraicGeometry.Scheme.Pullback.tensorCongr_SpecTensorTo_assoc AlgebraicGeometry.Scheme.Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc AlgebraicGeometry.Scheme.Pullback.ofPointTensor_SpecTensorTo_assoc specTensorTo_snd
exists_preimage 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.fst x CategoryTheory.Limits.pullback.snd y	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier instNontrivialCarrierTensor AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd
ext 📖	—	x y	—	—	—
ext_iff 📖	mathematical	—	x y	—	ext
fst_SpecTensorTo_apply 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Spec tensor SpecTensorTo x	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback SpecMap_tensorInl_fromSpecResidueField AlgebraicGeometry.Scheme.Hom.comp_apply CategoryTheory.Limits.limit.lift_π AlgebraicGeometry.Scheme.fromSpecResidueField_apply
hx 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' x s	—	—
hy 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' y s	—	—
instNontrivialCarrierTensor 📖	mathematical	—	Nontrivial CommRingCat.carrier tensor	—	CommRingCat.nontrivial_of_isPushout_of_isField Field.toIsField hx hy EuclideanDomain.toNontrivial CategoryTheory.IsPushout.of_hasPushout
isPullback_SpecMap_tensor 📖	mathematical	—	CategoryTheory.IsPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec tensor AlgebraicGeometry.Scheme.residueField x y s AlgebraicGeometry.Spec.map tensorInl tensorInr CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.residueFieldCongr hx AlgebraicGeometry.Scheme.Hom.residueFieldMap hy	—	AlgebraicGeometry.isPullback_SpecMap_pushout hx hy
mk'_s 📖	mathematical	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	s mk'	—	—
mk'_x 📖	mathematical	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	x mk'	—	—
mk'_y 📖	mathematical	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	y mk'	—	—
ofPoint_SpecTensorTo 📖	mathematical	—	ofPoint DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Spec tensor CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' SpecTensorTo	—	ext AlgebraicGeometry.Scheme.Pullback.instHasPullback fst_SpecTensorTo_apply snd_SpecTensorTo_apply
ofPoint_s 📖	mathematical	—	s ofPoint DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback
ofPoint_x 📖	mathematical	—	x ofPoint DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback
ofPoint_y 📖	mathematical	—	y ofPoint DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.snd	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback
snd_SpecTensorTo_apply 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.snd AlgebraicGeometry.Spec tensor SpecTensorTo y	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback SpecMap_tensorInl_fromSpecResidueField AlgebraicGeometry.Scheme.Hom.comp_apply CategoryTheory.Limits.limit.lift_π AlgebraicGeometry.Scheme.fromSpecResidueField_apply
specTensorTo_base_fst 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Spec tensor SpecTensorTo x	—	fst_SpecTensorTo_apply
specTensorTo_base_snd 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.Limits.pullback.snd AlgebraicGeometry.Spec tensor SpecTensorTo y	—	snd_SpecTensorTo_apply
specTensorTo_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec tensor CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Pullback.instHasPullback SpecTensorTo CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.residueField x AlgebraicGeometry.Spec.map tensorInl AlgebraicGeometry.Scheme.fromSpecResidueField	—	CategoryTheory.Limits.pullback.lift_fst AlgebraicGeometry.Scheme.Pullback.instHasPullback SpecMap_tensorInl_fromSpecResidueField
specTensorTo_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec tensor CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Pullback.instHasPullback SpecTensorTo CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Scheme.residueField x AlgebraicGeometry.Spec.map tensorInl AlgebraicGeometry.Scheme.fromSpecResidueField	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' specTensorTo_fst
specTensorTo_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec tensor CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Pullback.instHasPullback SpecTensorTo CategoryTheory.Limits.pullback.snd AlgebraicGeometry.Scheme.residueField y AlgebraicGeometry.Spec.map tensorInr AlgebraicGeometry.Scheme.fromSpecResidueField	—	CategoryTheory.Limits.pullback.lift_snd AlgebraicGeometry.Scheme.Pullback.instHasPullback SpecMap_tensorInl_fromSpecResidueField
specTensorTo_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec tensor CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme.Pullback.instHasPullback SpecTensorTo CategoryTheory.Limits.pullback.snd AlgebraicGeometry.Scheme.residueField y AlgebraicGeometry.Spec.map tensorInr AlgebraicGeometry.Scheme.fromSpecResidueField	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' specTensorTo_snd
tensorCongr_inv 📖	mathematical	—	CategoryTheory.Iso.inv CommRingCat CommRingCat.instCategory tensor tensorCongr CategoryTheory.Iso.hom AlgebraicGeometry.Scheme.Pullback.Triplet	—	—
tensorCongr_refl 📖	mathematical	—	tensorCongr refl AlgebraicGeometry.Scheme.Pullback.Triplet IsPreorder.toRefl IsEquiv.toIsPreorder eq_isEquiv CategoryTheory.Iso.refl CommRingCat CommRingCat.instCategory tensor	—	refl IsPreorder.toRefl IsEquiv.toIsPreorder eq_isEquiv
tensorCongr_symm 📖	mathematical	—	CategoryTheory.Iso.symm CommRingCat CommRingCat.instCategory tensor tensorCongr AlgebraicGeometry.Scheme.Pullback.Triplet	—	—
tensorCongr_trans 📖	mathematical	—	CategoryTheory.Iso.trans CommRingCat CommRingCat.instCategory tensor tensorCongr AlgebraicGeometry.Scheme.Pullback.Triplet	—	—
tensorCongr_trans_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory tensor CategoryTheory.Iso.hom tensorCongr AlgebraicGeometry.Scheme.Pullback.Triplet	—	—
tensorCongr_trans_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory tensor CategoryTheory.Iso.hom tensorCongr AlgebraicGeometry.Scheme.Pullback.Triplet	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorCongr_trans_hom

AlgebraicGeometry.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFstScheme 📖	mathematical	—	AlgebraicGeometry.Surjective CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst	—	CategoryTheory.MorphismProperty.pullback_fst AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeScheme
instIsStableUnderBaseChangeScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Surjective	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk' AlgebraicGeometry.instRespectsIsoSchemeSurjective AlgebraicGeometry.Scheme.Pullback.range_fst Set.preimage_univ
instSndScheme 📖	mathematical	—	AlgebraicGeometry.Surjective CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.snd	—	CategoryTheory.MorphismProperty.pullback_snd AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeScheme

---

← Back to Index