Affine space

Main definitions

• AlgebraicGeometry.AffineSpace: 𝔸(n; S) is the affine n-space over S.
• AlgebraicGeometry.AffineSpace.coord: The standard coordinate functions on the affine space.
• AlgebraicGeometry.AffineSpace.homOfVector: The morphism X ⟶ 𝔸(n; S) given by a X ⟶ S and a choice of n-coordinate functions.
• AlgebraicGeometry.AffineSpace.homOverEquiv: S-morphisms into Spec 𝔸(n; S) are equivalent to the choice of n global sections.
• AlgebraicGeometry.AffineSpace.SpecIso: 𝔸(n; Spec R) ≅ Spec R[n]

noncomputable def AlgebraicGeometry.AffineSpace (n : Type u) (S : Scheme) : Scheme

𝔸(n; S) is the affine n-space over S. Note that n : Type u is an arbitrary index type (e.g. ULift.{u} (Fin m)).

Equations

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

def AlgebraicGeometry.«term𝔸(_;_)» : Lean.ParserDescr

𝔸(n; S) is the affine n-space over S.

Equations

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

theorem AlgebraicGeometry.AffineSpace.of_mvPolynomial_int_ext {n : Type u} {R : CommRingCat} {f g : ↧(MvPolynomial n (ULift.{u_1, 0} ℤ)) ⟶ R} (h : ∀ (i : n), (CategoryTheory.ConcreteCategory.hom f) (MvPolynomial.X i) = (CategoryTheory.ConcreteCategory.hom g) (MvPolynomial.X i)) : f = g

@[instance_reducible]

noncomputable instance AlgebraicGeometry.AffineSpace.over (n : Type u) (S : Scheme) : (AffineSpace n S).CanonicallyOver S

Equations

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

theorem AlgebraicGeometry.AffineSpace.over_over (n : Type u) (S : Scheme) : AffineSpace n S ↘ S = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.terminal.from S) (CategoryTheory.Limits.terminal.from (Spec ↧(MvPolynomial n (ULift.{u, 0} ℤ))))

noncomputable def AlgebraicGeometry.AffineSpace.toSpecMvPoly (n : Type u) (S : Scheme) : AffineSpace n S ⟶ Spec ↧(MvPolynomial n (ULift.{u, 0} ℤ))

The map from the affine n-space over S to the integral model Spec ℤ[n].

Equations

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

noncomputable def AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv (n : Type u) {X : Scheme} : (X ⟶ Spec ↧(MvPolynomial n (ULift.{u, 0} ℤ))) ≃ (n → ↑(X.presheaf.obj (Opposite.op ⊤)))

Morphisms into Spec ℤ[n] are equivalent the choice of n global sections. Use homOverEquiv instead.

Equations

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

@[simp]

theorem AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply (n : Type u) {X : Scheme} (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) : (toSpecMvPolyIntEquiv n).symm v = CategoryTheory.CategoryStruct.comp X.toSpecΓ (Spec.map (CommRingCat.ofHom (MvPolynomial.eval₂Hom ((algebraMap ℤ ↑(X.presheaf.1 (Opposite.op ⊤))).comp ULift.ringEquiv.toRingHom) v)))

@[simp]

theorem AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply (n : Type u) {X : Scheme} (f : X ⟶ Spec ↧(MvPolynomial n (ULift.{u, 0} ℤ))) (i : n) : (toSpecMvPolyIntEquiv n) f i = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop f)) ((CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso ↧(MvPolynomial n (ULift.{u, 0} ℤ))).inv) (MvPolynomial.X i))

theorem AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp (n : Type u) {X Y : Scheme} (f : X ⟶ Y) (g : Y ⟶ Spec ↧(MvPolynomial n (ULift.{u, 0} ℤ))) (i : n) : (toSpecMvPolyIntEquiv n) (CategoryTheory.CategoryStruct.comp f g) i = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop f)) ((toSpecMvPolyIntEquiv n) g i)

noncomputable def AlgebraicGeometry.AffineSpace.coord {n : Type u} (S : Scheme) (i : n) : ↑((AffineSpace n S).presheaf.obj (Opposite.op ⊤))

