UnderlyingMap

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

Statistics

Metric	Count
Definitions `IsDominant`, `cover`, `instUniqueI₀SchemeCover`	3
Theorems `comp_iff`, `denseRange`, `isZariskiLocalAtTarget`, `of_comp`, `of_comp_of_isOpenImmersion`, `respectsIso`, `cover_I₀`, `cover_X`, `cover_f`, `denseRange`, `surjective`, `comp_iff`, `of_comp`, `sigmaDesc_of_union_range_eq_univ`, `surj`, `dominant_eq_topologically`, `injective_isStableUnderComposition`, `injective_isZariskiLocalAtTarget`, `instHasOfPrecompPropertySchemeSurjective`, `instIsDominantCompScheme`, `instIsDominantOfSurjective`, `instIsMultiplicativeSchemeIsDominant`, `instIsMultiplicativeSchemeSurjective`, `instIsZariskiLocalAtSourceTopologicallyGeneralizingMap`, `instIsZariskiLocalAtSourceTopologicallyIsOpenMap`, `instIsZariskiLocalAtTargetTopologicallyGeneralizingMap`, `instRespectsIsoSchemeSurjective`, `instRespectsIsoSchemeTopologicallyGeneralizingMap`, `instRespectsIsoSchemeTopologicallyInjective`, `instRespectsIsoSchemeTopologicallyIsClosedEmbedding`, `instRespectsIsoSchemeTopologicallyIsClosedMap`, `instRespectsIsoSchemeTopologicallyIsEmbedding`, `instRespectsIsoSchemeTopologicallyIsOpenEmbedding`, `instRespectsIsoSchemeTopologicallyIsOpenMap`, `instSurjectiveCompScheme`, `instSurjectiveDescI₀SchemeF`, `instSurjectiveOfIsIsoScheme`, `instSurjectiveOfNonemptyOfSubsingletonCarrierCarrierCommRingCat`, `isClosedEmbedding_isZariskiLocalAtTarget`, `isClosedMap_isZariskiLocalAtTarget`, `isDominant_iff`, `isEmbedding_isZariskiLocalAtTarget`, `isOpenEmbedding_isZariskiLocalAtTarget`, `isOpenMap_isZariskiLocalAtTarget`, `mem_range_iff_of_surjective`, `range_eq_range_of_surjective`, `range_eq_univ`, `specializingMap_isZariskiLocalAtTarget`, `specializingMap_respectsIso`, `surjective_eq_topologically`, `surjective_iff`, `surjective_isZariskiLocalAtTarget`, `surjective_of_isDominant_of_isClosed_range`	53
Total	56

AlgebraicGeometry

Definitions

