Module

StandardChartsBaseChange.lean

Nyll.SchemeTheory.ProjectiveSpace.StandardChartsBaseChange

1 declaration indexed from sourceView source ↗

Module documentation

Coordinate opens under projective-space base change

The inverse image of a coordinate basic open under the base-change map of projective spaces is the corresponding coordinate basic open over the new ring.

Imports1

Nyll.SchemeTheory.ProjectiveSpace.Basic

Imported by10

theorem

map_preimage_basicOpen_X

L34 ↗

AlgebraicGeometry.ProjSpace.map_preimage_basicOpen_X

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_map_preimage_basicOpen_X
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry MvPolynomial
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem _root_.AlgebraicGeometry.ProjSpace.map_preimage_basicOpen_X (R A : Type u) [CommRing R]
    [CommRing A] [Algebra R A] (n : ℕ) (j : Fin (n + 1)) :
    ProjSpace.map R A n ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
        (MvPolynomial.X j)
      = Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A) (MvPolynomial.X j)

Module documentation

Coordinate opens under projective-space base change

Declarations

map_preimage_basicOpen_X