Composition of rational maps

This file defines composition for partial maps and rational maps between schemes.

Main definitions

• Scheme.PartialMap.comp: given a dominant partial map f : X.PartialMap Y and any partial map g : Y.PartialMap Z, their composition f.comp g : X.PartialMap Z is defined on the preimage of g's domain under f.
• Scheme.RationalMap.comp: composition of rational maps, defined via a dominant representative.

Main statements

• Scheme.PartialMap.comp_equiv_of_equiv: Composition respects equivalence of partial maps.
• Scheme.PartialMap.comp_assoc: Composition of partial maps is associative.
• Scheme.RationalMap.comp_assoc: Composition of rational maps is associative.

noncomputable def AlgebraicGeometry.Scheme.PartialMap.comp {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.PartialMap Y) [IsDominant f.hom] (g : Y.PartialMap Z) : X.PartialMap Z

Composition of partial maps. The domain of f.comp g is the preimage of g.domain under f, viewed as an open subscheme of X. Requires f.hom to be dominant so that the domain is dense.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.PartialMap.comp_domain {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.PartialMap Y) [IsDominant f.hom] (g : Y.PartialMap Z) : (f.comp g).domain = (Hom.opensFunctor f.domain.ι).obj ((TopologicalSpace.Opens.map f.hom.base).obj g.domain)

@[simp]

theorem AlgebraicGeometry.Scheme.PartialMap.comp_hom {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.PartialMap Y) [IsDominant f.hom] (g : Y.PartialMap Z) : (f.comp g).hom = CategoryTheory.CategoryStruct.comp (Hom.isoImage f.domain.ι ((TopologicalSpace.Opens.map f.hom.base).obj g.domain)).inv (CategoryTheory.CategoryStruct.comp (f.hom ∣_ g.domain) g.hom)

