Module

ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem

25 declarations indexed from sourceView source ↗

Module documentation

Proj Space away To Section mk mem span iff exists X pow mul mem

Imports14

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Mathlib.RingTheory.GradedAlgebra.Basic
Mathlib.RingTheory.MvPolynomial.Homogeneous
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Localization.Defs
Mathlib.GroupTheory.MonoidLocalization.Basic
Mathlib.Tactic.SplitIfs
Mathlib.Tactic.Conv
Mathlib.Tactic.Set
Nyll.SchemeTheory.ProjectiveSpace.Basic
Nyll.AlgebraicCurves.Hilbert.Functor.Basic

Imported by1

Nyll.AlgebraicCurves.Geometry.Projective.All

def

xpow

L52 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.xpow

Documentation

The power of a homogeneous coordinate, bundled in the homogeneous component of its degree.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

def xpow (i : Fin (n + 1)) (d : ℕ) : ↥(homogeneousSubmodule (Fin (n + 1)) A d)

def

frac

L58 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.frac

Documentation

The homogeneous fraction with the given numerator and a matching power of the chosen coordinate.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

def frac (i : Fin (n + 1)) (d : ℕ) (F : ↥(homogeneousSubmodule (Fin (n + 1)) A d)) :
    HomogeneousLocalization.Away 𝒜 (MvPolynomial.X i)

theorem

frac_zero

L66 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.frac_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem frac_zero (i : Fin (n + 1)) (d : ℕ) : frac (A := A) i d 0 = 0

theorem

frac_add

L72 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.frac_add

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem frac_add (i : Fin (n + 1)) (d : ℕ) (F G : ↥(homogeneousSubmodule (Fin (n + 1)) A d)) :
    frac i d (F + G) = frac i d F + frac i d G

theorem

frac_mul

L79 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.frac_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem frac_mul (i : Fin (n + 1)) (e d : ℕ) (G : ↥(homogeneousSubmodule (Fin (n + 1)) A e))
    (F : ↥(homogeneousSubmodule (Fin (n + 1)) A d)) :
    frac i (e + d) ⟨(G : MvPolynomial (Fin (n + 1)) A) * (F : MvPolynomial (Fin (n + 1)) A),
      SetLike.mul_mem_graded G.2 F.2⟩ = frac i e G * frac i d F

def

comp

L91 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.comp

Documentation

The homogeneous component of a polynomial, bundled with its degree membership.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

def comp (d : ℕ) (p : MvPolynomial (Fin (n + 1)) A) : ↥(homogeneousSubmodule (Fin (n + 1)) A d)

theorem

comp_zero

L94 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.comp_zero

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem comp_zero (d : ℕ) : comp (A := A) (n := n) d 0 = 0

theorem

comp_add

L96 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.comp_add

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem comp_add (d : ℕ) (p q : MvPolynomial (Fin (n + 1)) A) : comp d (p + q) = comp d p + comp d
  q

theorem

coe_decompose

L100 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.coe_decompose

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem coe_decompose (φ : MvPolynomial (Fin (n + 1)) A) (i : ℕ) :
    ((DirectSum.decompose 𝒜 φ) i : MvPolynomial (Fin (n + 1)) A) = homogeneousComponent i φ

theorem

homogeneousComponent_mul_of_mem_right

L104 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.homogeneousComponent_mul_of_mem_right

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · full declaration

theorem homogeneousComponent_mul_of_mem_right {e : ℕ} (a : MvPolynomial (Fin (n + 1)) A)
    {g : MvPolynomial (Fin (n + 1)) A} (hg : g ∈ homogeneousSubmodule (Fin (n + 1)) A e) (d : ℕ) :
    homogeneousComponent d (a * g) = if e ≤ d then homogeneousComponent (d - e) a * g else 0 := by
  have h := DirectSum.coe_decompose_mul_of_right_mem 𝒜 (a := a) d hg
  simpa only [coe_decompose] using h

theorem

comp_of_mem

L110 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.comp_of_mem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · full declaration

theorem comp_of_mem {e : ℕ} {F : MvPolynomial (Fin (n + 1)) A}
    (hF : F ∈ homogeneousSubmodule (Fin (n + 1)) A e) (d : ℕ) :
    comp d F = if h : d = e then ⟨F, h ▸ hF⟩ else 0 := by
  apply Subtype.ext
  simp only [comp, homogeneousComponent_of_mem hF]
  split_ifs <;> rfl

def

fcHom

L121 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.fcHom

Documentation

The additive map sending a polynomial to the localized fraction of its chosen homogeneous component.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · full declaration

def fcHom (i : Fin (n + 1)) (d : ℕ) :
    MvPolynomial (Fin (n + 1)) A →+ HomogeneousLocalization.Away 𝒜 (MvPolynomial.X i) where
  toFun p := frac i d (comp d p)
  map_zero' := by simp only [comp_zero, frac_zero]
  map_add' p q := by simp only [comp_add, frac_add]

