Instances for the inputs of the algebraic main theorems

Instances on AlgebraicGeometry.AlgScheme, AlgebraicGeometry.Triple and AlgebraicGeometry.EmbeddedPair that the proofs of the theorems use and their statements do not: an algebraic k-scheme is separated, a morphism of algebraic k-schemes is a k-morphism, and the ambient scheme of a triple or of an embedded pair is smooth. AlgScheme.of X is the algebraic k-scheme of a scheme X separated and of finite type over k, and AlgScheme.ofHom f that of a structure morphism f; both unfold to their underlying scheme under reducible transparency.

instance AlgebraicGeometry.AlgScheme.isSeparated {k : Type u} [Field k] (X : AlgScheme k) : IsSeparated (X.left ↘ Spec ↧k)

instance AlgebraicGeometry.AlgScheme.isOver_left {k : Type u} [Field k] {X Y : AlgScheme k} (h : Y ⟶ X) : Scheme.Hom.IsOver h.left (Spec ↧k)

A morphism of algebraic k-schemes is a k-morphism.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AlgScheme.ofHom {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (hf : FiniteType f) (hs : IsSeparated f) : AlgScheme k

The algebraic k-scheme with underlying scheme X and structure morphism f, of finite type and separated. It is written as a structure, so that (ofHom f).left unfolds to X and (ofHom f).left ↘ Spec k to f under reducible transparency: instance search and simp see through it.

Equations

• AlgebraicGeometry.AlgScheme.ofHom f hf hs = { left := X, right := { as := PUnit.unit }, hom := f, prop := ⋯ }

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AlgScheme.of {k : Type u} [Field k] (X : Scheme) [X.Over (Spec ↧k)] [FiniteType (X ↘ Spec ↧k)] [IsSeparated (X ↘ Spec ↧k)] : AlgScheme k

The algebraic k-scheme of a scheme X over Spec k whose structure morphism is of finite type and separated; its underlying scheme is X (of_left), and instance search sees every instance on X at (of X).left.

Equations

• AlgebraicGeometry.AlgScheme.of X = AlgebraicGeometry.AlgScheme.ofHom (X ↘ AlgebraicGeometry.Spec ↧k) ⋯ ⋯

@[simp]

theorem AlgebraicGeometry.AlgScheme.of_left {k : Type u} [Field k] (X : Scheme) [X.Over (Spec ↧k)] [FiniteType (X ↘ Spec ↧k)] [IsSeparated (X ↘ Spec ↧k)] : (of X).left = X

instance AlgebraicGeometry.Triple.smooth {k : Type u} [Field k] (T : Triple k) : Smooth (T.X.left ↘ Spec ↧k)

instance AlgebraicGeometry.EmbeddedPair.smooth {k : Type u} [Field k] (P : EmbeddedPair k) : Smooth (P.X.left ↘ Spec ↧k)