Nyll.AlgebraicCurves.Hilbert.exists_point_I_eq_map

theorem

exists_point_I_eq_map

AlgebraicGeometry.HilbertFunctor.exists_point_I_eq_map

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_point_I_eq_map
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct

Lean source · statement

theorem _root_.AlgebraicGeometry.HilbertFunctor.exists_point_I_eq_map
    (n : ℕ) (h : ℕ → ℕ) (A B : Type) [CommRing A] [CommRing B] [Algebra A B] (P : Point A n h) :
    ∃ Q : Point B n h, Q.I = P.I.map (MvPolynomial.map (algebraMap A B))

exists_point_I_eq_map.lean

Module documentation

exists point I eq map

exists_point_I_eq_map

Module documentation

exists point I eq map

Declarations

exists_point_I_eq_map