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
• GeneralizingMap
• 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) : Prop

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

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

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] : Surjective 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)] : Surjective 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) : s ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) ↔ s ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)

theorem AlgebraicGeometry.Surjective.sigmaDesc_of_union_range_eq_univ {X : Scheme} {ι : Type v} [Small.{u, v} ι] {Y : ι → Scheme} {f : (i : ι) → Y i ⟶ X} (H : ⋃ (i : ι), Set.range ⇑(CategoryTheory.ConcreteCategory.hom (f i).base) = Set.univ) : Surjective (CategoryTheory.Limits.Sigma.desc f)

instance AlgebraicGeometry.instSurjectiveDescJSchemeMap {X : Scheme} {P : CategoryTheory.MorphismProperty Scheme} (𝒰 : Scheme.Cover P X) : Surjective (CategoryTheory.Limits.Sigma.desc fun (i : 𝒰.J) => 𝒰.map i)

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.instIsLocalAtSourceTopologicallyIsOpenMap : IsLocalAtSource (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) : Prop

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

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

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] : IsDominant 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)] : IsDominant 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))) : Surjective f

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] : IsDominant f

instance AlgebraicGeometry.specializingMap_respectsIso : (topologically @SpecializingMap).RespectsIso

instance AlgebraicGeometry.specializingMap_isLocalAtTarget : IsLocalAtTarget (topologically @SpecializingMap)

instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyGeneralizingMap : (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => GeneralizingMap).RespectsIso

instance AlgebraicGeometry.instIsLocalAtSourceTopologicallyGeneralizingMap : IsLocalAtSource (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => GeneralizingMap)

instance AlgebraicGeometry.instIsLocalAtTargetTopologicallyGeneralizingMap : IsLocalAtTarget (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] => GeneralizingMap)