theorem

fcHom_apply

L127 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.fcHom_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem fcHom_apply (i : Fin (n + 1)) (d : ℕ) (p : MvPolynomial (Fin (n + 1)) A) :
    fcHom (A := A) i d p = frac i d (comp d p)

theorem

fcHom_mul_of_mem

L130 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.fcHom_mul_of_mem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · full declaration

theorem fcHom_mul_of_mem (i : Fin (n + 1)) (d e : ℕ) (a : MvPolynomial (Fin (n + 1)) A)
    {g : MvPolynomial (Fin (n + 1)) A} (hg : g ∈ homogeneousSubmodule (Fin (n + 1)) A e) :
    fcHom (A := A) i d (a * g) = if e ≤ d then fcHom (A := A) i (d - e) a * frac i e ⟨g, hg⟩ else 0
      := by
  rcases Nat.lt_or_ge d e with hde | hed
  · rw [ite_eq_right (not_le.mpr hde), fcHom_apply]
    have h0 : comp d (a * g) = 0 := Subtype.ext (by
      simp only [comp, homogeneousComponent_mul_of_mem_right a hg d, ite_eq_right (not_le.mpr hde),
        Submodule.coe_zero])
    rw [h0, frac_zero]
  · obtain ⟨d', rfl⟩ := Nat.exists_eq_add_of_le' hed
    rw [ite_eq_left hed, fcHom_apply, fcHom_apply, Nat.add_sub_cancel]
    have h1 : comp (d' + e) (a * g) =
        ⟨(comp d' a : MvPolynomial (Fin (n + 1)) A) * ((⟨g, hg⟩ : ↥(𝒜 e)) : MvPolynomial (Fin (n +
          1)) A),
          SetLike.mul_mem_graded (comp d' a).2 hg⟩ := Subtype.ext (by
      simp only [comp, homogeneousComponent_mul_of_mem_right a hg (d' + e), ite_eq_left hed,
        Nat.add_sub_cancel])
    rw [h1, frac_mul]

theorem

fg_span_chart

L150 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.fg_span_chart

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section ChartIdeal
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem fg_span_chart (I : Ideal (MvPolynomial (Fin (n + 1)) A))
    (hI : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I) (hfg : I.FG) (i : Fin (n + 1)) :
    (Ideal.span { s | ∃ (d : ℕ) (F : MvPolynomial (Fin (n + 1)) A) (hF : F.IsHomogeneous d),
          F ∈ I ∧
          s = (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A) (X i))
              (HomogeneousLocalization.mk
                { deg := d
                  num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
                  den := ⟨X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                    (MvPolynomial.isHomogeneous_X_pow i d)⟩
                  den_mem := ⟨d, rfl⟩ }) }).FG

theorem

frac_congr