The standard coordinates of 𝔸(n; S).

Equations

• AlgebraicGeometry.AffineSpace.coord S i = (AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n) (AlgebraicGeometry.AffineSpace.toSpecMvPoly n S) i

noncomputable def AlgebraicGeometry.AffineSpace.homOfVector {n : Type u} {S X : Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) : X ⟶ AffineSpace n S

The morphism X ⟶ 𝔸(n; S) given by a X ⟶ S and a choice of n-coordinate functions.

Equations

• AlgebraicGeometry.AffineSpace.homOfVector f v = CategoryTheory.Limits.pullback.lift f ((AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n).symm v) ⋯

@[simp]

theorem AlgebraicGeometry.AffineSpace.homOfVector_over {n : Type u} {S X : Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) : CategoryTheory.CategoryStruct.comp (homOfVector f v) (AffineSpace n S ↘ S) = f

@[simp]

theorem AlgebraicGeometry.AffineSpace.homOfVector_over_assoc {n : Type u} {S X : Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) {Z : Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (homOfVector f v) (CategoryTheory.CategoryStruct.comp (AffineSpace n S ↘ S) h) = CategoryTheory.CategoryStruct.comp f h

theorem AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly {n : Type u} {S X : Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) : CategoryTheory.CategoryStruct.comp (homOfVector f v) (toSpecMvPoly n S) = (toSpecMvPolyIntEquiv n).symm v

theorem AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly_assoc {n : Type u} {S X : Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) {Z : Scheme} (h : Spec ↧(MvPolynomial n (ULift.{u, 0} ℤ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (homOfVector f v) (CategoryTheory.CategoryStruct.comp (toSpecMvPoly n S) h) = CategoryTheory.CategoryStruct.comp ((toSpecMvPolyIntEquiv n).symm v) h

@[simp]

theorem AlgebraicGeometry.AffineSpace.homOfVector_appTop_coord {n : Type u} {S X : Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) (i : n) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (homOfVector f v))) (coord S i) = v i

theorem AlgebraicGeometry.AffineSpace.hom_ext {n : Type u} {S X : Scheme} {f g : X ⟶ AffineSpace n S} (h₁ : CategoryTheory.CategoryStruct.comp f (AffineSpace n S ↘ S) = CategoryTheory.CategoryStruct.comp g (AffineSpace n S ↘ S)) (h₂ : ∀ (i : n), (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)) : f = g

theorem AlgebraicGeometry.AffineSpace.hom_ext_iff {n : Type u} {S X : Scheme} {f g : X ⟶ AffineSpace n S} : f = g ↔ CategoryTheory.CategoryStruct.comp f (AffineSpace n S ↘ S) = CategoryTheory.CategoryStruct.comp g (AffineSpace n S ↘ S) ∧ ∀ (i : n), (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop f)) (coord S i) = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop g)) (coord S i)

theorem AlgebraicGeometry.AffineSpace.comp_homOfVector {n : Type u} {S X Y : Scheme} (v : n → ↑(Y.presheaf.obj (Opposite.op ⊤))) (f : X ⟶ Y) (g : Y ⟶ S) : CategoryTheory.CategoryStruct.comp f (homOfVector g v) = homOfVector (CategoryTheory.CategoryStruct.comp f g) (⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop f)) ∘ v)

theorem AlgebraicGeometry.AffineSpace.comp_homOfVector_assoc {n : Type u} {S X Y : Scheme} (v : n → ↑(Y.presheaf.obj (Opposite.op ⊤))) (f : X ⟶ Y) (g : Y ⟶ S) {Z : Scheme} (h : AffineSpace n S ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (homOfVector g v) h) = CategoryTheory.CategoryStruct.comp (homOfVector (CategoryTheory.CategoryStruct.comp f g) (⇑(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop f)) ∘ v)) h

instance AlgebraicGeometry.AffineSpace.instIsOverHomOfVectorOverSchemeInferInstanceOverClass {n : Type u} (S : Scheme) {X : Scheme} [X.Over S] (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) : Scheme.Hom.IsOver (homOfVector (X ↘ S) v) S

