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 : 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_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
    AlgebraicGeometry.Surjective f ↔ Function.Surjective ⇑f.base
    source
    theorem AlgebraicGeometry.Surjective.surj {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : 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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.Surjective f] :
    Function.Surjective ⇑f.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.instRespectsIsoSchemeTopologicallyIsEmbedding :
    (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsEmbedding).RespectsIso
    Equations
    source
    instance AlgebraicGeometry.isEmbedding_isLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsEmbedding)
    Equations
    source
    instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenEmbedding :
    (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsOpenEmbedding).RespectsIso
    Equations
    source
    instance AlgebraicGeometry.isOpenEmbedding_isLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsOpenEmbedding)
    Equations
    source
    instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedEmbedding :
    (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsClosedEmbedding).RespectsIso
    Equations
    source
    instance AlgebraicGeometry.isClosedEmbedding_isLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsClosedEmbedding)
    Equations
    source
    class AlgebraicGeometry.IsDominant {X : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
      AlgebraicGeometry.IsDominant f ↔ DenseRange ⇑f.base
      source
      theorem AlgebraicGeometry.IsDominant.denseRange {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : 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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.IsDominant f] :
      DenseRange ⇑f.base
      source
      @[instance 100]
      instance AlgebraicGeometry.instIsDominantOfSurjective {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Surjective f] :
      AlgebraicGeometry.IsDominant f
      Equations
      • ⋯ = ⋯
      source
      instance AlgebraicGeometry.instIsDominantCompScheme {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsDominant (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.IsOpenImmersion g] :
      AlgebraicGeometry.IsDominant f