L227 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.frac_congr

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section Sat
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem frac_congr (i : Fin (n + 1)) {d d' : ℕ} (h : d = d') (F : ↥(𝒜 d)) (F' : ↥(𝒜 d'))
    (hF : (F : MvPolynomial (Fin (n + 1)) A) = F') : frac i d F = frac i d' F'

theorem

frac_xpow

L232 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.frac_xpow

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section Sat
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem frac_xpow (i : Fin (n + 1)) (N : ℕ) : frac i N (xpow (A := A) i N) = 1

theorem

frac_xpow_mul

L238 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.frac_xpow_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section Sat
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem frac_xpow_mul (i : Fin (n + 1)) (N d : ℕ) (F : ↥(𝒜 d)) :
    frac i (N + d) ⟨MvPolynomial.X i ^ N * (F : MvPolynomial (Fin (n + 1)) A),
      SetLike.mul_mem_graded (xpow (A := A) i N).2 F.2⟩ = frac i d F

theorem

frac_mul_xpow

L245 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.frac_mul_xpow

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section Sat
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem frac_mul_xpow (i : Fin (n + 1)) (d N : ℕ) (F : ↥(𝒜 d)) :
    frac i (d + N) ⟨(F : MvPolynomial (Fin (n + 1)) A) * MvPolynomial.X i ^ N,
      SetLike.mul_mem_graded F.2 (xpow (A := A) i N).2⟩ = frac i d F

theorem

awayMk_eq_frac

L252 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.awayMk_eq_frac

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section Sat
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem awayMk_eq_frac (i : Fin (n + 1)) (m : ℕ) (H : MvPolynomial (Fin (n + 1)) A)
    (hH : H ∈ 𝒜 (m • 1)) (hH' : H ∈ 𝒜 m) :
    HomogeneousLocalization.Away.mk 𝒜 (ProjSpace.X_mem_one A n i) m H hH = frac i m ⟨H, hH'⟩

def

InSat

L264 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.InSat

Documentation

Membership represented by a homogeneous numerator in the ideal and a matching coordinate-power denominator.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section Sat
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

def InSat (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (i : Fin (n + 1))
    (x : HomogeneousLocalization.Away 𝒜 (MvPolynomial.X i)) : Prop

def

satAway

L273 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.satAway

Documentation

The ideal of the chart localization represented by homogeneous fractions with numerator in the given ideal.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section Sat
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · full declaration

def satAway (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (i : Fin (n + 1)) :
    Ideal (HomogeneousLocalization.Away 𝒜 (MvPolynomial.X i)) where
  carrier := {x | InSat I i x}
  zero_mem' := by
    refine ⟨0, 0, MvPolynomial.isHomogeneous_zero _ _ _, I.zero_mem, ?_⟩
    rw [show (⟨(0 : MvPolynomial (Fin (n + 1)) A), (MvPolynomial.mem_homogeneousSubmodule 0 _).mpr
      (MvPolynomial.isHomogeneous_zero _ _ 0)⟩ : ↥(𝒜 0)) = 0 from Subtype.ext rfl, frac_zero]
  add_mem' := by
    rintro x y ⟨D, P, hP, hPI, rfl⟩ ⟨D', P', hP', hP'I, rfl⟩
    refine ⟨D + D', P * MvPolynomial.X i ^ D' + MvPolynomial.X i ^ D * P',
      (hP.mul (MvPolynomial.isHomogeneous_X_pow i D')).add ((MvPolynomial.isHomogeneous_X_pow i
        D).mul hP'),
      I.add_mem (I.mul_mem_right _ hPI) (I.mul_mem_left _ hP'I), ?_⟩
    rw [← frac_mul_xpow i D D' ⟨P, _⟩, ← frac_xpow_mul i D D' ⟨P', _⟩, ← frac_add]
    rfl
  smul_mem' := by
    rintro c x ⟨D, P, hP, hPI, rfl⟩
    obtain ⟨m, H, hH, rfl⟩ := HomogeneousLocalization.Away.mk_surjective 𝒜 (ProjSpace.X_mem_one A n
      i) c
    have hH' : H ∈ 𝒜 m := by simpa using hH
    have hHh : H.IsHomogeneous m := (MvPolynomial.mem_homogeneousSubmodule m H).mp hH'
    refine ⟨m + D, H * P, hHh.mul hP, I.mul_mem_left _ hPI, ?_⟩
    rw [smul_eq_mul, awayMk_eq_frac i m H hH hH', ← frac_mul]

theorem

mem_satAway_iff

L297 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.mem_satAway_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section Sat
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem mem_satAway_iff (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (i : Fin (n + 1))
    (x : HomogeneousLocalization.Away 𝒜 (MvPolynomial.X i)) : x ∈ satAway I i ↔ InSat I i x

theorem

exists_X_pow_mul_mem_of_inSat

L301 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem.K6SOL.exists_X_pow_mul_mem_of_inSat

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace K6SOL
section Sat
variable {A : Type} [CommRing A] {n : ℕ}
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A

Lean source · statement

theorem exists_X_pow_mul_mem_of_inSat (I : Ideal (MvPolynomial (Fin (n + 1)) A)) (i : Fin (n + 1))
    (d : ℕ) (F : MvPolynomial (Fin (n + 1)) A) (hF : F.IsHomogeneous d)
    (h : InSat I i (frac i d ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩)) :
    ∃ N : ℕ, MvPolynomial.X i ^ N * F ∈ I

theorem

awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem

L323 ↗

AlgebraicGeometry.ProjSpace.awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
open K6SOL in

Lean source · statement

theorem _root_.AlgebraicGeometry.ProjSpace.awayToSection_mk_mem_span_iff_exists_X_pow_mul_mem
    (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
    (i : Fin (n + 1)) (d : ℕ) (F : MvPolynomial (Fin (n + 1)) A) (hF : F.IsHomogeneous d) :
    (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A) (X i))
      (HomogeneousLocalization.mk
        { deg := d
          num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
          den := ⟨X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
            (MvPolynomial.isHomogeneous_X_pow i d)⟩
          den_mem := ⟨d, rfl⟩ }) ∈
        Ideal.span { s | ∃ (d : ℕ) (F : MvPolynomial (Fin (n + 1)) A) (hF : F.IsHomogeneous d),
          F ∈ I ∧
          s = (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A) (X i))
              (HomogeneousLocalization.mk
                { deg := d
                  num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
                  den := ⟨X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                    (MvPolynomial.isHomogeneous_X_pow i d)⟩
                  den_mem := ⟨d, rfl⟩ }) } ↔
      ∃ N : ℕ, X i ^ N * F ∈ I

Module documentation

Proj Space away To Section mk mem span iff exists X pow mul mem

Declarations