RationalMap

📁 Source: Mathlib/AlgebraicGeometry/RationalMap.lean

Statistics

Metric	Count
Definitions toPartialMap, toRationalMap, PartialMap, IsOver, compHom, domain, equiv, fromFunctionField, fromSpecStalkOfMem, hom, instSetoid, ofFromSpecStalk, restrict, toRationalMap, RationalMap, IsOver, compHom, domain, equivFunctionField, equivFunctionFieldOver, fromFunctionField, ofFunctionField, openCoverDomain, toPartialMap, «term_⤏_»	25
Theorems toPartialMap_domain, toPartialMap_hom, isDominant_homOfLE, isDominant_ι, compHom_domain, compHom_hom, dense_domain, equiv_iff_of_domain_eq_of_isSeparated, equiv_iff_of_isSeparated, equiv_iff_of_isSeparated_of_le, equiv_of_fromSpecStalkOfMem_eq, equiv_toPartialMap_iff_of_isSeparated, equivalence_rel, exists_restrict_isOver, ext, ext_iff, fromFunctionField_restrict, fromSpecStalkOfMem_compHom, fromSpecStalkOfMem_ofFromSpecStalk, fromSpecStalkOfMem_restrict, fromSpecStalkOfMem_toPartialMap, instIsOverCompHomOfIsOver, instIsOverRestrict, instIsOverToPartialMapOfIsOver, instIsReducedToScheme, isOver_iff, isOver_iff_eq_restrict, isOver_toRationalMap_iff_of_isSeparated, le_domain_toRationalMap, mem_domain_ofFromSpecStalk, ofFromSpecStalk_comp, restrict_domain, restrict_equiv, restrict_hom, restrict_id, restrict_id_hom, restrict_restrict, restrict_restrict_hom, restrict_toRationalMap, toPartialMap_toRationalMap_restrict, toRationalMap_eq_iff, toRationalMap_surjective, exists_partialMap_over, compHom_toRationalMap, dense_domain, eq_of_fromFunctionField_eq, exists_partialMap_over, exists_rep, fromFunctionField_ofFunctionField, fromFunctionField_toRationalMap, isOver_iff, mem_domain, toRationalMap_toPartialMap, instIsOverCompHomOfIsOver, instIsOverToPartialMapOfIsSeparatedOfIsOver, instIsOverToRationalMapOfIsOver	56
Total	81

AlgebraicGeometry

Definitions

Name	Category	Theorems
«term_⤏_» 📖	CompOp	—

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
PartialMap 📖	CompData	2 math math: PartialMap.toRationalMap_surjective, PartialMap.equivalence_rel
RationalMap 📖	CompOp	1 math math: PartialMap.toRationalMap_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsOverCompHomOfIsOver 📖	mathematical	—	RationalMap.IsOver RationalMap.compHom	—	RationalMap.exists_partialMap_over PartialMap.instIsOverCompHomOfIsOver
instIsOverToPartialMapOfIsSeparatedOfIsOver 📖	mathematical	—	PartialMap.IsOver RationalMap.toPartialMap	—	PartialMap.isOver_toRationalMap_iff_of_isSeparated RationalMap.toRationalMap_toPartialMap
instIsOverToRationalMapOfIsOver 📖	mathematical	—	RationalMap.IsOver PartialMap.toRationalMap	—	—

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
toPartialMap 📖	CompOp	6 math math: toPartialMap_hom, toPartialMap_domain, AlgebraicGeometry.Scheme.PartialMap.equiv_toPartialMap_iff_of_isSeparated, AlgebraicGeometry.Scheme.PartialMap.isOver_iff_eq_restrict, AlgebraicGeometry.Scheme.PartialMap.instIsOverToPartialMapOfIsOver, AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_toPartialMap
toRationalMap 📖	CompOp	1 math math: AlgebraicGeometry.Scheme.RationalMap.isOver_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toPartialMap_domain 📖	mathematical	—	AlgebraicGeometry.Scheme.PartialMap.domain toPartialMap Top.top AlgebraicGeometry.Scheme.Opens OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
toPartialMap_hom 📖	mathematical	—	AlgebraicGeometry.Scheme.PartialMap.hom toPartialMap CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme Top.top AlgebraicGeometry.Scheme.Opens OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CategoryTheory.Iso.hom AlgebraicGeometry.Scheme.topIso	—	—

AlgebraicGeometry.Scheme.PartialMap

Definitions

