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]

def AlgebraicGeometry.AffineSpace (n : Type v) (S : AlgebraicGeometry.Scheme) : AlgebraicGeometry.Scheme

𝔸(n; S) is the affine n-space over S. Note that n is an arbitrary index type (e.g. 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 v} {R : CommRingCat} {f g : CommRingCat.of (MvPolynomial n (ULift.{u_1, 0} ℤ)) ⟶ R} (h : ∀ (i : n), f (MvPolynomial.X i) = g (MvPolynomial.X i)) : f = g

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

Equations

• AlgebraicGeometry.AffineSpace.over n S = CategoryTheory.CanonicallyOverClass.mk

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

def AlgebraicGeometry.AffineSpace.toSpecMvPoly (n : Type v) (S : AlgebraicGeometry.Scheme) : AlgebraicGeometry.AffineSpace n S ⟶ AlgebraicGeometry.Spec (CommRingCat.of (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.

def AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv (n : Type v) {X : AlgebraicGeometry.Scheme} : (X ⟶ AlgebraicGeometry.Spec (CommRingCat.of (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 v) {X : AlgebraicGeometry.Scheme} (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) : (AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n).symm v = CategoryTheory.CategoryStruct.comp X.toSpecΓ (AlgebraicGeometry.Spec.map (MvPolynomial.eval₂Hom ((algebraMap ℤ ↑(X.presheaf.obj (Opposite.op ⊤))).comp ULift.ringEquiv.toRingHom) v))

@[simp]

theorem AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply (n : Type v) {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of (MvPolynomial n (ULift.{u, 0} ℤ)))) (i : n) : (AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n) f i = (AlgebraicGeometry.Scheme.Hom.app f ⊤) ((AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n (ULift.{u, 0} ℤ)))).inv (MvPolynomial.X i))

theorem AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp (n : Type v) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ AlgebraicGeometry.Spec (CommRingCat.of (MvPolynomial n (ULift.{u_1, 0} ℤ)))) (i : n) : (AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n) (CategoryTheory.CategoryStruct.comp f g) i = (AlgebraicGeometry.Scheme.Hom.app f ⊤) ((AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n) g i)

def AlgebraicGeometry.AffineSpace.coord {n : Type v} (S : AlgebraicGeometry.Scheme) (i : n) : ↑((AlgebraicGeometry.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

def AlgebraicGeometry.AffineSpace.homOfVector {n : Type v} {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) : X ⟶ AlgebraicGeometry.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 v} {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.homOfVector f v) (AlgebraicGeometry.AffineSpace n S ↘ S) = f

@[simp]

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

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

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

theorem AlgebraicGeometry.AffineSpace.homOfVector_app_top_coord {n : Type v} {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))) (i : n) : (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.AffineSpace.homOfVector f v) ⊤) (AlgebraicGeometry.AffineSpace.coord S i) = v i

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

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

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

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

Equations

• ⋯ = ⋯

def AlgebraicGeometry.AffineSpace.homOverEquiv {n : Type v} (S : AlgebraicGeometry.Scheme) {X : AlgebraicGeometry.Scheme} [X.Over S] : { f : X ⟶ AlgebraicGeometry.AffineSpace n S // AlgebraicGeometry.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_apply {n : Type v} (S : AlgebraicGeometry.Scheme) {X : AlgebraicGeometry.Scheme} [X.Over S] (f : { f : X ⟶ AlgebraicGeometry.AffineSpace n S // AlgebraicGeometry.Scheme.Hom.IsOver f S }) (i : n) : (AlgebraicGeometry.AffineSpace.homOverEquiv S) f i = (AlgebraicGeometry.Scheme.Hom.app ↑f ⊤) (AlgebraicGeometry.AffineSpace.coord S i)

@[simp]

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

def AlgebraicGeometry.AffineSpace.isoOfIsAffine (n : Type v) (S : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine S] : AlgebraicGeometry.AffineSpace n S ≅ AlgebraicGeometry.Spec (CommRingCat.of (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 v) (S : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine S] : (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).inv = AlgebraicGeometry.AffineSpace.homOfVector (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map MvPolynomial.C) S.isoSpec.inv) (⇑(AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑(S.presheaf.obj (Opposite.op ⊤))))).inv ∘ MvPolynomial.X)

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