noncomputable def AlgebraicGeometry.AffineSpace.homOverEquiv {n : Type u} (S : Scheme) {X : Scheme} [X.Over S] : { f : X ⟶ AffineSpace n S // Scheme.Hom.IsOver f S } ≃ (n → ↑(X.presheaf.obj (Opposite.op ⊤)))

S-morphisms into Spec 𝔸(n; S) are equivalent to the choice of n global sections.

Equations

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

@[simp]

theorem AlgebraicGeometry.AffineSpace.homOverEquiv_symm_apply_coe {n : Type u} (S : Scheme) {X : Scheme} [X.Over S] (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) : ↑((homOverEquiv S).symm v) = homOfVector (X ↘ S) v

@[simp]

theorem AlgebraicGeometry.AffineSpace.homOverEquiv_apply {n : Type u} (S : Scheme) {X : Scheme} [X.Over S] (f : { f : X ⟶ AffineSpace n S // Scheme.Hom.IsOver f S }) (i : n) : (homOverEquiv S) f i = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop ↑f)) (coord S i)

noncomputable def AlgebraicGeometry.AffineSpace.isoOfIsAffine (n : Type u) (S : Scheme) [IsAffine S] : AffineSpace n S ≅ Spec ↧(MvPolynomial n ↑(S.presheaf.obj (Opposite.op ⊤)))

The affine space over an affine base is isomorphic to the spectrum of the polynomial ring. Also see AffineSpace.SpecIso.

Equations

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

theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv (n : Type u) (S : Scheme) [IsAffine S] : (isoOfIsAffine n S).inv = homOfVector (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom MvPolynomial.C)) S.isoSpec.inv) (⇑(CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso ↧(MvPolynomial n ↑(S.presheaf.obj (Opposite.op ⊤)))).inv) ∘ MvPolynomial.X)

theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom (n : Type u) (S : Scheme) [IsAffine S] : (isoOfIsAffine n S).hom = CategoryTheory.CategoryStruct.comp (AffineSpace n S).toSpecΓ (Spec.map (CommRingCat.ofHom (MvPolynomial.eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace n S ↘ S))) (coord S))))

@[simp]

theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop {n : Type u} (S : Scheme) [IsAffine S] : Scheme.Hom.appTop (isoOfIsAffine n S).hom = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso ↧(MvPolynomial n ↑(S.presheaf.obj (Opposite.op ⊤)))).hom (CommRingCat.ofHom (MvPolynomial.eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (AffineSpace n S ↘ S))) (coord S)))

@[simp]

theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord {n : Type u} (S : Scheme) [IsAffine S] (i : n) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (isoOfIsAffine n S).inv)) (coord S i) = (CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso ↧(MvPolynomial n ↑(S.presheaf.obj (Opposite.op ⊤)))).inv) (MvPolynomial.X i)

@[simp]

theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over {n : Type u} (S : Scheme) [IsAffine S] : CategoryTheory.CategoryStruct.comp (isoOfIsAffine n S).inv (AffineSpace n S ↘ S) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom MvPolynomial.C)) S.isoSpec.inv

@[simp]

theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc {n : Type u} (S : Scheme) [IsAffine S] {Z : Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (isoOfIsAffine n S).inv (CategoryTheory.CategoryStruct.comp (AffineSpace n S ↘ S) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom MvPolynomial.C)) (CategoryTheory.CategoryStruct.comp S.isoSpec.inv h)

instance AlgebraicGeometry.AffineSpace.instIsAffine {n : Type u} (S : Scheme) [IsAffine S] : IsAffine (AffineSpace n S)

noncomputable def AlgebraicGeometry.AffineSpace.SpecIso (n : Type u) (R : CommRingCat) : AffineSpace n (Spec R) ≅ Spec ↧(MvPolynomial n ↑R)

The affine space over an affine base is isomorphic to the spectrum of the polynomial ring.

Equations

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

@[simp]

theorem AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop {n : Type u} (R : CommRingCat) : Scheme.Hom.appTop (SpecIso n R).hom = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso ↧(MvPolynomial n ↑R)).hom (CommRingCat.ofHom (MvPolynomial.eval₂Hom (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso R).inv (Scheme.Hom.appTop (AffineSpace n (Spec R) ↘ Spec R)))) (coord (Spec R))))