Name	Category	Theorems
IsOver 📖	MathDef	10 math math: AlgebraicGeometry.Scheme.RationalMap.IsOver.exists_partialMap_over, instIsOverRestrict, instIsOverCompHomOfIsOver, isOver_iff_eq_restrict, AlgebraicGeometry.Scheme.instIsOverToPartialMapOfIsSeparatedOfIsOver, isOver_iff, instIsOverToPartialMapOfIsOver, isOver_toRationalMap_iff_of_isSeparated, exists_restrict_isOver, AlgebraicGeometry.Scheme.RationalMap.exists_partialMap_over
compHom 📖	CompOp	6 math math: compHom_domain, instIsOverCompHomOfIsOver, isOver_iff_eq_restrict, AlgebraicGeometry.Scheme.RationalMap.compHom_toRationalMap, isOver_iff, compHom_hom
domain 📖	CompOp	16 math math: ext_iff, compHom_domain, AlgebraicGeometry.Scheme.Hom.toPartialMap_domain, toPartialMap_toRationalMap_restrict, equiv_toPartialMap_iff_of_isSeparated, restrict_id, equiv_iff_of_isSeparated, ofFromSpecStalk_comp, isOver_iff_eq_restrict, mem_domain_ofFromSpecStalk, isOver_iff, dense_domain, le_domain_toRationalMap, compHom_hom, AlgebraicGeometry.Scheme.RationalMap.mem_domain, restrict_id_hom
equiv 📖	MathDef	8 math math: equiv_toPartialMap_iff_of_isSeparated, equivalence_rel, equiv_iff_of_isSeparated, equiv_of_fromSpecStalkOfMem_eq, equiv_iff_of_domain_eq_of_isSeparated, toRationalMap_eq_iff, restrict_equiv, equiv_iff_of_isSeparated_of_le
fromFunctionField 📖	CompOp	2 math math: fromFunctionField_restrict, AlgebraicGeometry.Scheme.RationalMap.fromFunctionField_toRationalMap
fromSpecStalkOfMem 📖	CompOp	4 math math: fromSpecStalkOfMem_compHom, fromSpecStalkOfMem_restrict, fromSpecStalkOfMem_ofFromSpecStalk, fromSpecStalkOfMem_toPartialMap
hom 📖	CompOp	12 math math: AlgebraicGeometry.Scheme.Hom.toPartialMap_hom, ext_iff, toPartialMap_toRationalMap_restrict, equiv_toPartialMap_iff_of_isSeparated, equiv_iff_of_isSeparated, ofFromSpecStalk_comp, restrict_hom, restrict_restrict_hom, isOver_iff, equiv_iff_of_isSeparated_of_le, compHom_hom, restrict_id_hom
instSetoid 📖	CompOp	—
ofFromSpecStalk 📖	CompOp	3 math math: ofFromSpecStalk_comp, mem_domain_ofFromSpecStalk, fromSpecStalkOfMem_ofFromSpecStalk
restrict 📖	CompOp	16 math math: instIsOverRestrict, toPartialMap_toRationalMap_restrict, restrict_id, equiv_iff_of_isSeparated, fromFunctionField_restrict, isOver_iff_eq_restrict, restrict_hom, fromSpecStalkOfMem_restrict, restrict_restrict_hom, restrict_restrict, restrict_toRationalMap, restrict_equiv, equiv_iff_of_isSeparated_of_le, restrict_domain, exists_restrict_isOver, restrict_id_hom
toRationalMap 📖	CompOp	14 math math: AlgebraicGeometry.Scheme.RationalMap.IsOver.exists_partialMap_over, toRationalMap_surjective, toPartialMap_toRationalMap_restrict, AlgebraicGeometry.Scheme.RationalMap.toRationalMap_toPartialMap, AlgebraicGeometry.Scheme.instIsOverToRationalMapOfIsOver, AlgebraicGeometry.Scheme.RationalMap.fromFunctionField_toRationalMap, AlgebraicGeometry.Scheme.RationalMap.compHom_toRationalMap, toRationalMap_eq_iff, restrict_toRationalMap, isOver_toRationalMap_iff_of_isSeparated, le_domain_toRationalMap, AlgebraicGeometry.Scheme.RationalMap.mem_domain, AlgebraicGeometry.Scheme.RationalMap.exists_partialMap_over, AlgebraicGeometry.Scheme.RationalMap.exists_rep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compHom_domain 📖	mathematical	—	domain compHom	—	—
compHom_hom 📖	mathematical	—	hom compHom CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme domain	—	—
dense_domain 📖	mathematical	—	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike domain	—	—
equiv_iff_of_domain_eq_of_isSeparated 📖	mathematical	domain	equiv	—	dense_domain le_rfl Eq.le equiv_iff_of_isSeparated_of_le AlgebraicGeometry.Scheme.homOfLE_rfl CategoryTheory.Category.id_comp
equiv_iff_of_isSeparated 📖	mathematical	—	equiv hom restrict AlgebraicGeometry.Scheme.Opens SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier domain Dense.inter_of_isOpen_left SetLike.coe TopologicalSpace.Opens.instSetLike dense_domain TopologicalSpace.Opens.is_open' inf_le_left inf_le_right	—	equiv_iff_of_isSeparated_of_le Dense.inter_of_isOpen_left dense_domain TopologicalSpace.Opens.is_open' inf_le_left inf_le_right
equiv_iff_of_isSeparated_of_le 📖	mathematical	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder domain	equiv hom restrict	—	inf_le_left Opens.isDominant_homOfLE Dense.inter_of_isOpen_left TopologicalSpace.Opens.is_open' AlgebraicGeometry.ext_of_isDominant_of_isSeparated' instIsReducedToScheme instIsOverRestrict LE.le.trans AlgebraicGeometry.Scheme.homOfLE_homOfLE_assoc inf_le_right
equiv_of_fromSpecStalkOfMem_eq 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier domain fromSpecStalkOfMem	equiv	—	CommRingCat.Colimits.hasColimits_commRingCat Dense.inter_of_isOpen_left dense_domain TopologicalSpace.Opens.is_open' AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι inf_le_left inf_le_right AlgebraicGeometry.spread_out_unique_of_isGermInjective' AlgebraicGeometry.instIsIsoSchemeMapOfCommRingCat AlgebraicGeometry.Spec.map_inv CategoryTheory.Category.assoc CategoryTheory.IsIso.hom_inv_id_assoc fromSpecStalkOfMem_restrict IsOpen.dense IrreducibleSpace.toPreirreducibleSpace LE.le.trans LE.le.trans_eq Set.image_subset_range Subtype.range_val CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom CategoryTheory.cancel_mono AlgebraicGeometry.IsOpenImmersion.mono AlgebraicGeometry.Scheme.homOfLE_ι AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι
equiv_toPartialMap_iff_of_isSeparated 📖	mathematical	—	equiv AlgebraicGeometry.Scheme.Hom.toPartialMap hom CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme domain AlgebraicGeometry.Scheme.Opens.ι	—	Dense.inter_of_isOpen_left dense_domain TopologicalSpace.Opens.is_open' inf_le_left inf_le_right equiv_iff_of_isSeparated instIsOverToPartialMapOfIsOver inf_top_eq CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom AlgebraicGeometry.Scheme.homOfLE_ι_assoc AlgebraicGeometry.Scheme.isoOfEq_hom_ι_assoc
equivalence_rel 📖	mathematical	—	AlgebraicGeometry.Scheme.PartialMap equiv	—	dense_domain AlgebraicGeometry.Scheme.homOfLE_rfl CategoryTheory.Category.id_comp Dense.inter_of_isOpen_left TopologicalSpace.Opens.is_open' LE.le.trans inf_le_left inf_le_right AlgebraicGeometry.Scheme.homOfLE_homOfLE CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.homOfLE_homOfLE_assoc
exists_restrict_isOver 📖	mathematical	—	IsOver restrict	—	AlgebraicGeometry.Scheme.RationalMap.IsOver.exists_partialMap_over toRationalMap_eq_iff IsOver.eq_1 instIsOverRestrict
ext 📖	—	domain hom CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme CategoryTheory.Iso.hom AlgebraicGeometry.Scheme.isoOfEq	—	—	ext_iff
ext_iff 📖	mathematical	—	hom CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme domain CategoryTheory.Iso.hom AlgebraicGeometry.Scheme.isoOfEq	—	AlgebraicGeometry.Scheme.isoOfEq_rfl CategoryTheory.Category.id_comp
fromFunctionField_restrict 📖	mathematical	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder domain	fromFunctionField restrict	—	fromSpecStalkOfMem_restrict AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat
fromSpecStalkOfMem_compHom 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier domain compHom	fromSpecStalkOfMem CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.Category.assoc
fromSpecStalkOfMem_ofFromSpecStalk 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.fromSpecStalk	fromSpecStalkOfMem ofFromSpecStalk mem_domain_ofFromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.spread_out_of_isGermInjective'
fromSpecStalkOfMem_restrict 📖	mathematical	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder domain SetLike.instMembership	fromSpecStalkOfMem restrict	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Scheme.homOfLE_base CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc Inseparable.specializes Inseparable.of_eq AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk TopCat.Presheaf.stalkCongr_inv CategoryTheory.Iso.eq_inv_comp CategoryTheory.IsIso.comp_inv_eq CategoryTheory.IsIso.eq_inv_comp AlgebraicGeometry.Scheme.homOfLE_ι AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom ContinuousMap.map_specializes AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_assoc AlgebraicGeometry.Scheme.Hom.stalkMap_comp
fromSpecStalkOfMem_toPartialMap 📖	mathematical	—	fromSpecStalkOfMem AlgebraicGeometry.Scheme.Hom.toPartialMap CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.fromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_ι_assoc
instIsOverCompHomOfIsOver 📖	mathematical	—	IsOver compHom	—	CategoryTheory.comp_over CategoryTheory.instHomIsOverComp
instIsOverRestrict 📖	mathematical	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder domain	IsOver restrict	—	CategoryTheory.comp_over CategoryTheory.instHomIsOverComp CategoryTheory.instHomIsOverOfIsOverTower_1 CategoryTheory.instIsOverTower_2 AlgebraicGeometry.instIsOverHomOfLE
instIsOverToPartialMapOfIsOver 📖	mathematical	—	IsOver AlgebraicGeometry.Scheme.Hom.toPartialMap	—	CategoryTheory.comp_over CategoryTheory.instHomIsOverComp CategoryTheory.instHomIsOverOfIsOverTower CategoryTheory.instIsOverTower_2 CategoryTheory.instIsOverTower AlgebraicGeometry.Scheme.Opens.instIsOverι
instIsReducedToScheme 📖	mathematical	—	AlgebraicGeometry.IsReduced AlgebraicGeometry.Scheme.Opens.toScheme	—	AlgebraicGeometry.isReduced_of_isOpenImmersion AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι
isOver_iff 📖	mathematical	—	IsOver hom compHom CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.Opens.toScheme domain AlgebraicGeometry.Scheme.Opens.ι	—	CategoryTheory.comp_over CategoryTheory.instHomIsOverOfIsOverTower CategoryTheory.instIsOverTower_2 CategoryTheory.instIsOverTower AlgebraicGeometry.Scheme.Opens.instIsOverι
isOver_iff_eq_restrict 📖	mathematical	—	IsOver compHom CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass restrict AlgebraicGeometry.Scheme.Hom.toPartialMap domain dense_domain	—	dense_domain AlgebraicGeometry.Scheme.isoOfEq_rfl CategoryTheory.comp_over CategoryTheory.instHomIsOverOfIsOverTower CategoryTheory.instIsOverTower_2 CategoryTheory.instIsOverTower AlgebraicGeometry.Scheme.Opens.instIsOverι CategoryTheory.instHomIsOverOfIsOverTower_1 AlgebraicGeometry.instIsOverHomOfLE CategoryTheory.instHomIsOverId
isOver_toRationalMap_iff_of_isSeparated 📖	mathematical	—	AlgebraicGeometry.Scheme.RationalMap.IsOver toRationalMap IsOver	—	exists_restrict_isOver isOver_iff Opens.isDominant_homOfLE AlgebraicGeometry.ext_of_isDominant instIsReducedToScheme CategoryTheory.comp_over CategoryTheory.instHomIsOverOfIsOverTower CategoryTheory.instIsOverTower_2 CategoryTheory.instIsOverTower AlgebraicGeometry.Scheme.Opens.instIsOverι CategoryTheory.instHomIsOverOfIsOverTower_1 AlgebraicGeometry.instIsOverHomOfLE CategoryTheory.Category.assoc CategoryTheory.HomIsOver.comp_over AlgebraicGeometry.Scheme.instIsOverToRationalMapOfIsOver
le_domain_toRationalMap 📖	mathematical	—	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier domain AlgebraicGeometry.Scheme.RationalMap.domain toRationalMap	—	le_sSup
mem_domain_ofFromSpecStalk 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.fromSpecStalk	TopCat.carrier AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier domain ofFromSpecStalk	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.spread_out_of_isGermInjective'
ofFromSpecStalk_comp 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf AlgebraicGeometry.Scheme.fromSpecStalk	AlgebraicGeometry.Scheme.Opens.toScheme domain ofFromSpecStalk hom AlgebraicGeometry.Scheme.Opens.ι	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.spread_out_of_isGermInjective'
restrict_domain 📖	mathematical	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder domain	restrict	—	—
restrict_equiv 📖	mathematical	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder domain	equiv restrict	—	le_rfl AlgebraicGeometry.Scheme.homOfLE_rfl CategoryTheory.Category.id_comp
restrict_hom 📖	mathematical	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder domain	hom restrict CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.homOfLE	—	—
restrict_id 📖	mathematical	—	restrict domain dense_domain le_rfl AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	ext dense_domain le_rfl AlgebraicGeometry.Scheme.homOfLE_rfl CategoryTheory.Category.id_comp AlgebraicGeometry.Scheme.isoOfEq_rfl
restrict_id_hom 📖	mathematical	—	hom restrict domain dense_domain le_rfl AlgebraicGeometry.Scheme.Opens PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	dense_domain le_rfl AlgebraicGeometry.Scheme.homOfLE_rfl CategoryTheory.Category.id_comp
restrict_restrict 📖	mathematical	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder domain	restrict LE.le.trans	—	ext LE.le.trans AlgebraicGeometry.Scheme.homOfLE_homOfLE_assoc AlgebraicGeometry.Scheme.isoOfEq_rfl CategoryTheory.Category.id_comp
restrict_restrict_hom 📖	mathematical	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder domain	hom restrict LE.le.trans	—	LE.le.trans AlgebraicGeometry.Scheme.homOfLE_homOfLE_assoc
restrict_toRationalMap 📖	mathematical	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder domain	toRationalMap restrict	—	toRationalMap_eq_iff restrict_equiv
toPartialMap_toRationalMap_restrict 📖	mathematical	—	hom restrict AlgebraicGeometry.Scheme.RationalMap.toPartialMap toRationalMap domain dense_domain le_domain_toRationalMap	—	dense_domain le_domain_toRationalMap AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms equiv_iff_of_domain_eq_of_isSeparated AlgebraicGeometry.instHasTerminalScheme AlgebraicGeometry.Scheme.instIsSeparatedOfIsSeparated AlgebraicGeometry.instIsOverTerminalScheme toRationalMap_eq_iff ext_iff
toRationalMap_eq_iff 📖	mathematical	—	toRationalMap equiv	—	Quotient.eq
toRationalMap_surjective 📖	mathematical	—	AlgebraicGeometry.Scheme.PartialMap AlgebraicGeometry.Scheme.RationalMap toRationalMap	—	—

