NYLL
Module

ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
19 declarations indexed from sourceView source ↗

Module documentation

Proj Space eq comap map of ideal basic Open eq span

Imports10
Imported by1

Declarations

theorem

X_pow_mem

L71 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.X_pow_mem
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Dehom
variable {R : Type} [CommRing R] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem X_pow_mem (e : ℕ) : (X i : MvPolynomial (Fin (n + 1)) R) ^ e ∈ 𝒜 e
def

dh

L78 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.dh
Documentation

The section on the chosen projective chart represented by a homogeneous numerator divided by a matching coordinate power.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Dehom
variable {R : Type} [CommRing R] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
def dh (e : ℕ) (G : 𝒜 e) : Γ(Proj 𝒜, Proj.basicOpen 𝒜 (X i))
theorem

dh_add

L86 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.dh_add
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Dehom
variable {R : Type} [CommRing R] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem dh_add (e : ℕ) (G H : 𝒜 e) : dh n i e (G + H) = dh n i e G + dh n i e H
theorem

dh_zero

L94 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.dh_zero
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Dehom
variable {R : Type} [CommRing R] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem dh_zero (e : ℕ) : dh n i e (0 : 𝒜 e) = 0
theorem

dh_congr

L102 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.dh_congr
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Dehom
variable {R : Type} [CommRing R] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem dh_congr {e : ℕ} {G H : 𝒜 e} (h : (G : MvPolynomial (Fin (n + 1)) R) = H) :
    dh n i e G = dh n i e H
theorem

dh_eq_zero

L106 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.dh_eq_zero
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Dehom
variable {R : Type} [CommRing R] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem dh_eq_zero {e : ℕ} {G : 𝒜 e} (h : (G : MvPolynomial (Fin (n + 1)) R) = 0) : dh n i e G = 0
theorem

dh_mul

L110 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.dh_mul
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Dehom
variable {R : Type} [CommRing R] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem dh_mul (a b : ℕ) (G : 𝒜 a) (H : 𝒜 b) :
    dh n i (a + b) ⟨(G : MvPolynomial (Fin (n + 1)) R) * (H : MvPolynomial (Fin (n + 1)) R),
        SetLike.GradedMul.mul_mem G.2 H.2⟩ =
      dh n i a G * dh n i b H
theorem

dh_mul'

L122 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.dh_mul'
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Dehom
variable {R : Type} [CommRing R] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem dh_mul' {a b e : ℕ} (h : a + b = e) (G : 𝒜 a) (H : 𝒜 b) (K : 𝒜 e)
    (hK : (K : MvPolynomial (Fin (n + 1)) R) = (G : MvPolynomial (Fin (n + 1)) R) * (H :
      MvPolynomial (Fin (n + 1)) R)) :
    dh n i e K = dh n i a G * dh n i b H
theorem

dh_sum

L130 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.dh_sum
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Dehom
variable {R : Type} [CommRing R] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem dh_sum {ι : Type} (s : Finset ι) (e : ℕ) (G : ι → 𝒜 e) :
    dh n i e (∑ j ∈ s, G j) = ∑ j ∈ s, dh n i e (G j)
theorem

coe_decompose

L137 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.coe_decompose
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Dehom
variable {R : Type} [CommRing R] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem coe_decompose (G : MvPolynomial (Fin (n + 1)) R) (e : ℕ) :
    ((DirectSum.decompose 𝒜 G) e : MvPolynomial (Fin (n + 1)) R) = homogeneousComponent e G
theorem

decompose_sum_apply

L141 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.decompose_sum_apply
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Dehom
variable {R : Type} [CommRing R] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem decompose_sum_apply {ι : Type} (s : Finset ι) (f : ι → MvPolynomial (Fin (n + 1)) R) (e :
  ℕ) :
    DirectSum.decompose 𝒜 (∑ j ∈ s, f j) e = ∑ j ∈ s, DirectSum.decompose 𝒜 (f j) e
theorem

dh_decompose_mem_of_mem_span

L151 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.dh_decompose_mem_of_mem_span
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Dehom
variable {R : Type} [CommRing R] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem dh_decompose_mem_of_mem_span (S : Set (MvPolynomial (Fin (n + 1)) R))
    (T : Ideal Γ(Proj 𝒜, Proj.basicOpen 𝒜 (X i)))
    (hS : ∀ p ∈ S, ∀ e : ℕ, dh n i e (DirectSum.decompose 𝒜 p e) ∈ T)
    {F : MvPolynomial (Fin (n + 1)) R} (hF : F ∈ Ideal.span S) :
    ∀ e : ℕ, dh n i e (DirectSum.decompose 𝒜 F e) ∈ T
theorem

