Structures · Geometry
AlgebraicGeometry.Surjective
A morphism of schemes is surjective if the underlying map is.
- Shape
- One type argument · adds surj
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Forgetful instances
Every AlgebraicGeometry.Surjective is also a
Provided automatically by
Concrete types that are instances3
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.AffineSpace
- CategoryTheory.Limits.sigmaObj
How is a type an instance?
Loading the hierarchy index…
Assumed by37
- AlgebraicGeometry.Scheme.Hom.surjective
- AlgebraicGeometry.Scheme.Hom.cover
- AlgebraicGeometry.Surjective.surj
- AlgebraicGeometry.range_eq_univ
- AlgebraicGeometry.UniversallyClosed.of_comp_surjective
- AlgebraicGeometry.Scheme.Hom.presieve₀_cover
- AlgebraicGeometry.Scheme.Hom.singleton_mem_propQCPrecoverage
- AlgebraicGeometry.Scheme.Hom.singleton_mem_qcPrecoverage
- AlgebraicGeometry.isIso_of_isClosedImmersion_of_surjective
- AlgebraicGeometry.Flat.isQuotientMap_of_surjective
- AlgebraicGeometry.range_eq_range_of_surjective
- AlgebraicGeometry.Surjective.of_comp
- AlgebraicGeometry.Flat.isIso_of_surjective_of_mono
- AlgebraicGeometry.Flat.epi_of_flat_of_surjective
- AlgebraicGeometry.instIsDominantOfSurjective
- AlgebraicGeometry.Scheme.Hom.cover.congr_simp
- AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfQuasiCompact
- AlgebraicGeometry.Scheme.Hom.singleton_mem_fppfPrecoverage
- AlgebraicGeometry.isRegularEpi_of_flat_of_surjective_of_isAffine
- AlgebraicGeometry.Scheme.instEffectiveEpiOfQuasiCompactOfSurjectiveOfFlat
- AlgebraicGeometry.Surjective.instSndScheme
- AlgebraicGeometry.instUniqueI₀SchemeCover
- AlgebraicGeometry.instFaithfulOverSchemePullbackOfSurjectiveOfFlatOfLocallyOfFinitePresentation
- AlgebraicGeometry.QuasiCompactCover.homCover
- AlgebraicGeometry.QuasiCompactCover.singleton
- AlgebraicGeometry.Surjective.comp_iff
- AlgebraicGeometry.effectiveEpi_base_of_flat
- AlgebraicGeometry.instSurjectiveCompScheme
- AlgebraicGeometry.Scheme.Hom.cover_f
- AlgebraicGeometry.Scheme.Hom.cover_X
- AlgebraicGeometry.instGeometricallyIrreducibleCompSchemeOfIsOpenImmersionOfSurjective
- AlgebraicGeometry.Scheme.Hom.generate_singleton_mem_propQCTopology
- AlgebraicGeometry.Scheme.Hom.singleton_mem_fpqcPrecoverage
- AlgebraicGeometry.Surjective.instFstScheme
- AlgebraicGeometry.Scheme.Hom.cover_I₀
- AlgebraicGeometry.Scheme.instEffectiveEpiOfLocallyOfFinitePresentationOfSurjectiveOfFlat
- AlgebraicGeometry.mem_range_iff_of_surjective