@[simp]

theorem AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord {n : Type u} (R : CommRingCat) (i : n) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (SpecIso n R).inv)) (coord (Spec R) i) = (CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso ↧(MvPolynomial n ↑R)).inv) (MvPolynomial.X i)

@[simp]

theorem AlgebraicGeometry.AffineSpace.SpecIso_inv_over {n : Type u} (R : CommRingCat) : CategoryTheory.CategoryStruct.comp (SpecIso n R).inv (AffineSpace n (Spec R) ↘ Spec R) = Spec.map (CommRingCat.ofHom MvPolynomial.C)

@[simp]

theorem AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc {n : Type u} (R : CommRingCat) {Z : Scheme} (h : Spec R ⟶ Z) : CategoryTheory.CategoryStruct.comp (SpecIso n R).inv (CategoryTheory.CategoryStruct.comp (AffineSpace n (Spec R) ↘ Spec R) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom MvPolynomial.C)) h

noncomputable def AlgebraicGeometry.AffineSpace.map (n : Type u) {S T : Scheme} (f : S ⟶ T) : AffineSpace n S ⟶ AffineSpace n T

𝔸(n; S) is functorial w.r.t. S.

Equations

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

@[simp]

theorem AlgebraicGeometry.AffineSpace.map_over {n : Type u} {S T : Scheme} (f : S ⟶ T) : CategoryTheory.CategoryStruct.comp (map n f) (AffineSpace n T ↘ T) = CategoryTheory.CategoryStruct.comp (AffineSpace n S ↘ S) f

@[simp]

theorem AlgebraicGeometry.AffineSpace.map_over_assoc {n : Type u} {S T : Scheme} (f : S ⟶ T) {Z : Scheme} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (map n f) (CategoryTheory.CategoryStruct.comp (AffineSpace n T ↘ T) h) = CategoryTheory.CategoryStruct.comp (AffineSpace n S ↘ S) (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem AlgebraicGeometry.AffineSpace.map_appTop_coord {n : Type u} {S T : Scheme} (f : S ⟶ T) (i : n) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (map n f))) (coord T i) = coord S i

@[simp]

theorem AlgebraicGeometry.AffineSpace.map_toSpecMvPoly {n : Type u} {S T : Scheme} (f : S ⟶ T) : CategoryTheory.CategoryStruct.comp (map n f) (toSpecMvPoly n T) = toSpecMvPoly n S

@[simp]

