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
GeneralizingMap
IsEmbedding
IsOpenEmbedding
IsClosedEmbedding
DenseRange (IsDominant)

instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyInjective :

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

instance AlgebraicGeometry.injective_isZariskiLocalAtTarget :

IsZariskiLocalAtTarget (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 ⟶ 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.instIsStableUnderCompositionSchemeSurjective :

CategoryTheory.MorphismProperty.IsStableUnderComposition @Surjective

instance AlgebraicGeometry.instRespectsIsoSchemeSurjective :

CategoryTheory.MorphismProperty.RespectsIso @Surjective

instance AlgebraicGeometry.instHasOfPrecompPropertySchemeSurjective (P : CategoryTheory.MorphismProperty Scheme) :

CategoryTheory.MorphismProperty.HasOfPrecompProperty (@Surjective) P

instance AlgebraicGeometry.surjective_isZariskiLocalAtTarget :

IsZariskiLocalAtTarget @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.instSurjectiveDescI₀SchemeF {X : Scheme} {P : CategoryTheory.MorphismProperty Scheme} (𝒰 : Scheme.Cover (Scheme.precoverage P) X) :

Surjective (CategoryTheory.Limits.Sigma.desc fun (i : 𝒰.I₀) => 𝒰.f i)

def AlgebraicGeometry.Scheme.Hom.cover {P : CategoryTheory.MorphismProperty Scheme} {X S : Scheme} (f : X ⟶ S) (hf : P f) [Surjective f] :

Cover (precoverage P) S

The single object covering by one surjective morphism satisfying P.

Equations

AlgebraicGeometry.Scheme.Hom.cover f hf = CategoryTheory.Precoverage.ZeroHypercover.singleton f ⋯

Instances For

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.cover_I₀ {P : CategoryTheory.MorphismProperty Scheme} {X S : Scheme} (f : X ⟶ S) (hf : P f) [Surjective f] :

(cover f hf).I₀ = PUnit.{v + 1}

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.cover_X {P : CategoryTheory.MorphismProperty Scheme} {X S : Scheme} (f : X ⟶ S) (hf : P f) [Surjective f] (x✝ : PUnit.{v + 1}) :

(cover f hf).X x✝ = X

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.cover_f {P : CategoryTheory.MorphismProperty Scheme} {X S : Scheme} (f : X ⟶ S) (hf : P f) [Surjective f] (x✝ : PUnit.{v + 1}) :

(cover f hf).f x✝ = f

instance AlgebraicGeometry.instUniqueI₀SchemeCover {P : CategoryTheory.MorphismProperty Scheme} {X S : Scheme} (f : X ⟶ S) (hf : P f) [Surjective f] :

Unique (Scheme.Hom.cover f hf).I₀

Equations

AlgebraicGeometry.instUniqueI₀SchemeCover f hf = inferInstanceAs (Unique PUnit.{?u.37 + 1})

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_isZariskiLocalAtTarget :

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

instance AlgebraicGeometry.instIsZariskiLocalAtSourceTopologicallyIsOpenMap :

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

instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedMap :

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

instance AlgebraicGeometry.isClosedMap_isZariskiLocalAtTarget :

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

instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsEmbedding :

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

instance AlgebraicGeometry.isEmbedding_isZariskiLocalAtTarget :

IsZariskiLocalAtTarget (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_isZariskiLocalAtTarget :

IsZariskiLocalAtTarget (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_isZariskiLocalAtTarget :

IsZariskiLocalAtTarget (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 ⟶ 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.isZariskiLocalAtTarget :

IsZariskiLocalAtTarget @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_isZariskiLocalAtTarget :

IsZariskiLocalAtTarget (topologically @SpecializingMap)

instance AlgebraicGeometry.instRespectsIsoSchemeTopologicallyGeneralizingMap :

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

instance AlgebraicGeometry.instIsZariskiLocalAtSourceTopologicallyGeneralizingMap :

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

instance AlgebraicGeometry.instIsZariskiLocalAtTargetTopologicallyGeneralizingMap :

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