NYLL
Module

ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
15 declarations indexed from sourceView source ↗

Module documentation

Proj Space spec Map comp away Inclusion eq of forall apply ratio mul eq

Imports2
Imported by2

Declarations

theorem

X_mul_comm

L38 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.X_mul_comm
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
Lean source · statement
theorem X_mul_comm (i j : Fin (n + 1)) : XX i * XX j = XX j * XX i
abbrev

mapI

L41 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.mapI
Documentation

The localization map from chart i to the overlap of charts i and j.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
Lean source · statement
abbrev mapI (i j : Fin (n + 1)) : Away 𝒜 (XX i) →+* Away 𝒜 (XX i * XX j)
abbrev

mapJ

L45 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.mapJ
Documentation

The localization map from chart j to the overlap of charts i and j.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
Lean source · statement
abbrev mapJ (i j : Fin (n + 1)) : Away 𝒜 (XX j) →+* Away 𝒜 (XX i * XX j)
theorem

mapJ_ratio_mul_mapI_ratio

L48 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.mapJ_ratio_mul_mapI_ratio
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
Lean source · statement
theorem mapJ_ratio_mul_mapI_ratio (i j l : Fin (n + 1)) :
    mapJ R n i j (ProjSpace.ratio R n j l) * mapI R n i j (ProjSpace.ratio R n i j) =
      mapI R n i j (ProjSpace.ratio R n i l)
theorem

isLocalizationElem_eq

L58 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.isLocalizationElem_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
Lean source · statement
theorem isLocalizationElem_eq (i j : Fin (n + 1)) :
    Away.isLocalizationElem (ProjSpace.X_mem_one R n i) (ProjSpace.X_mem_one R n j) =
      ProjSpace.ratio R n i j
theorem

mapI_algebraMap

L64 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.mapI_algebraMap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
Lean source · statement
theorem mapI_algebraMap (i j : Fin (n + 1)) (r : R) :
    mapI R n i j (algebraMap R (Away 𝒜 (XX i)) r) = mapJ R n i j (algebraMap R (Away 𝒜 (XX j)) r)
theorem

isUnit_ψi_ratio