Name	Category	Theorems
`IsDominant` 📖	CompData	19 math math: `IsDominant.respectsIso`, `instIsDominantιCoborderRange`, `instIsDominantOfSurjective`, `Scheme.PartialMap.Opens.isDominant_homOfLE`, `IsDominant.of_comp`, `isDominant_of_of_appTop_injective`, `Scheme.instIsDominantToImageOfQuasiCompact`, `isDominant_iff`, `IsDominant.isZariskiLocalAtTarget`, `instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat`, `instIsMultiplicativeSchemeIsDominant`, `isSchemeTheoreticallyDominant_iff_isDominant`, `Scheme.PartialMap.Opens.isDominant_ι`, `instIsDominantOfIsSchemeTheoreticallyDominantOfQuasiCompact`, `IsDominant.comp_iff`, `instIsDominantCompScheme`, `dominant_eq_topologically`, `Scheme.Hom.instIsDominantToNormalization`, `IsDominant.of_comp_of_isOpenImmersion`
`instUniqueI₀SchemeCover` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dominant_eq_topologically` 📖	mathematical	—	`IsDominant` `topologically` `DenseRange`	—	`isDominant_iff`
`injective_isStableUnderComposition` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `Scheme` `Scheme.instCategory` `topologically`	—	—
`injective_isZariskiLocalAtTarget` 📖	mathematical	—	`IsZariskiLocalAtTarget` `topologically`	—	`topologically_isZariskiLocalAtTarget` `instRespectsIsoSchemeTopologicallyInjective` `Function.Injective.restrictPreimage`
`instHasOfPrecompPropertySchemeSurjective` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasOfPrecompProperty` `Scheme` `Scheme.instCategory` `Surjective`	—	`Surjective.of_comp`
`instIsDominantCompScheme` 📖	mathematical	—	`IsDominant` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory`	—	`DenseRange.comp` `Scheme.Hom.denseRange` `Scheme.Hom.continuous`
`instIsDominantOfSurjective` 📖	mathematical	—	`IsDominant`	—	`Function.Surjective.denseRange` `Scheme.Hom.surjective`
`instIsMultiplicativeSchemeIsDominant` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `Scheme` `Scheme.instCategory` `IsDominant`	—	`instIsDominantOfSurjective` `instSurjectiveOfIsIsoScheme` `CategoryTheory.IsIso.id` `instIsDominantCompScheme`
`instIsMultiplicativeSchemeSurjective` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `Scheme` `Scheme.instCategory` `Surjective`	—	`instSurjectiveOfIsIsoScheme` `CategoryTheory.IsIso.id` `Surjective.surj`
`instIsZariskiLocalAtSourceTopologicallyGeneralizingMap` 📖	mathematical	—	`IsZariskiLocalAtSource` `topologically` `GeneralizingMap`	—	`topologically_isZariskiLocalAtSource'` `instRespectsIsoSchemeTopologicallyGeneralizingMap` `TopologicalSpace.IsOpenCover.generalizingMap_iff_comp`
`instIsZariskiLocalAtSourceTopologicallyIsOpenMap` 📖	mathematical	—	`IsZariskiLocalAtSource` `topologically` `IsOpenMap`	—	`topologically_isZariskiLocalAtSource'` `instRespectsIsoSchemeTopologicallyIsOpenMap` `TopologicalSpace.IsOpenCover.isOpenMap_iff_comp`
`instIsZariskiLocalAtTargetTopologicallyGeneralizingMap` 📖	mathematical	—	`IsZariskiLocalAtTarget` `topologically` `GeneralizingMap`	—	`topologically_isZariskiLocalAtTarget'` `instRespectsIsoSchemeTopologicallyGeneralizingMap` `TopologicalSpace.IsOpenCover.generalizingMap_iff_restrictPreimage`
`instRespectsIsoSchemeSurjective` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `Surjective`	—	`topologically_respectsIso` `Homeomorph.surjective` `surjective_eq_topologically`
`instRespectsIsoSchemeTopologicallyGeneralizingMap` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `topologically` `GeneralizingMap`	—	`topologically_respectsIso` `Topology.IsInducing.generalizingMap` `Topology.IsEmbedding.toIsInducing` `Topology.IsOpenEmbedding.toIsEmbedding` `Homeomorph.isOpenEmbedding` `IsOpen.stableUnderGeneralization` `Topology.IsOpenEmbedding.isOpen_range` `GeneralizingMap.comp`
`instRespectsIsoSchemeTopologicallyInjective` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `topologically`	—	`topologically_respectsIso` `Homeomorph.injective`
`instRespectsIsoSchemeTopologicallyIsClosedEmbedding` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `topologically` `Topology.IsClosedEmbedding`	—	`topologically_respectsIso` `Homeomorph.isClosedEmbedding` `Topology.IsClosedEmbedding.comp`
`instRespectsIsoSchemeTopologicallyIsClosedMap` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `topologically` `IsClosedMap`	—	`topologically_respectsIso` `Homeomorph.isClosedMap` `IsClosedMap.comp`
`instRespectsIsoSchemeTopologicallyIsEmbedding` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `topologically` `Topology.IsEmbedding`	—	`topologically_respectsIso` `Homeomorph.isEmbedding` `Topology.IsEmbedding.comp`
`instRespectsIsoSchemeTopologicallyIsOpenEmbedding` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `topologically` `Topology.IsOpenEmbedding`	—	`topologically_respectsIso` `Homeomorph.isOpenEmbedding` `Topology.IsOpenEmbedding.comp`
`instRespectsIsoSchemeTopologicallyIsOpenMap` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `topologically` `IsOpenMap`	—	`topologically_respectsIso` `Homeomorph.isOpenMap` `IsOpenMap.comp`
`instSurjectiveCompScheme` 📖	mathematical	—	`Surjective` `CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory`	—	`Scheme.Hom.surjective`
`instSurjectiveDescI₀SchemeF` 📖	mathematical	—	`Surjective` `CategoryTheory.Limits.sigmaObj` `CategoryTheory.PreZeroHypercover.I₀` `Scheme` `Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `Scheme.precoverage` `CategoryTheory.PreZeroHypercover.X` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.Sigma.desc` `CategoryTheory.PreZeroHypercover.f`	—	`Surjective.sigmaDesc_of_union_range_eq_univ` `UnivLE.small` `UnivLE.self` `Scheme.Cover.iUnion_range` `Scheme.instJointlySurjectivePrecoverage`
`instSurjectiveOfIsIsoScheme` 📖	mathematical	—	`Surjective`	—	`Homeomorph.surjective`
`instSurjectiveOfNonemptyOfSubsingletonCarrierCarrierCommRingCat` 📖	mathematical	—	`Surjective`	—	`Function.surjective_to_subsingleton`
`isClosedEmbedding_isZariskiLocalAtTarget` 📖	mathematical	—	`IsZariskiLocalAtTarget` `topologically` `Topology.IsClosedEmbedding`	—	`topologically_isZariskiLocalAtTarget'` `instRespectsIsoSchemeTopologicallyIsClosedEmbedding` `TopologicalSpace.IsOpenCover.isClosedEmbedding_iff_restrictPreimage`
`isClosedMap_isZariskiLocalAtTarget` 📖	mathematical	—	`IsZariskiLocalAtTarget` `topologically` `IsClosedMap`	—	`topologically_isZariskiLocalAtTarget'` `instRespectsIsoSchemeTopologicallyIsClosedMap` `TopologicalSpace.IsOpenCover.isClosedMap_iff_restrictPreimage`
`isDominant_iff` 📖	mathematical	—	`IsDominant` `DenseRange` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	—	—
`isEmbedding_isZariskiLocalAtTarget` 📖	mathematical	—	`IsZariskiLocalAtTarget` `topologically` `Topology.IsEmbedding`	—	`topologically_isZariskiLocalAtTarget'` `instRespectsIsoSchemeTopologicallyIsEmbedding` `TopologicalSpace.IsOpenCover.isEmbedding_iff_restrictPreimage`
`isOpenEmbedding_isZariskiLocalAtTarget` 📖	mathematical	—	`IsZariskiLocalAtTarget` `topologically` `Topology.IsOpenEmbedding`	—	`topologically_isZariskiLocalAtTarget'` `instRespectsIsoSchemeTopologicallyIsOpenEmbedding` `TopologicalSpace.IsOpenCover.isOpenEmbedding_iff_restrictPreimage`
`isOpenMap_isZariskiLocalAtTarget` 📖	mathematical	—	`IsZariskiLocalAtTarget` `topologically` `IsOpenMap`	—	`topologically_isZariskiLocalAtTarget'` `instRespectsIsoSchemeTopologicallyIsOpenMap` `TopologicalSpace.IsOpenCover.isOpenMap_iff_restrictPreimage`
`mem_range_iff_of_surjective` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory`	`TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Set` `Set.instMembership` `Set.range` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	—	`range_eq_range_of_surjective`
`range_eq_range_of_surjective` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory`	`Set.range` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	—	`Set.range_comp` `range_eq_univ` `Set.image_univ`
`range_eq_univ` 📖	mathematical	—	`Set.range` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `Set.univ`	—	`Scheme.Hom.surjective`
`specializingMap_isZariskiLocalAtTarget` 📖	mathematical	—	`IsZariskiLocalAtTarget` `topologically` `SpecializingMap`	—	`topologically_isZariskiLocalAtTarget` `specializingMap_respectsIso` `specializingMap_iff_closure_singleton_subset` `Set.image_singleton` `TopologicalSpace.Opens.mem_iSup` `TopologicalSpace.Opens.mem_top` `IsOpen.stableUnderGeneralization` `TopologicalSpace.Opens.is_open'` `specializes_iff_mem_closure` `Set.image_congr` `closure_subtype`
`specializingMap_respectsIso` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `Scheme` `Scheme.instCategory` `topologically` `SpecializingMap`	—	`topologically_respectsIso` `IsClosedMap.specializingMap` `Homeomorph.isClosedMap` `SpecializingMap.comp`
`surjective_eq_topologically` 📖	mathematical	—	`Surjective` `topologically`	—	`surjective_iff`
`surjective_iff` 📖	mathematical	—	`Surjective` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	—	—
`surjective_isZariskiLocalAtTarget` 📖	mathematical	—	`IsZariskiLocalAtTarget` `Surjective`	—	`instRespectsIsoSchemeSurjective` `surjective_eq_topologically` `topologically_isZariskiLocalAtTarget` `Function.Surjective.restrictPreimage`
`surjective_of_isDominant_of_isClosed_range` 📖	mathematical	—	`Surjective`	—	`Set.range_eq_univ` `IsClosed.closure_eq` `DenseRange.closure_range` `Scheme.Hom.denseRange`