theorem AlgebraicGeometry.Scheme.PartialMap.comp_restrict_left {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.PartialMap Y) [IsDominant f.hom] (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) (g : Y.PartialMap Z) : (f.restrict U hU hU').comp g = (f.comp g).restrict ((Hom.opensFunctor f.domain.ι).obj ((TopologicalSpace.Opens.map f.hom.base).obj g.domain) ⊓ U) ⋯ ⋯

theorem AlgebraicGeometry.Scheme.PartialMap.comp_restrict_right {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.PartialMap Y) [IsDominant f.hom] (g : Y.PartialMap Z) (V : Y.Opens) (hV : Dense ↑V) (hV' : V ≤ g.domain) : f.comp (g.restrict V hV hV') = (f.comp g).restrict ((Hom.opensFunctor f.domain.ι).obj ((TopologicalSpace.Opens.map f.hom.base).obj V)) ⋯ ⋯

theorem AlgebraicGeometry.Scheme.PartialMap.comp_equiv_of_equiv_left {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] {f₁ f₂ : X.PartialMap Y} [IsDominant f₁.hom] [IsDominant f₂.hom] (h : f₁.equiv f₂) (g : Y.PartialMap Z) : (f₁.comp g).equiv (f₂.comp g)

Composition respects equivalence of partial maps on the left.

theorem AlgebraicGeometry.Scheme.PartialMap.comp_equiv_of_equiv_right {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.PartialMap Y) [IsDominant f.hom] {g₁ g₂ : Y.PartialMap Z} (h : g₁.equiv g₂) : (f.comp g₁).equiv (f.comp g₂)

Composition respects equivalence of partial maps on the right.

theorem AlgebraicGeometry.Scheme.PartialMap.comp_equiv_of_equiv {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f₁ f₂ : X.PartialMap Y) [IsDominant f₁.hom] [IsDominant f₂.hom] (hf : f₁.equiv f₂) (g₁ g₂ : Y.PartialMap Z) (hg : g₁.equiv g₂) : (f₁.comp g₁).equiv (f₂.comp g₂)

Composition respects equivalence of partial maps in both arguments.

instance AlgebraicGeometry.Scheme.PartialMap.isDominant_comp_hom {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.PartialMap Y) [IsDominant f.hom] (g : Y.PartialMap Z) [IsDominant g.hom] : IsDominant (f.comp g).hom

@[simp]

theorem AlgebraicGeometry.Scheme.PartialMap.comp_assoc {X₁ X₂ X₃ Y : Scheme} [PreirreducibleSpace ↥X₁] [IrreducibleSpace ↥X₂] [Nonempty ↥X₃] (f : X₁.PartialMap X₂) [IsDominant f.hom] (g : X₂.PartialMap X₃) [IsDominant g.hom] (h : X₃.PartialMap Y) : (f.comp g).comp h = f.comp (g.comp h)

@[simp]

theorem AlgebraicGeometry.Scheme.PartialMap.comp_toPartialMap {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.PartialMap Y) [IsDominant f.hom] (g : Y ⟶ Z) : f.comp (Hom.toPartialMap g) = f.compHom g

theorem AlgebraicGeometry.Scheme.PartialMap.comp_id {X Y : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.PartialMap Y) [IsDominant f.hom] : f.comp (PartialMap.id Y) = f

noncomputable def AlgebraicGeometry.Scheme.RationalMap.comp {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.RationalMap Y) [f.IsDominant] (g : Y.RationalMap Z) : X.RationalMap Z

Composition of rational maps. Requires f to be dominant, so that we may choose a dominant representative.

Equations

• f.comp g = Quotient.liftOn g (AlgebraicGeometry.Scheme.PartialMap.toRationalMap ∘ f.representative.comp) ⋯

theorem AlgebraicGeometry.Scheme.RationalMap.comp_def {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.RationalMap Y) [f.IsDominant] (g : Y.PartialMap Z) : f.comp g.toRationalMap = (f.representative.comp g).toRationalMap

theorem AlgebraicGeometry.Scheme.RationalMap.toRationalMap_comp {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.PartialMap Y) [IsDominant f.hom] (g : Y.PartialMap Z) : f.toRationalMap.comp g.toRationalMap = (f.comp g).toRationalMap

@[simp]

theorem AlgebraicGeometry.Scheme.RationalMap.comp_id {X Y : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.RationalMap Y) [f.IsDominant] : f.comp (id Y) = f

instance AlgebraicGeometry.Scheme.RationalMap.instIsDominantComp {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.RationalMap Y) [f.IsDominant] (g : Y.RationalMap Z) [g.IsDominant] : (f.comp g).IsDominant

theorem AlgebraicGeometry.Scheme.RationalMap.comp_toRationalMap {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] (f : X.RationalMap Y) [f.IsDominant] (h : Y ⟶ Z) : f.comp (Hom.toRationalMap h) = f.compHom h

theorem AlgebraicGeometry.Scheme.RationalMap.comp_assoc {X₁ X₂ X₃ Y : Scheme} [PreirreducibleSpace ↥X₁] [IrreducibleSpace ↥X₂] [Nonempty ↥X₃] (f₁ : X₁.RationalMap X₂) [f₁.IsDominant] (f₂ : X₂.RationalMap X₃) [f₂.IsDominant] (f₃ : X₃.RationalMap Y) : (f₁.comp f₂).comp f₃ = f₁.comp (f₂.comp f₃)

instance AlgebraicGeometry.Scheme.RationalMap.isOver_comp {X Y Z : Scheme} [PreirreducibleSpace ↥X] [Nonempty ↥Y] {S : Scheme} [IrreducibleSpace ↥Y] [Nonempty ↥Z] [X.Over S] [Y.Over S] [Z.Over S] (f : X.RationalMap Y) [f.IsDominant] [IsOver S f] (g : Y.RationalMap Z) [g.IsDominant] [IsOver S g] : IsOver S (f.comp g)

@[simp]

theorem AlgebraicGeometry.Scheme.PartialMap.id_comp {X Y : Scheme} [IrreducibleSpace ↥X] (f : X.PartialMap Y) : (PartialMap.id X).comp f = f

@[simp]

theorem AlgebraicGeometry.Scheme.RationalMap.id_comp {X Y : Scheme} [IrreducibleSpace ↥X] (f : X.RationalMap Y) : (id X).comp f = f