theorem AlgebraicGeometry.AffineSpace.map_toSpecMvPoly_assoc {n : Type u} {S T : Scheme} (f : S ⟶ T) {Z : Scheme} (h : Spec ↧(MvPolynomial n (ULift.{u, 0} ℤ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (map n f) (CategoryTheory.CategoryStruct.comp (toSpecMvPoly n T) h) = CategoryTheory.CategoryStruct.comp (toSpecMvPoly n S) h

@[simp]

theorem AlgebraicGeometry.AffineSpace.map_id {n : Type u} (S : Scheme) : map n (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id (AffineSpace n S)

@[simp]

theorem AlgebraicGeometry.AffineSpace.map_comp {n : Type u} {S S' S'' : Scheme} (f : S ⟶ S') (g : S' ⟶ S'') : map n (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map n f) (map n g)

theorem AlgebraicGeometry.AffineSpace.map_comp_assoc {n : Type u} {S S' S'' : Scheme} (f : S ⟶ S') (g : S' ⟶ S'') {Z : Scheme} (h : AffineSpace n S'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (map n (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (map n f) (CategoryTheory.CategoryStruct.comp (map n g) h)

theorem AlgebraicGeometry.AffineSpace.map_SpecMap {n : Type u} {R S : CommRingCat} (φ : R ⟶ S) : map n (Spec.map φ) = CategoryTheory.CategoryStruct.comp (SpecIso n S).hom (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ)))) (SpecIso n R).inv)

noncomputable def AlgebraicGeometry.AffineSpace.mapSpecMap {n : Type u} {R S : CommRingCat} (φ : R ⟶ S) : CategoryTheory.Arrow.mk (map n (Spec.map φ)) ≅ CategoryTheory.Arrow.mk (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))))

The map between affine spaces over affine bases is isomorphic to the natural map between polynomial rings.

Equations

• AlgebraicGeometry.AffineSpace.mapSpecMap φ = CategoryTheory.Arrow.isoMk (AlgebraicGeometry.AffineSpace.SpecIso n S) (AlgebraicGeometry.AffineSpace.SpecIso n R) ⋯

theorem AlgebraicGeometry.AffineSpace.isPullback_map {n : Type u} {S T : Scheme} (f : S ⟶ T) : CategoryTheory.IsPullback (map n f) (AffineSpace n S ↘ S) (AffineSpace n T ↘ T) f

noncomputable def AlgebraicGeometry.AffineSpace.reindex {n m : Type u} (i : m → n) (S : Scheme) : AffineSpace n S ⟶ AffineSpace m S

𝔸(n; S) is functorial w.r.t. n.

Equations

• AlgebraicGeometry.AffineSpace.reindex i S = AlgebraicGeometry.AffineSpace.homOfVector (AlgebraicGeometry.AffineSpace n S ↘ S) (AlgebraicGeometry.AffineSpace.coord S ∘ i)

@[simp]

theorem AlgebraicGeometry.AffineSpace.reindex_over {n m : Type u} (i : m → n) (S : Scheme) : CategoryTheory.CategoryStruct.comp (reindex i S) (AffineSpace m S ↘ S) = AffineSpace n S ↘ S

theorem AlgebraicGeometry.AffineSpace.reindex_over_assoc {n m : Type u} (i : m → n) (S : Scheme) {Z : Scheme} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (reindex i S) (CategoryTheory.CategoryStruct.comp (AffineSpace m S ↘ S) h) = CategoryTheory.CategoryStruct.comp (AffineSpace n S ↘ S) h

@[simp]

theorem AlgebraicGeometry.AffineSpace.reindex_appTop_coord {n m : Type u} (i : m → n) (S : Scheme) (j : m) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appTop (reindex i S))) (coord S j) = coord S (i j)

@[simp]

theorem AlgebraicGeometry.AffineSpace.reindex_id {n : Type u} (S : Scheme) : reindex id S = CategoryTheory.CategoryStruct.id (AffineSpace n S)

@[simp]

theorem AlgebraicGeometry.AffineSpace.reindex_comp {n₁ n₂ n₃ : Type u} (i : n₁ ⟶ n₂) (j : n₂ ⟶ n₃) (S : Scheme) : reindex (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp i j))) S = CategoryTheory.CategoryStruct.comp (reindex (⇑(CategoryTheory.ConcreteCategory.hom j)) S) (reindex (⇑(CategoryTheory.ConcreteCategory.hom i)) S)

theorem AlgebraicGeometry.AffineSpace.reindex_comp_assoc {n₁ n₂ n₃ : Type u} (i : n₁ ⟶ n₂) (j : n₂ ⟶ n₃) (S : Scheme) {Z : Scheme} (h : AffineSpace n₁ S ⟶ Z) : CategoryTheory.CategoryStruct.comp (reindex (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp i j))) S) h = CategoryTheory.CategoryStruct.comp (reindex (⇑(CategoryTheory.ConcreteCategory.hom j)) S) (CategoryTheory.CategoryStruct.comp (reindex (⇑(CategoryTheory.ConcreteCategory.hom i)) S) h)

@[simp]

theorem AlgebraicGeometry.AffineSpace.map_reindex {n₁ n₂ : Type u} (i : n₁ → n₂) {S T : Scheme} (f : S ⟶ T) : CategoryTheory.CategoryStruct.comp (map n₂ f) (reindex i T) = CategoryTheory.CategoryStruct.comp (reindex i S) (map n₁ f)

@[simp]

theorem AlgebraicGeometry.AffineSpace.map_reindex_assoc {n₁ n₂ : Type u} (i : n₁ → n₂) {S T : Scheme} (f : S ⟶ T) {Z : Scheme} (h : AffineSpace n₁ T ⟶ Z) : CategoryTheory.CategoryStruct.comp (map n₂ f) (CategoryTheory.CategoryStruct.comp (reindex i T) h) = CategoryTheory.CategoryStruct.comp (reindex i S) (CategoryTheory.CategoryStruct.comp (map n₁ f) h)