AlgebraicGeometry.Scheme.PartialMap.Opens

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDominant_homOfLE 📖	mathematical	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	AlgebraicGeometry.IsDominant AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.homOfLE	—	AlgebraicGeometry.Scheme.homOfLE_ι isDominant_ι AlgebraicGeometry.IsDominant.of_comp_of_isOpenImmersion AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι
isDominant_ι 📖	mathematical	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike	AlgebraicGeometry.IsDominant AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Opens.ι	—	AlgebraicGeometry.Scheme.Opens.range_ι

AlgebraicGeometry.Scheme.RationalMap

Definitions

Name	Category	Theorems
IsOver 📖	CompData	4 math math: AlgebraicGeometry.Scheme.instIsOverToRationalMapOfIsOver, AlgebraicGeometry.Scheme.instIsOverCompHomOfIsOver, AlgebraicGeometry.Scheme.PartialMap.isOver_toRationalMap_iff_of_isSeparated, isOver_iff
compHom 📖	CompOp	3 math math: AlgebraicGeometry.Scheme.instIsOverCompHomOfIsOver, compHom_toRationalMap, isOver_iff
domain 📖	CompOp	3 math math: dense_domain, AlgebraicGeometry.Scheme.PartialMap.le_domain_toRationalMap, mem_domain
equivFunctionField 📖	CompOp	—
equivFunctionFieldOver 📖	CompOp	—
fromFunctionField 📖	CompOp	2 math math: fromFunctionField_ofFunctionField, fromFunctionField_toRationalMap
ofFunctionField 📖	CompOp	1 math math: fromFunctionField_ofFunctionField
openCoverDomain 📖	CompOp	—
toPartialMap 📖	CompOp	3 math math: AlgebraicGeometry.Scheme.PartialMap.toPartialMap_toRationalMap_restrict, toRationalMap_toPartialMap, AlgebraicGeometry.Scheme.instIsOverToPartialMapOfIsSeparatedOfIsOver

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compHom_toRationalMap 📖	mathematical	—	AlgebraicGeometry.Scheme.PartialMap.toRationalMap AlgebraicGeometry.Scheme.PartialMap.compHom compHom	—	—
dense_domain 📖	mathematical	—	Dense TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike domain	—	Dense.mono AlgebraicGeometry.Scheme.PartialMap.le_domain_toRationalMap AlgebraicGeometry.Scheme.PartialMap.dense_domain
eq_of_fromFunctionField_eq 📖	—	fromFunctionField AlgebraicGeometry.irreducibleSpace_of_isIntegral	—	—	AlgebraicGeometry.irreducibleSpace_of_isIntegral exists_rep AlgebraicGeometry.Scheme.PartialMap.toRationalMap_eq_iff AlgebraicGeometry.Scheme.PartialMap.equiv_of_fromSpecStalkOfMem_eq AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat AlgebraicGeometry.instIsGermInjectiveOfIsIntegral
exists_partialMap_over 📖	mathematical	—	AlgebraicGeometry.Scheme.PartialMap.IsOver AlgebraicGeometry.Scheme.PartialMap.toRationalMap	—	IsOver.exists_partialMap_over
exists_rep 📖	mathematical	—	AlgebraicGeometry.Scheme.PartialMap.toRationalMap	—	—
fromFunctionField_ofFunctionField 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.functionField AlgebraicGeometry.irreducibleSpace_of_isIntegral TopCat.Presheaf.stalk CommRingCat CommRingCat.instCategory CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.PresheafedSpace.presheaf genericPoint TopCat.carrier AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat AlgebraicGeometry.Scheme.fromSpecStalk	fromFunctionField ofFunctionField	—	AlgebraicGeometry.irreducibleSpace_of_isIntegral CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_ofFromSpecStalk
fromFunctionField_toRationalMap 📖	mathematical	—	fromFunctionField AlgebraicGeometry.Scheme.PartialMap.toRationalMap AlgebraicGeometry.Scheme.PartialMap.fromFunctionField	—	—
isOver_iff 📖	mathematical	—	IsOver compHom CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass AlgebraicGeometry.Scheme.Hom.toRationalMap	—	exists_partialMap_over AlgebraicGeometry.Scheme.Hom.toRationalMap.eq_1 compHom_toRationalMap AlgebraicGeometry.Scheme.PartialMap.dense_domain AlgebraicGeometry.Scheme.PartialMap.isOver_iff_eq_restrict AlgebraicGeometry.Scheme.PartialMap.restrict_toRationalMap AlgebraicGeometry.Scheme.PartialMap.toRationalMap_surjective AlgebraicGeometry.Scheme.PartialMap.toRationalMap_eq_iff CategoryTheory.Category.assoc CategoryTheory.comp_over CategoryTheory.instHomIsOverOfIsOverTower CategoryTheory.instIsOverTower_2 CategoryTheory.instIsOverTower AlgebraicGeometry.Scheme.Opens.instIsOverι CategoryTheory.instHomIsOverOfIsOverTower_1 AlgebraicGeometry.instIsOverHomOfLE
mem_domain 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier domain AlgebraicGeometry.Scheme.PartialMap.domain AlgebraicGeometry.Scheme.PartialMap.toRationalMap	—	TopologicalSpace.Opens.mem_sSup
toRationalMap_toPartialMap 📖	mathematical	—	AlgebraicGeometry.Scheme.PartialMap.toRationalMap toPartialMap	—	AlgebraicGeometry.Scheme.PartialMap.toRationalMap_surjective AlgebraicGeometry.Scheme.PartialMap.dense_domain AlgebraicGeometry.Scheme.PartialMap.le_domain_toRationalMap AlgebraicGeometry.Scheme.PartialMap.restrict_toRationalMap AlgebraicGeometry.Scheme.PartialMap.ext AlgebraicGeometry.Scheme.isoOfEq_rfl CategoryTheory.Category.id_comp AlgebraicGeometry.Scheme.PartialMap.toPartialMap_toRationalMap_restrict

AlgebraicGeometry.Scheme.RationalMap.IsOver

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_partialMap_over 📖	mathematical	—	AlgebraicGeometry.Scheme.PartialMap.IsOver AlgebraicGeometry.Scheme.PartialMap.toRationalMap	—	—

---

← Back to Index