decompose_of_isHomogeneous

L182 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.decompose_of_isHomogeneous
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Dehom
variable {R : Type} [CommRing R] (n : ℕ) (i : Fin (n + 1))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem decompose_of_isHomogeneous {d : ℕ} {F : MvPolynomial (Fin (n + 1)) R} (hF : F.IsHomogeneous
  d) :
    DirectSum.decompose 𝒜 F d = ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
theorem

homogeneousComponent_map

L198 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.homogeneousComponent_map
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Map
variable (n : ℕ) (A B : Type) [CommRing A] [CommRing B] [Algebra A B] (i : Fin (n + 1))
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
local notation "φ" => MvPolynomial.map (algebraMap A B)
Lean source · statement
theorem homogeneousComponent_map (e : ℕ) (p : MvPolynomial (Fin (n + 1)) A) :
    homogeneousComponent e (φ p) = φ (homogeneousComponent e p)
theorem

coe_decompose_map

L204 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.coe_decompose_map
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Map
variable (n : ℕ) (A B : Type) [CommRing A] [CommRing B] [Algebra A B] (i : Fin (n + 1))
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
local notation "φ" => MvPolynomial.map (algebraMap A B)
Lean source · statement
theorem coe_decompose_map (e : ℕ) (p : MvPolynomial (Fin (n + 1)) A) :
    ((DirectSum.decompose 𝒜B (φ p)) e : MvPolynomial (Fin (n + 1)) B) =
      φ ((DirectSum.decompose 𝒜A p) e : MvPolynomial (Fin (n + 1)) A)
theorem

basicOpen_le_preimage

L209 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.basicOpen_le_preimage
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Map
variable (n : ℕ) (A B : Type) [CommRing A] [CommRing B] [Algebra A B] (i : Fin (n + 1))
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
local notation "φ" => MvPolynomial.map (algebraMap A B)
Lean source · statement
theorem basicOpen_le_preimage :
    Proj.basicOpen 𝒜B (X i) ≤ ProjSpace.map A B n ⁻¹ᵁ Proj.basicOpen 𝒜A (X i)
theorem

map_mem

L213 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.map_mem
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Map
variable (n : ℕ) (A B : Type) [CommRing A] [CommRing B] [Algebra A B] (i : Fin (n + 1))
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
local notation "φ" => MvPolynomial.map (algebraMap A B)
Lean source · statement
theorem map_mem (e : ℕ) (G : 𝒜A e) : φ (G : MvPolynomial (Fin (n + 1)) A) ∈ 𝒜B e
theorem

appLE_dh

L219 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.BCComap.appLE_dh
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace BCComap
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
section Map
variable (n : ℕ) (A B : Type) [CommRing A] [CommRing B] [Algebra A B] (i : Fin (n + 1))
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "𝒜B" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B
local notation "φ" => MvPolynomial.map (algebraMap A B)
Lean source · statement
theorem appLE_dh (e : ℕ) (G : 𝒜A e) :
    (ProjSpace.map A B n).appLE (Proj.basicOpen 𝒜A (X i)) (Proj.basicOpen 𝒜B (X i))
        (basicOpen_le_preimage n A B i) (dh n i e G) =
      dh n i e ⟨φ (G : MvPolynomial (Fin (n + 1)) A), map_mem n A B e G⟩
theorem

eq_comap_map_of_ideal_basicOpen_eq_span

L263 ↗
AlgebraicGeometry.ProjSpace.eq_comap_map_of_ideal_basicOpen_eq_span
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_eq_comap_map_of_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.HilbertFunctor
Lean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.eq_comap_map_of_ideal_basicOpen_eq_span
    (n : ℕ) (A B : Type) [CommRing A] [CommRing B] [Algebra A B]
    (I : Ideal (MvPolynomial (Fin (n + 1)) A))
    (hI : ∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I)
    (𝓘 : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)).IdealSheafData)
    (h𝓘 : ∀ i : Fin (n + 1),
        𝓘.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A) (X i),
          Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A) (X i)
            (ProjSpace.X_mem_one A n i) one_pos⟩ =
        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⟩ }) })
    (𝓙 : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)).IdealSheafData)
    (h𝓙 : ∀ i : Fin (n + 1),
        𝓙.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B) (X i),
          Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B) (X i)
            (ProjSpace.X_mem_one B n i) one_pos⟩ =
        Ideal.span { s | ∃ (d : ℕ) (F : MvPolynomial (Fin (n + 1)) B) (hF : F.IsHomogeneous d),
          F ∈ I.map (MvPolynomial.map (algebraMap A B)) ∧
          s = (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B) (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⟩ }) }) :
    𝓙 = 𝓘.comap (ProjSpace.map A B n)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.