Documentation

Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Properties on the underlying functions of morphisms of schemes. #

This file includes various results on properties of morphisms of schemes that come from properties of the underlying map of topological spaces, including

source
instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyInjective :
(AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Function.Injective).RespectsIso
Equations
source
instance AlgebraicGeometry.injective_isLocalAtTarget :
AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Function.Injective)
Equations
source
theorem AlgebraicGeometry.surjective_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
AlgebraicGeometry.Surjective f ↔ Function.Surjective ⇑f.val.base
source
class AlgebraicGeometry.Surjective {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
Prop

A morphism of schemes is surjective if the underlying map is.

Instances
    source
    theorem AlgebraicGeometry.Surjective.surj {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.Surjective f] :
    Function.Surjective ⇑f.val.base
    source
    theorem AlgebraicGeometry.surjective_eq_topologically :
    @AlgebraicGeometry.Surjective = AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective
    source
    theorem AlgebraicGeometry.Scheme.Hom.surjective {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.Surjective f] :
    Function.Surjective ⇑f.val.base
    source
    @[instance 100]
    instance AlgebraicGeometry.instSurjectiveOfIsIsoScheme {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] :
    AlgebraicGeometry.Surjective f
    Equations
    • ⋯ = ⋯
    source
    instance AlgebraicGeometry.instSurjectiveCompScheme {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.Surjective f] [AlgebraicGeometry.Surjective g] :
    AlgebraicGeometry.Surjective (CategoryTheory.CategoryStruct.comp f g)
    Equations
    • ⋯ = ⋯
    source
    theorem AlgebraicGeometry.Surjective.of_comp {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.Surjective (CategoryTheory.CategoryStruct.comp f g)] :
    AlgebraicGeometry.Surjective g
    source
    theorem AlgebraicGeometry.Surjective.comp_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.Surjective f] :
    AlgebraicGeometry.Surjective (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.Surjective g
    source
    instance AlgebraicGeometry.instRespectsIsoSchemeSurjective :
    CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.Surjective
    Equations
    source
    instance AlgebraicGeometry.surjective_isLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget @AlgebraicGeometry.Surjective
    Equations
    source
    instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenMap :
    (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsOpenMap).RespectsIso
    Equations
    source
    instance AlgebraicGeometry.isOpenMap_isLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsOpenMap)
    Equations
    source
    instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedMap :
    (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsClosedMap).RespectsIso
    Equations
    source
    instance AlgebraicGeometry.isClosedMap_isLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsClosedMap)
    Equations
    source
    instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyEmbedding :
    (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Embedding).RespectsIso
    Equations
    source
    instance AlgebraicGeometry.embedding_isLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Embedding)
    Equations
    source
    instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyOpenEmbedding :
    (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => OpenEmbedding).RespectsIso
    Equations
    source
    instance AlgebraicGeometry.openEmbedding_isLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => OpenEmbedding)
    Equations
    source
    instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyClosedEmbedding :
    (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => ClosedEmbedding).RespectsIso
    Equations
    source
    instance AlgebraicGeometry.closedEmbedding_isLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => ClosedEmbedding)
    Equations