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
class AlgebraicGeometry.Surjective {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
Prop

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

Instances
    source
    theorem AlgebraicGeometry.surjective_iff {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
    AlgebraicGeometry.Surjective f ↔ Function.Surjective ⇑f.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 Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.Surjective f] :
    Function.Surjective ⇑f.base
    source
    @[instance 100]
    instance AlgebraicGeometry.instSurjectiveOfIsIsoScheme {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] :
    AlgebraicGeometry.Surjective f
    Equations
    • ⋯ = ⋯
    source
    instance AlgebraicGeometry.instSurjectiveCompScheme {X Y 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 Y 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 Y 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
    @[simp]
    theorem AlgebraicGeometry.range_eq_univ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f] :
    Set.range ⇑f.base = Set.univ
    source
    theorem AlgebraicGeometry.range_eq_range_of_surjective {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) (e : X ⟶ Y) [AlgebraicGeometry.Surjective e] (hge : CategoryTheory.CategoryStruct.comp e g = f) :
    Set.range ⇑f.base = Set.range ⇑g.base
    source
    theorem AlgebraicGeometry.mem_range_iff_of_surjective {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) (e : X ⟶ Y) [AlgebraicGeometry.Surjective e] (hge : CategoryTheory.CategoryStruct.comp e g = f) (s : ↑↑S.toPresheafedSpace) :
    s ∈ Set.range ⇑f.base ↔ s ∈ Set.range ⇑g.base
    source
    instance AlgebraicGeometry.injective_isStableUnderComposition :
    (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) => Function.Injective x).IsStableUnderComposition
    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.instRespectsIsoSchemeTopologicallyIsEmbedding :
    (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsEmbedding).RespectsIso
    Equations
    source
    instance AlgebraicGeometry.isEmbedding_isLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsEmbedding)
    Equations
    source
    instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenEmbedding :
    (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding).RespectsIso
    Equations
    source
    instance AlgebraicGeometry.isOpenEmbedding_isLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding)
    Equations
    source
    instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedEmbedding :
    (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsClosedEmbedding).RespectsIso
    Equations
    source
    instance AlgebraicGeometry.isClosedEmbedding_isLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsClosedEmbedding)
    Equations
    source
    class AlgebraicGeometry.IsDominant {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
    Prop

    A morphism of schemes is dominant if the underlying map has dense range.

    Instances
      source
      theorem AlgebraicGeometry.isDominant_iff {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
      AlgebraicGeometry.IsDominant f ↔ DenseRange ⇑f.base
      source
      theorem AlgebraicGeometry.dominant_eq_topologically :
      @AlgebraicGeometry.IsDominant = AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => DenseRange
      source
      theorem AlgebraicGeometry.Scheme.Hom.denseRange {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.IsDominant f] :
      DenseRange ⇑f.base
      source
      @[instance 100]
      instance AlgebraicGeometry.instIsDominantOfSurjective {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f] :
      AlgebraicGeometry.IsDominant f
      Equations
      • ⋯ = ⋯
      source
      instance AlgebraicGeometry.instIsDominantCompScheme {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsDominant f] [AlgebraicGeometry.IsDominant g] :
      AlgebraicGeometry.IsDominant (CategoryTheory.CategoryStruct.comp f g)
      Equations
      • ⋯ = ⋯
      source
      instance AlgebraicGeometry.instIsMultiplicativeSchemeIsDominant :
      CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsDominant
      Equations
      source
      theorem AlgebraicGeometry.IsDominant.of_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsDominant (CategoryTheory.CategoryStruct.comp f g)] :
      AlgebraicGeometry.IsDominant g
      source
      theorem AlgebraicGeometry.IsDominant.comp_iff {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsDominant f] :
      AlgebraicGeometry.IsDominant (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.IsDominant g
      source
      instance AlgebraicGeometry.IsDominant.respectsIso :
      CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.IsDominant
      Equations
      source
      instance AlgebraicGeometry.IsDominant.isLocalAtTarget :
      AlgebraicGeometry.IsLocalAtTarget @AlgebraicGeometry.IsDominant
      Equations
      source
      theorem AlgebraicGeometry.surjective_of_isDominant_of_isClosed_range {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsDominant f] (hf : IsClosed (Set.range ⇑f.base)) :
      AlgebraicGeometry.Surjective f
      source
      theorem AlgebraicGeometry.IsDominant.of_comp_of_isOpenImmersion {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsDominant (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.IsOpenImmersion g] :
      AlgebraicGeometry.IsDominant f
      source
      instance AlgebraicGeometry.specializingMap_respectsIso :
      (AlgebraicGeometry.topologically @SpecializingMap).RespectsIso
      Equations
      source
      instance AlgebraicGeometry.specializingMap_isLocalAtTarget :
      AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically @SpecializingMap)
      Equations