AlgebraicGeometry.IsDominant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_iff` 📖	mathematical	—	`AlgebraicGeometry.IsDominant` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`of_comp` `AlgebraicGeometry.instIsDominantCompScheme`
`denseRange` 📖	mathematical	—	`DenseRange` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `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'`	—	—
`isZariskiLocalAtTarget` 📖	mathematical	—	`AlgebraicGeometry.IsZariskiLocalAtTarget` `AlgebraicGeometry.IsDominant`	—	`respectsIso` `AlgebraicGeometry.dominant_eq_topologically` `AlgebraicGeometry.topologically_isZariskiLocalAtTarget'` `TopologicalSpace.IsOpenCover.denseRange_iff_restrictPreimage`
`of_comp` 📖	mathematical	—	`AlgebraicGeometry.IsDominant`	—	`AlgebraicGeometry.isDominant_iff` `denseRange_iff_closure_range` `Set.univ_subset_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `closure_mono` `Set.range_comp_subset_range`
`of_comp_of_isOpenImmersion` 📖	mathematical	—	`AlgebraicGeometry.IsDominant`	—	`AlgebraicGeometry.isDominant_iff` `DenseRange.eq_1` `Set.preimage_image_eq` `Topology.IsEmbedding.injective` `Topology.IsOpenEmbedding.toIsEmbedding` `AlgebraicGeometry.Scheme.Hom.isOpenEmbedding` `Dense.preimage` `Set.range_comp` `Topology.IsOpenEmbedding.isOpenMap`
`respectsIso` 📖	mathematical	—	`CategoryTheory.MorphismProperty.RespectsIso` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsDominant`	—	`CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `AlgebraicGeometry.instIsMultiplicativeSchemeIsDominant` `AlgebraicGeometry.instIsDominantOfSurjective` `AlgebraicGeometry.instSurjectiveOfIsIsoScheme`

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
`cover` 📖	CompOp	4 math math: `cover_X`, `cover_f`, `cover_I₀`, `AlgebraicGeometry.QuasiCompactCover.homCover`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cover_I₀` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.I₀` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `cover`	—	—
`cover_X` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `cover`	—	—
`cover_f` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.f` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `cover`	—	—
`denseRange` 📖	mathematical	—	`DenseRange` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'`	—	`AlgebraicGeometry.IsDominant.denseRange`
`surjective` 📖	mathematical	—	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'`	—	`AlgebraicGeometry.Surjective.surj`

AlgebraicGeometry.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_iff` 📖	mathematical	—	`AlgebraicGeometry.Surjective` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`of_comp` `AlgebraicGeometry.instSurjectiveCompScheme`
`of_comp` 📖	mathematical	—	`AlgebraicGeometry.Surjective`	—	`Function.Surjective.of_comp` `AlgebraicGeometry.Scheme.Hom.surjective`
`sigmaDesc_of_union_range_eq_univ` 📖	mathematical	`Set.iUnion` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `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` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `Set.univ`	`AlgebraicGeometry.Surjective` `CategoryTheory.Limits.sigmaObj` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `AlgebraicGeometry.Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `CategoryTheory.Limits.Sigma.desc`	—	`AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `AlgebraicGeometry.Scheme.Hom.comp_apply` `CategoryTheory.Limits.Sigma.ι_desc`
`surj` 📖	mathematical	—	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `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'`	—	—

---

← Back to Index