NYLL
Module

ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
17 declarations indexed from sourceView source ↗

Module documentation

Proj Space exists linear Equiv twist Obj of le pullback Chart

Imports3
Imported by5

Declarations

theorem

le_inf_chart

L40 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.le_inf_chart
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
theorem le_inf_chart (hW : W ≤ pullbackChart φ i) : W ≤ W ⊓ pullbackChart φ i
theorem

res_down_up

L42 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.res_down_up
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
theorem res_down_up (hW : W ≤ pullbackChart φ i) (x : Γ(X, W ⊓ pullbackChart φ i)) :
    restrictFun (inf_le_left : W ⊓ pullbackChart φ i ≤ W) (restrictFun (le_inf_chart φ hW) x) = x
theorem

res_up_down

L47 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.res_up_down
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
theorem res_up_down (hW : W ≤ pullbackChart φ i) (a : Γ(X, W)) :
    restrictFun (le_inf_chart φ hW) (restrictFun (inf_le_left : W ⊓ pullbackChart φ i ≤ W) a) = a
def

fwd

L53 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.fwd
Documentation

Restriction of the chosen chart component, giving a linear map to regular functions.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · full declaration
def fwd (hW : W ≤ pullbackChart φ i) : twistObj π φ m W →ₗ[Γ(X, W)] Γ(X, W) where
  toFun g := restrictFun (le_inf_chart φ hW) (g.val i)
  map_add' g g' := by
    show restrictFun _ ((g + g').val i) = _
    rw [twistObj.add_val, Pi.add_apply, map_add]
  map_smul' a g := by
    change restrictFun _ ((a • g).val i) = a * restrictFun _ (g.val i)
    rw [twistObj.smul_val, map_mul, res_up_down φ hW]
theorem

fwd_apply

L62 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.fwd_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
theorem fwd_apply (hW : W ≤ pullbackChart φ i) (g : twistObj π φ m W) :
    fwd π φ m hW g = restrictFun (le_inf_chart φ hW) (g.val i)
def

invVal

L66 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.invVal
Documentation

The chart components obtained by multiplying a function by the powers of the frame units.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
def invVal (i : Fin (N + 1)) (a : Γ(X, W)) (j : Fin (N + 1)) : Γ(X, W ⊓ pullbackChart
  φ j)
theorem

cocycle_res

L71 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.cocycle_res
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
theorem cocycle_res (i j l : Fin (N + 1)) :
    restrictFun (le_trans inf_le_left inf_le_right : (W ⊓ pullbackChart φ j) ⊓ pullbackChart φ l ≤
      pullbackChart φ j)
        (frameUnit φ j l) *
      restrictFun (inf_le_right : (W ⊓ pullbackChart φ j) ⊓ pullbackChart φ l ≤ pullbackChart φ l)
        (frameUnit φ l i)
      = restrictFun (le_trans inf_le_left inf_le_right : (W ⊓ pullbackChart φ j) ⊓ pullbackChart φ
        l ≤ pullbackChart φ j)
        (frameUnit φ j i)
theorem

invVal_compat

L86 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.invVal_compat
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
theorem invVal_compat (i : Fin (N + 1)) (a : Γ(X, W)) : TwistCompat φ m W (invVal φ m i a)
def

inv

L105 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.inv
Documentation

The twisted section whose chart components are obtained from the given regular function.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
def inv (i : Fin (N + 1)) (a : Γ(X, W)) : twistObj π φ m W
theorem

inv_val

L108 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.inv_val
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
theorem inv_val (a : Γ(X, W)) (j : Fin (N + 1)) : (inv π φ m i a).val j = invVal φ m i a j
theorem

fwd_inv

L110 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.fwd_inv
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
theorem fwd_inv (hW : W ≤ pullbackChart φ i) (a : Γ(X, W)) : fwd π φ m hW (inv π φ m i a) = a
theorem

inv_fwd

L113 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.inv_fwd
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
theorem inv_fwd (hW : W ≤ pullbackChart φ i) (g : twistObj π φ m W) : inv π φ m i (fwd π φ m hW g)
  = g
def

equiv

L125 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.equiv
Documentation

The linear trivialization of the twist on an open contained in the chosen chart.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
def equiv (hW : W ≤ pullbackChart φ i) : twistObj π φ m W ≃ₗ[Γ(X, W)] Γ(X, W)
theorem

equiv_apply

L131 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.equiv_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
theorem equiv_apply (hW : W ≤ pullbackChart φ i) (g : twistObj π φ m W) :
    equiv π φ m hW g = restrictFun (le_inf_chart φ hW) (g.val i)
theorem

equiv_symm_apply

L134 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.equiv_symm_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
theorem equiv_symm_apply (hW : W ≤ pullbackChart φ i) (a : Γ(X, W)) : (equiv π φ m hW).symm a = inv
  π φ m i a
theorem

main

L137 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart.P2mTwistChartTriv.main
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mTwistChartTriv
open AlgebraicGeometry.ProjSpace
variable {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
  (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
  (m : ℕ) {i : Fin (N + 1)} {W : X.Opens}
Lean source · statement
theorem main (hW : W ≤ pullbackChart φ i) :
    ∃ e : twistObj π φ m W ≃ₗ[Γ(X, W)] Γ(X, W),
      (∀ g : twistObj π φ m W,
        restrictFun (inf_le_left : W ⊓ pullbackChart φ i ≤ W) (e g) = g.val i) ∧
      (∀ (a : Γ(X, W)) (j : Fin (N + 1)),
        (e.symm a).val j =
          restrictFun (inf_le_right : W ⊓ pullbackChart φ j ≤ pullbackChart φ j) (frameUnit φ j i)
            ^ m *
            restrictFun (inf_le_left : W ⊓ pullbackChart φ j ≤ W) a)
theorem

exists_linearEquiv_twistObj_of_le_pullbackChart

L151 ↗
AlgebraicGeometry.ProjSpace.exists_linearEquiv_twistObj_of_le_pullbackChart
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_linearEquiv_twistObj_of_le_pullbackChart
open CategoryTheory AlgebraicGeometry
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.exists_linearEquiv_twistObj_of_le_pullbackChart
    {A : Type u} [CommRing A] {N : ℕ} {X : Scheme.{u}}
    (π : X ⟶ Spec (.of A)) (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
    (m : ℕ) {i : Fin (N + 1)} {W : X.Opens} (hW : W ≤ ProjSpace.pullbackChart φ i) :
    ∃ e : ProjSpace.twistObj π φ m W ≃ₗ[Γ(X, W)] Γ(X, W),
      (∀ g : ProjSpace.twistObj π φ m W,
        ProjSpace.restrictFun (inf_le_left : W ⊓ ProjSpace.pullbackChart φ i ≤ W) (e g) = g.val i) ∧
      (∀ (a : Γ(X, W)) (j : Fin (N + 1)),
        (e.symm a).val j =
          ProjSpace.restrictFun (inf_le_right : W ⊓ ProjSpace.pullbackChart φ j ≤
            ProjSpace.pullbackChart φ j)
              (ProjSpace.frameUnit φ j i) ^ m *
            ProjSpace.restrictFun (inf_le_left : W ⊓ ProjSpace.pullbackChart φ j ≤ W) a)

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