noncomputable def AlgebraicGeometry.AffineSpace.functor : CategoryTheory.Functor Type uᵒᵖ (CategoryTheory.Functor Scheme Scheme)

The affine space as a functor.

Equations

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

@[simp]

theorem AlgebraicGeometry.AffineSpace.functor_obj_map (n : Type uᵒᵖ) {X✝ Y✝ : Scheme} (f : X✝ ⟶ Y✝) : (functor.obj n).map f = map (Opposite.unop n) f

@[simp]

theorem AlgebraicGeometry.AffineSpace.functor_obj_obj (n : Type uᵒᵖ) (S : Scheme) : (functor.obj n).obj S = AffineSpace (Opposite.unop n) S

@[simp]

theorem AlgebraicGeometry.AffineSpace.functor_map_app {n m : Type uᵒᵖ} (i : n ⟶ m) (S : Scheme) : (functor.map i).app S = reindex (⇑(CategoryTheory.ConcreteCategory.hom i.unop)) S

instance AlgebraicGeometry.AffineSpace.instIsAffineHomOverSchemeInferInstanceOverClass {n : Type u} (S : Scheme) : IsAffineHom (AffineSpace n S ↘ S)

instance AlgebraicGeometry.AffineSpace.instSurjectiveOverSchemeInferInstanceOverClass {n : Type u} (S : Scheme) : Surjective (AffineSpace n S ↘ S)

instance AlgebraicGeometry.AffineSpace.instLocallyOfFinitePresentationOverSchemeInferInstanceOverClassOfFinite {n : Type u} (S : Scheme) [Finite n] : LocallyOfFinitePresentation (AffineSpace n S ↘ S)

theorem AlgebraicGeometry.AffineSpace.isOpenMap_over {n : Type u} (S : Scheme) : IsOpenMap ⇑(AffineSpace n S ↘ S)

instance AlgebraicGeometry.AffineSpace.instGeometricallyIrreducibleOverSchemeInferInstanceOverClass {n : Type u} (S : Scheme) : GeometricallyIrreducible (AffineSpace n S ↘ S)

instance AlgebraicGeometry.AffineSpace.instIrreducibleSpaceCarrierCarrierCommRingCat {n : Type u} (S : Scheme) [IrreducibleSpace ↥S] : IrreducibleSpace ↥(AffineSpace n S)

instance AlgebraicGeometry.AffineSpace.instGeometricallyReducedOverSchemeInferInstanceOverClass {n : Type u} (S : Scheme) : GeometricallyReduced (AffineSpace n S ↘ S)

instance AlgebraicGeometry.AffineSpace.instIsReduced {n : Type u} (S : Scheme) [h : IsReduced S] : IsReduced (AffineSpace n S)

instance AlgebraicGeometry.AffineSpace.instGeometricallyIntegralOverSchemeInferInstanceOverClass {n : Type u} (S : Scheme) : GeometricallyIntegral (AffineSpace n S ↘ S)

instance AlgebraicGeometry.AffineSpace.instIsIntegral {n : Type u} (S : Scheme) [IsIntegral S] : IsIntegral (AffineSpace n S)

instance AlgebraicGeometry.AffineSpace.instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty {n : Type u} (S : Scheme) [IsEmpty n] : CategoryTheory.IsIso (AffineSpace n S ↘ S)

theorem AlgebraicGeometry.AffineSpace.isIntegralHom_over_iff_isEmpty {n : Type u} (S : Scheme) : IsIntegralHom (AffineSpace n S ↘ S) ↔ IsEmpty ↥S ∨ IsEmpty n

theorem AlgebraicGeometry.AffineSpace.not_isIntegralHom {n : Type u} (S : Scheme) [Nonempty ↥S] [Nonempty n] : ¬IsIntegralHom (AffineSpace n S ↘ S)

theorem AlgebraicGeometry.AffineSpace.spec_le_iff (R : CommRingCat) (p q : ↥(Spec R)) : p ≤ q ↔ q.asIdeal ≤ p.asIdeal