@[simp]

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

theorem AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_app_top_coord {n : Type v} (S : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine S] (i : n) : (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).inv ⊤) (AlgebraicGeometry.AffineSpace.coord S i) = (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑(S.presheaf.obj (Opposite.op ⊤))))).inv (MvPolynomial.X i)

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

def AlgebraicGeometry.AffineSpace.SpecIso (n : Type v) (R : CommRingCat) : AlgebraicGeometry.AffineSpace n (AlgebraicGeometry.Spec R) ≅ AlgebraicGeometry.Spec (CommRingCat.of (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_app_top {n : Type v} (R : CommRingCat) : AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.AffineSpace.SpecIso n R).hom ⊤ = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).hom (MvPolynomial.eval₂Hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.AffineSpace n (AlgebraicGeometry.Spec R) ↘ AlgebraicGeometry.Spec R) ⊤)) (AlgebraicGeometry.AffineSpace.coord (AlgebraicGeometry.Spec R)))

theorem AlgebraicGeometry.AffineSpace.SpecIso_inv_app_top_coord {n : Type v} (R : CommRingCat) (i : n) : (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.AffineSpace.SpecIso n R).inv ⊤) (AlgebraicGeometry.AffineSpace.coord (AlgebraicGeometry.Spec R) i) = (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv (MvPolynomial.X i)

@[simp]

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

@[simp]

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

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

𝔸(n; S) is functorial wrt S.

Equations

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

@[simp]

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

@[simp]

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

theorem AlgebraicGeometry.AffineSpace.map_app_top_coord {n : Type v} {S T : AlgebraicGeometry.Scheme} (f : S ⟶ T) (i : n) : (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.AffineSpace.map n f) ⊤) (AlgebraicGeometry.AffineSpace.coord T i) = AlgebraicGeometry.AffineSpace.coord S i

@[simp]

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

@[simp]

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

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

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

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

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) ⋯

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

𝔸(n; S) is functorial wrt 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 v} (i : m → n) (S : AlgebraicGeometry.Scheme) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.reindex i S) (AlgebraicGeometry.AffineSpace m S ↘ S) = AlgebraicGeometry.AffineSpace n S ↘ S

@[simp]

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

theorem AlgebraicGeometry.AffineSpace.reindex_app_top_coord {n m : Type v} (i : m → n) (S : AlgebraicGeometry.Scheme) (j : m) : (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.AffineSpace.reindex i S) ⊤) (AlgebraicGeometry.AffineSpace.coord S j) = AlgebraicGeometry.AffineSpace.coord S (i j)

@[simp]

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

@[simp]

theorem AlgebraicGeometry.AffineSpace.reindex_comp {n₁ n₂ n₃ : Type v} (i : n₁ → n₂) (j : n₂ → n₃) (S : AlgebraicGeometry.Scheme) : AlgebraicGeometry.AffineSpace.reindex (j ∘ i) S = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.reindex j S) (AlgebraicGeometry.AffineSpace.reindex i S)

theorem AlgebraicGeometry.AffineSpace.reindex_comp_assoc {n₁ n₂ n₃ : Type v} (i : n₁ → n₂) (j : n₂ → n₃) (S : AlgebraicGeometry.Scheme) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.AffineSpace n₁ S ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.reindex (j ∘ i) S) h = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.reindex j S) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.reindex i S) h)

@[simp]

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

@[simp]

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

def AlgebraicGeometry.AffineSpace.functor : CategoryTheory.Functor Type vᵒᵖ (CategoryTheory.Functor AlgebraicGeometry.Scheme AlgebraicGeometry.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_map_app {n m : Type vᵒᵖ} (i : n ⟶ m) (S : AlgebraicGeometry.Scheme) : (AlgebraicGeometry.AffineSpace.functor.map i).app S = AlgebraicGeometry.AffineSpace.reindex i.unop S

@[simp]

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

@[simp]

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