Documentation

LeanPool.CCDN.Algebra.ProjectiveClosureIdeal

The projective closure ideal of an affine coordinate ideal. The homogenizing parameter is a polynomial variable over the affine quotient, so primeness and homogeneous components are proved directly.

source
noncomputable def CCDN.projectiveClosureMap {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) :
MvPolynomial (Fin (n + 1)) K →ₐ[K] Polynomial (MvPolynomial (Fin n) K ⧸ I)

Send the homogenizing coordinate to t and every affine coordinate to its quotient class times t.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CCDN.projectiveClosureMap_coeff {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) (f : MvPolynomial (Fin (n + 1)) K) (M : ℕ) :
    ((projectiveClosureMap I) f).coeff M = (Ideal.Quotient.mk I) ((affineChart n) ((MvPolynomial.homogeneousComponent M) f))

    The coefficient of t ^ M in projectiveClosureMap I f is the class modulo I of the dehomogenization of the degree-M homogeneous component of f.

    source
    noncomputable def CCDN.projectiveClosureIdeal {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) :
    Ideal (MvPolynomial (Fin (n + 1)) K)

    The projective closure of the affine coordinate ideal I: the homogeneous ideal of polynomials in n + 1 variables all of whose homogeneous components dehomogenize (by setting X 0 = 1) into I, defined as the kernel of projectiveClosureMap I.

    Equations
    Instances For
      source
      instance CCDN.projectiveClosureIdeal_isPrime {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) [I.IsPrime] :
      (projectiveClosureIdeal I).IsPrime
      source
      theorem CCDN.mem_projectiveClosureIdeal_iff {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) (f : MvPolynomial (Fin (n + 1)) K) :
      f ∈ projectiveClosureIdeal I ↔ ∀ (M : ℕ), (affineChart n) ((MvPolynomial.homogeneousComponent M) f) ∈ I

      A polynomial lies in the projective closure ideal of I if and only if the dehomogenization of each of its homogeneous components lies in I.

      source
      theorem CCDN.homogeneous_mem_projectiveClosureIdeal_iff {K : Type u_1} [Field K] {n M : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) (f : MvPolynomial (Fin (n + 1)) K) (hf : f.IsHomogeneous M) :
      f ∈ projectiveClosureIdeal I ↔ (affineChart n) f ∈ I

      A homogeneous polynomial lies in the projective closure ideal of I if and only if its dehomogenization lies in I.

      source
      theorem CCDN.projectiveClosureIdeal_homogeneous {K : Type u_1} [Field K] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) (f : MvPolynomial (Fin (n + 1)) K) (hf : f ∈ projectiveClosureIdeal I) (M : ℕ) :
      (MvPolynomial.homogeneousComponent M) f ∈ projectiveClosureIdeal I

      The projective closure ideal is homogeneous: every homogeneous component of a member is a member.

      source
      theorem CCDN.projectiveClosureIdeal_scalar_extension {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) :
      Ideal.map (MvPolynomial.map (algebraMap K L)) (projectiveClosureIdeal I) = projectiveClosureIdeal (Ideal.map (MvPolynomial.map (algebraMap K L)) I)

      Closure commutes with arbitrary coefficient-field extension.

      source
      theorem CCDN.projectiveClosureIdeal_geometrically_prime {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) [(Ideal.map (MvPolynomial.map (algebraMap K L)) I).IsPrime] :
      (Ideal.map (MvPolynomial.map (algebraMap K L)) (projectiveClosureIdeal I)).IsPrime

      If the extension of I to a field extension L of K is prime, then so is the extension of the projective closure ideal of I to L.