L80 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.isUnit_ψi_ratio
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
section lift
variable {B : Type u} [CommRing B] [Algebra R B] (a : Fin (n + 1) → B) (i j : Fin (n + 1))
  (hj : IsUnit (a j))
  (ψi : Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
    (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B)
  (hψi : ∀ l, ψi (ProjSpace.ratio R n i l) * a i = a l)
include hj hψi in
Lean source · statement
theorem isUnit_ψi_ratio : IsUnit (ψi (ProjSpace.ratio R n i j))
theorem

isUnit_ψi_elem

L84 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.isUnit_ψi_elem
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
section lift
variable {B : Type u} [CommRing B] [Algebra R B] (a : Fin (n + 1) → B) (i j : Fin (n + 1))
  (hj : IsUnit (a j))
  (ψi : Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
    (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B)
  (hψi : ∀ l, ψi (ProjSpace.ratio R n i l) * a i = a l)
include hj hψi in
Lean source · statement
theorem isUnit_ψi_elem :
    IsUnit (ψi.toRingHom (Away.isLocalizationElem (ProjSpace.X_mem_one R n i) (ProjSpace.X_mem_one
      R n j)))
def

liftij

L94 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.liftij
Documentation

The overlap homomorphism obtained by lifting ψi through the localization where the second coordinate ratio is a unit.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
section lift
variable {B : Type u} [CommRing B] [Algebra R B] (a : Fin (n + 1) → B) (i j : Fin (n + 1))
  (hj : IsUnit (a j))
  (ψi : Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
    (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B)
  (hψi : ∀ l, ψi (ProjSpace.ratio R n i l) * a i = a l)
Lean source · statement
def liftij : Away 𝒜 (XX i * XX j) →+* B
theorem

liftij_mapI

L102 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.liftij_mapI
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
section lift
variable {B : Type u} [CommRing B] [Algebra R B] (a : Fin (n + 1) → B) (i j : Fin (n + 1))
  (hj : IsUnit (a j))
  (ψi : Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
    (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B)
  (hψi : ∀ l, ψi (ProjSpace.ratio R n i l) * a i = a l)
Lean source · statement
theorem liftij_mapI (z : Away 𝒜 (XX i)) : liftij R n a i j hj ψi hψi (mapI R n i j z) = ψi z
theorem

liftij_mapJ

L110 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.liftij_mapJ
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
section lift
variable {B : Type u} [CommRing B] [Algebra R B] (a : Fin (n + 1) → B) (i j : Fin (n + 1))
  (hj : IsUnit (a j))
  (ψi : Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
    (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B)
  (hψi : ∀ l, ψi (ProjSpace.ratio R n i l) * a i = a l)
Lean source · statement
theorem liftij_mapJ
    (ψj : Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
      (MvPolynomial.X j : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B)
    (hψj : ∀ l, ψj (ProjSpace.ratio R n j l) * a j = a l)
    (z : Away 𝒜 (XX j)) : liftij R n a i j hj ψi hψi (mapJ R n i j z) = ψj z
theorem

ψi_eq_comp

L131 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.ψi_eq_comp
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
section lift
variable {B : Type u} [CommRing B] [Algebra R B] (a : Fin (n + 1) → B) (i j : Fin (n + 1))
  (hj : IsUnit (a j))
  (ψi : Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
    (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B)
  (hψi : ∀ l, ψi (ProjSpace.ratio R n i l) * a i = a l)
Lean source · statement
theorem ψi_eq_comp : ψi.toRingHom = (liftij R n a i j hj ψi hψi).comp (mapI R n i j)
theorem

ψj_eq_comp

L134 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.ψj_eq_comp
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
section lift
variable {B : Type u} [CommRing B] [Algebra R B] (a : Fin (n + 1) → B) (i j : Fin (n + 1))
  (hj : IsUnit (a j))
  (ψi : Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
    (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B)
  (hψi : ∀ l, ψi (ProjSpace.ratio R n i l) * a i = a l)
Lean source · statement
theorem ψj_eq_comp
    (ψj : Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
      (MvPolynomial.X j : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B)
    (hψj : ∀ l, ψj (ProjSpace.ratio R n j l) * a j = a l) :
    ψj.toRingHom = (liftij R n a i j hj ψi hψi).comp (mapJ R n i j)
theorem

main

L141 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq.ProjPointEq.main
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
namespace ProjPointEq
variable (R : Type u) [CommRing R] (n : ℕ)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "XX" => (MvPolynomial.X : Fin (n + 1) → MvPolynomial (Fin (n + 1)) R)
section lift
variable {B : Type u} [CommRing B] [Algebra R B] (a : Fin (n + 1) → B) (i j : Fin (n + 1))
  (hj : IsUnit (a j))
  (ψi : Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
    (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B)
  (hψi : ∀ l, ψi (ProjSpace.ratio R n i l) * a i = a l)
include hj hψi in
Lean source · statement
theorem main
    (ψj : Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
      (MvPolynomial.X j : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B)
    (hψj : ∀ l, ψj (ProjSpace.ratio R n j l) * a j = a l) :
    Spec.map (CommRingCat.ofHom ψi.toRingHom) ≫
        Proj.awayι 𝒜 (XX i) (ProjSpace.X_mem_one R n i) one_pos =
      Spec.map (CommRingCat.ofHom ψj.toRingHom) ≫
        Proj.awayι 𝒜 (XX j) (ProjSpace.X_mem_one R n j) one_pos
theorem

specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq

L162 ↗
AlgebraicGeometry.ProjSpace.specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
universe u
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem
  _root_.AlgebraicGeometry.ProjSpace.specMap_comp_awayInclusion_eq_of_forall_apply_ratio_mul_eq
    (R : Type u) [CommRing R] (n : ℕ) (B : Type u) [CommRing B] [Algebra R B]
    (a : Fin (n + 1) → B) (i j : Fin (n + 1)) (_hi : IsUnit (a i)) (hj : IsUnit (a j))
    (ψi : HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
        (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B)
    (ψj : HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
        (MvPolynomial.X j : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B)
    (hψi : ∀ l, ψi (ProjSpace.ratio R n i l) * a i = a l)
    (hψj : ∀ l, ψj (ProjSpace.ratio R n j l) * a j = a l) :
    Spec.map (CommRingCat.ofHom ψi.toRingHom) ≫
        Proj.awayι (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R) (MvPolynomial.X i)
          (ProjSpace.X_mem_one R n i) one_pos =
      Spec.map (CommRingCat.ofHom ψj.toRingHom) ≫
        Proj.awayι (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R) (MvPolynomial.X j)
          (ProjSpace.X_mem_one R n j) one_pos

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