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

Injective
Surjective
IsOpenMap
IsClosedMap
IsEmbedding
IsOpenEmbedding
IsClosedEmbedding
DenseRange (IsDominant)

instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyInjective :

(topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Function.Injective).RespectsIso

instance AlgebraicGeometry.injective_isLocalAtTarget :

IsLocalAtTarget (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Function.Injective)

class AlgebraicGeometry.Surjective {X Y : Scheme} (f : X ⟶ Y) :

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

surj : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f.base)

Instances

theorem AlgebraicGeometry.surjective_iff {X Y : Scheme} (f : X ⟶ Y) :

Surjective f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f.base)

theorem AlgebraicGeometry.surjective_eq_topologically :

@Surjective = topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective

theorem AlgebraicGeometry.Scheme.Hom.surjective {X Y : Scheme} (f : X.Hom Y) [Surjective f] :

Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f.base)

@[instance 100]

instance AlgebraicGeometry.instSurjectiveOfIsIsoScheme {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] :

instance AlgebraicGeometry.instSurjectiveCompScheme {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [Surjective f] [Surjective g] :

Surjective (CategoryTheory.CategoryStruct.comp f g)

theorem AlgebraicGeometry.Surjective.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [Surjective (CategoryTheory.CategoryStruct.comp f g)] :

theorem AlgebraicGeometry.Surjective.comp_iff {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [Surjective f] :

Surjective (CategoryTheory.CategoryStruct.comp f g) ↔ Surjective g

instance AlgebraicGeometry.instRespectsIsoSchemeSurjective :

CategoryTheory.MorphismProperty.RespectsIso @Surjective

instance AlgebraicGeometry.surjective_isLocalAtTarget :

IsLocalAtTarget @Surjective

@[simp]

theorem AlgebraicGeometry.range_eq_univ {X Y : Scheme} (f : X ⟶ Y) [Surjective f] :

Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) = Set.univ

theorem AlgebraicGeometry.range_eq_range_of_surjective {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) (e : X ⟶ Y) [Surjective e] (hge : CategoryTheory.CategoryStruct.comp e g = f) :

Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)

theorem AlgebraicGeometry.mem_range_iff_of_surjective {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) (e : X ⟶ Y) [Surjective e] (hge : CategoryTheory.CategoryStruct.comp e g = f) (s : ↑↑S.toPresheafedSpace) :

s ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) ↔ s ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)

instance AlgebraicGeometry.injective_isStableUnderComposition :

(topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) => Function.Injective x).IsStableUnderComposition

instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenMap :

(topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsOpenMap).RespectsIso

instance AlgebraicGeometry.isOpenMap_isLocalAtTarget :

IsLocalAtTarget (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsOpenMap)

instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedMap :

(topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsClosedMap).RespectsIso

instance AlgebraicGeometry.isClosedMap_isLocalAtTarget :

IsLocalAtTarget (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => IsClosedMap)

instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsEmbedding :

(topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsEmbedding).RespectsIso

instance AlgebraicGeometry.isEmbedding_isLocalAtTarget :

IsLocalAtTarget (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsEmbedding)

instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenEmbedding :

(topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding).RespectsIso

instance AlgebraicGeometry.isOpenEmbedding_isLocalAtTarget :

IsLocalAtTarget (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding)

instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedEmbedding :

(topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsClosedEmbedding).RespectsIso

instance AlgebraicGeometry.isClosedEmbedding_isLocalAtTarget :

IsLocalAtTarget (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsClosedEmbedding)

class AlgebraicGeometry.IsDominant {X Y : Scheme} (f : X ⟶ Y) :

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

denseRange : DenseRange ⇑(CategoryTheory.ConcreteCategory.hom f.base)

Instances

theorem AlgebraicGeometry.isDominant_iff {X Y : Scheme} (f : X ⟶ Y) :

IsDominant f ↔ DenseRange ⇑(CategoryTheory.ConcreteCategory.hom f.base)

theorem AlgebraicGeometry.dominant_eq_topologically :

@IsDominant = topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => DenseRange

theorem AlgebraicGeometry.Scheme.Hom.denseRange {X Y : Scheme} (f : X.Hom Y) [IsDominant f] :

DenseRange ⇑(CategoryTheory.ConcreteCategory.hom f.base)

@[instance 100]

instance AlgebraicGeometry.instIsDominantOfSurjective {X Y : Scheme} (f : X ⟶ Y) [Surjective f] :

instance AlgebraicGeometry.instIsDominantCompScheme {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsDominant f] [IsDominant g] :

IsDominant (CategoryTheory.CategoryStruct.comp f g)

instance AlgebraicGeometry.instIsMultiplicativeSchemeIsDominant :

CategoryTheory.MorphismProperty.IsMultiplicative @IsDominant

theorem AlgebraicGeometry.IsDominant.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [H : IsDominant (CategoryTheory.CategoryStruct.comp f g)] :

theorem AlgebraicGeometry.IsDominant.comp_iff {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsDominant f] :

IsDominant (CategoryTheory.CategoryStruct.comp f g) ↔ IsDominant g

instance AlgebraicGeometry.IsDominant.respectsIso :

CategoryTheory.MorphismProperty.RespectsIso @IsDominant

instance AlgebraicGeometry.IsDominant.isLocalAtTarget :

IsLocalAtTarget @IsDominant

theorem AlgebraicGeometry.surjective_of_isDominant_of_isClosed_range {X Y : Scheme} (f : X ⟶ Y) [IsDominant f] (hf : IsClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base))) :

theorem AlgebraicGeometry.IsDominant.of_comp_of_isOpenImmersion {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [H : IsDominant (CategoryTheory.CategoryStruct.comp f g)] [IsOpenImmersion g] :

instance AlgebraicGeometry.specializingMap_respectsIso :

(topologically @SpecializingMap).RespectsIso

instance AlgebraicGeometry.specializingMap_isLocalAtTarget :

IsLocalAtTarget (topologically @SpecializingMap)