NYLL
Module

BaseChange.lean

Nyll.SchemeTheory.ProjectiveSpace.BaseChange
30 declarations indexed from sourceView source ↗

Module documentation

Projective space under extension of coefficients

The morphism of projective spaces induced by an algebra map is a pullback of the structural morphism. Polynomial scalar extension identifies the affine charts and their overlaps.

Imports4
Imported by12

Declarations

def

awayMapX

L55 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.awayMapX
Documentation

The homomorphism between standard homogeneous localization charts induced by coefficient extension.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
def awayMapX (j : Fin (n + 1)) :
    Away 𝒜R (MvPolynomial.X j) →+* Away 𝒜A (MvPolynomial.X j)
theorem

awayMapX_mk_aux

L60 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.awayMapX_mk_aux
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem awayMapX_mk_aux (j : Fin (n + 1))
    {y : MvPolynomial (Fin (n + 1)) A}
    (h : (mvMapGraded R A n) (MvPolynomial.X j) = y) (hy : y ∈ 𝒜A 1)
    (d : ℕ) (p : MvPolynomial (Fin (n + 1)) R) (hp : p ∈ 𝒜R (d • 1)) :
    (h ▸ Away.map (mvMapGraded R A n) (MvPolynomial.X j))
        (Away.mk 𝒜R (X_mem_one R n j) d p hp)
      = Away.mk 𝒜A hy d ((mvMapGraded R A n) p)
          ((mvMapGraded R A n).map_mem hp)
theorem

awayMapX_mk

L72 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.awayMapX_mk
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem awayMapX_mk (j : Fin (n + 1)) (d : ℕ)
    (p : MvPolynomial (Fin (n + 1)) R) (hp : p ∈ 𝒜R (d • 1)) :
    awayMapX R A n j
        (Away.mk 𝒜R (X_mem_one R n j) d p hp)
      = Away.mk 𝒜A (X_mem_one A n j) d
          (MvPolynomial.map (algebraMap R A) p)
          ((mem_homogeneousSubmodule _ _).mpr
            (((mem_homogeneousSubmodule _ _).mp hp).map _))
theorem

C_mem_zero

L83 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.C_mem_zero
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem C_mem_zero {S : Type u} [CommRing S] (r : S) :
    (C r : MvPolynomial (Fin (n + 1)) S)
      ∈ homogeneousSubmodule (Fin (n + 1)) S ((0 : ℕ) • 1)
theorem

algebraMap_eq_mk_zero

L88 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.algebraMap_eq_mk_zero
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem algebraMap_eq_mk_zero {S : Type u} [CommRing S]
    (j : Fin (n + 1)) (r : S) :
    algebraMap S (Away (homogeneousSubmodule (Fin (n + 1)) S) (X j)) r
      = Away.mk _ (X_mem_one S n j) 0 (C r)
          (C_mem_zero n r)
theorem

awayMapX_algebraMap

L98 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.awayMapX_algebraMap
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem awayMapX_algebraMap (j : Fin (n + 1)) :
    (awayMapX R A n j).comp (algebraMap R (Away 𝒜R (X j)))
      = (algebraMap A (Away 𝒜A (X j))).comp (algebraMap R A)
theorem

awayMapX_ratio

L106 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.awayMapX_ratio
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem awayMapX_ratio (j k : Fin (n + 1)) :
    awayMapX R A n j (ratio R n j k)
      = ratio A n j k
theorem

val_aeval_ratio_monomial

L119 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.val_aeval_ratio_monomial
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayChart
variable {S : Type u} [CommRing S] (j : Fin (n + 1))
local notation "𝒜S" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) S
Lean source · full declaration
theorem val_aeval_ratio_monomial (d : {k // k ≠ j} →₀ ℕ) (c : S) :
    (MvPolynomial.aeval (R := S) (fun k : {k // k ≠ j} => ratio S n j k.1)
        (MvPolynomial.monomial d c)).val
      = Localization.mk
          (c • ∏ k ∈ d.support, (X k.1 : MvPolynomial (Fin (n + 1)) S) ^ d k)
          (⟨(X j) ^ (∑ k ∈ d.support, d k), ∑ k ∈ d.support, d k, rfl⟩
            : Submonoid.powers (X j : MvPolynomial (Fin (n + 1)) S)) := by
  have hval : (HomogeneousLocalization.val : Away 𝒜S (X j) → _)
      = (algebraMap (Away 𝒜S (X j)) (Localization.Away (X j))) := rfl
  rw [aeval_monomial, Finsupp.prod, hval, map_mul, map_prod]
  simp only [map_pow, ratio, ← hval, Away.val_mk,
    val_algebraMap, ← Localization.mk_one_eq_algebraMap,
    Localization.mk_pow, Localization.mk_prod, Localization.mk_mul]
  congr 1
  · rw [MvPolynomial.smul_eq_C_mul]
  · refine Subtype.ext ?_
    push_cast
    simp only [Finset.prod_pow_eq_pow_sum, pow_one, one_mul]
theorem

exponent_inj

L138 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.exponent_inj
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayChart
variable {S : Type u} [CommRing S] (j : Fin (n + 1))
local notation "𝒜S" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) S
Lean source · full declaration
theorem exponent_inj (N : ℕ) :
    Function.Injective fun d : {k // k ≠ j} →₀ ℕ =>
      d.mapDomain (Subtype.val : {k // k ≠ j} → Fin (n + 1))
        + Finsupp.single j (N - ∑ k ∈ d.support, d k) := by
  intro d d' h
  refine DFunLike.ext _ _ fun k => ?_
  have := DFunLike.congr_fun h k.1
  simp only [Finsupp.add_apply, Finsupp.single_apply, ite_eq_right (Ne.symm k.2), add_zero,
    Finsupp.mapDomain_apply_of_injective Subtype.val_injective] at this
  exact this
theorem

aeval_ratio_injective

L149 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.aeval_ratio_injective
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayChart
variable {S : Type u} [CommRing S] (j : Fin (n + 1))
local notation "𝒜S" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) S
Lean source · full declaration
theorem aeval_ratio_injective :
    Function.Injective
      (MvPolynomial.aeval (R := S) (fun k : {k // k ≠ j} => ratio S n j k.1)
        : MvPolynomial {k // k ≠ j} S →ₐ[S] Away 𝒜S (X j)) := by
  classical
  rw [injective_iff_map_eq_zero]
  intro p hp
  replace hp := congrArg HomogeneousLocalization.val hp
  rw [HomogeneousLocalization.val_zero, MvPolynomial.as_sum p, map_sum,
    show (HomogeneousLocalization.val : Away 𝒜S (X j) → _)
      = (algebraMap (Away 𝒜S (X j)) (Localization.Away (X j))) from rfl, map_sum] at hp
  simp only [← show (HomogeneousLocalization.val : Away 𝒜S (X j) → _)
      = (algebraMap (Away 𝒜S (X j)) (Localization.Away (X j))) from rfl,
    val_aeval_ratio_monomial] at hp
  set N := (p.support.sup fun d => ∑ k ∈ d.support, d k) with hN
  let ι := algebraMap (MvPolynomial (Fin (n + 1)) S)
    (Localization.Away (X j : MvPolynomial (Fin (n + 1)) S))
  have hXcancel : ∀ q : MvPolynomial (Fin (n + 1)) S, X j * q = 0 → q = 0 := fun q hq =>
    (MvPolynomial.X_mul_cancel_left_iff (i := j)).mp (hq.trans (mul_zero _).symm)
  have hι : Function.Injective ι :=
    IsLocalization.injective (M := Submonoid.powers (X j : MvPolynomial (Fin (n+1)) S))
      _ (Submonoid.powers_le.mpr (mem_nonZeroDivisors_iff.mpr
        ⟨hXcancel, fun q hq => hXcancel q (mul_comm q _ ▸ hq)⟩))
  have hp' := congrArg (· * ι ((X j)^N)) hp
  simp only [zero_mul, Finset.sum_mul] at hp'
  have hterm : ∀ d ∈ p.support,
      Localization.mk (p.coeff d • ∏ k ∈ d.support, (X k.1 : MvPolynomial _ S) ^ d k)
          (⟨(X j)^(∑ k ∈ d.support, d k), _, rfl⟩
            : Submonoid.powers (X j : MvPolynomial _ S))
        * ι ((X j)^N)
      = ι ((p.coeff d • ∏ k ∈ d.support, (X k.1 : MvPolynomial _ S) ^ d k)
          * (X j)^(N - ∑ k ∈ d.support, d k)) := by
    intro d hd
    rw [show (ι ((X j)^N) : Localization.Away (X j : MvPolynomial (Fin (n+1)) S))
        = Localization.mk ((X j)^N) (1 : Submonoid.powers _) from
      (Localization.mk_one_eq_algebraMap _).symm,
      Localization.mk_mul, ← Localization.mk_one_eq_algebraMap,
      Localization.mk_eq_mk_iff, Localization.r_iff_exists]
    refine ⟨1, ?_⟩
    push_cast
    simp only [one_mul, mul_one]
    rw [mul_left_comm, ← pow_add,
      Nat.add_sub_cancel' (Finset.le_sup (f := fun d => ∑ k ∈ d.support, d k) hd)]
  rw [Finset.sum_congr rfl hterm, ← map_sum] at hp'
  replace hp' := hι (hp'.trans (map_zero ι).symm)
  have hform : ∀ d ∈ p.support,
      (p.coeff d • ∏ k ∈ d.support, (X k.1 : MvPolynomial (Fin (n+1)) S) ^ d k)
        * (X j)^(N - ∑ k ∈ d.support, d k)
      = (MvPolynomial.monomial
          (d.mapDomain Subtype.val + Finsupp.single j (N - ∑ k ∈ d.support, d k)))
          (p.coeff d) := by
    intro d _
    rw [MvPolynomial.monomial_eq, Finsupp.prod_add_index (by simp)
        (by intros; exact pow_add _ _ _),
      show ((Finsupp.single j (N - ∑ k ∈ d.support, d k)).prod
            fun i e => (X i : MvPolynomial (Fin (n + 1)) S) ^ e)
          = (X j)^(N - ∑ k ∈ d.support, d k) from
        Finsupp.prod_single_index (pow_zero _),
      Finsupp.prod_mapDomain_index_inj Subtype.val_injective, Finsupp.prod,
      MvPolynomial.smul_eq_C_mul, mul_assoc]
  rw [Finset.sum_congr rfl hform] at hp'
  ext d₀
  by_cases hd₀ : d₀ ∈ p.support
  · have hcoef := congrArg (fun q : MvPolynomial (Fin (n + 1)) S => q.coeff (d₀.mapDomain
      Subtype.val
      + Finsupp.single j (N - ∑ k ∈ d₀.support, d₀ k))) hp'
    simp only [MvPolynomial.coeff_sum, MvPolynomial.coeff_monomial,
      AddMonoidAlgebra.coeff_zero] at hcoef
    rw [Finset.sum_congr rfl (fun d _ => if_congr
      ⟨fun h => exponent_inj n j N h, fun h => h ▸ rfl⟩ rfl rfl),
      Finset.sum_ite_eq' p.support d₀ (fun d => p.coeff d), ite_eq_left hd₀] at hcoef
    exact hcoef.trans (by simp)
  · exact (MvPolynomial.notMem_support_iff.mp hd₀).trans (by simp)
def

awayChartEquiv

L225 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.awayChartEquiv
Documentation

The algebra equivalence identifying the standard chart with a polynomial ring in coordinate ratios.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayChart
variable {S : Type u} [CommRing S] (j : Fin (n + 1))
local notation "𝒜S" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) S
Lean source · statement
def awayChartEquiv :
    MvPolynomial {k // k ≠ j} S ≃ₐ[S] Away 𝒜S (MvPolynomial.X j)
theorem

awayChartEquiv_X

L237 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.awayChartEquiv_X
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayChart
variable {S : Type u} [CommRing S] (j : Fin (n + 1))
local notation "𝒜S" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) S
Lean source · statement
theorem awayChartEquiv_X (k : {k // k ≠ j}) :
    (awayChartEquiv (S := S) n j) (MvPolynomial.X k)
      = ratio S n j k.1
instance

algebra_away_R

L248 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.algebra_away_R
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayBC
variable (j : Fin (n + 1))
Lean source · statement
instance algebra_away_R :
    Algebra R (Away 𝒜A (MvPolynomial.X j))
def

awayMapXₐ

L253 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.awayMapXₐ
Documentation

The coefficient ring algebra homomorphism between the standard localization charts.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayBC
variable (j : Fin (n + 1))
local instance algebra_away_R :
    Algebra R (Away 𝒜A (MvPolynomial.X j)) :=
  ((algebraMap A (Away 𝒜A (X j))).comp (algebraMap R A)).toAlgebra
Lean source · full declaration
def awayMapXₐ :
    Away 𝒜R (MvPolynomial.X j) →ₐ[R] Away 𝒜A (MvPolynomial.X j) where
  toRingHom := awayMapX R A n j
  commutes' r := RingHom.congr_fun (awayMapX_algebraMap R A n j) r
def

incAₐ

L259 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.incAₐ
Documentation

The algebra homomorphism from the extended coefficient ring into its projective chart.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayBC
variable (j : Fin (n + 1))
local instance algebra_away_R :
    Algebra R (Away 𝒜A (MvPolynomial.X j)) :=
  ((algebraMap A (Away 𝒜A (X j))).comp (algebraMap R A)).toAlgebra
Lean source · full declaration
def incAₐ : A →ₐ[R] Away 𝒜A (MvPolynomial.X j) where
  toRingHom := algebraMap A (Away 𝒜A (X j))
  commutes' _ := rfl
def

scalarRTensorAlgEquiv'

L265 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.scalarRTensorAlgEquiv'
Documentation

The algebra equivalence between scalar extension of a polynomial ring and polynomials over the extended coefficients.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayBC
variable (j : Fin (n + 1))
local instance algebra_away_R :
    Algebra R (Away 𝒜A (MvPolynomial.X j)) :=
  ((algebraMap A (Away 𝒜A (X j))).comp (algebraMap R A)).toAlgebra
Lean source · statement
def scalarRTensorAlgEquiv' (σ : Type*) : MvPolynomial σ R ⊗[R] A ≃ₐ[R] MvPolynomial σ A
theorem

scalarRTensor_tmul_one

L269 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.scalarRTensor_tmul_one
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayBC
variable (j : Fin (n + 1))
local instance algebra_away_R :
    Algebra R (Away 𝒜A (MvPolynomial.X j)) :=
  ((algebraMap A (Away 𝒜A (X j))).comp (algebraMap R A)).toAlgebra
Lean source · statement
theorem scalarRTensor_tmul_one {σ : Type*}
    (p : MvPolynomial σ R) :
    scalarRTensorAlgEquiv' R A σ (p ⊗ₜ (1 : A))
      = MvPolynomial.map (algebraMap R A) p
theorem

scalarRTensor_one_tmul

L276 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.scalarRTensor_one_tmul
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayBC
variable (j : Fin (n + 1))
local instance algebra_away_R :
    Algebra R (Away 𝒜A (MvPolynomial.X j)) :=
  ((algebraMap A (Away 𝒜A (X j))).comp (algebraMap R A)).toAlgebra
Lean source · statement
theorem scalarRTensor_one_tmul {σ : Type*} (a : A) :
    scalarRTensorAlgEquiv' R A σ ((1 : MvPolynomial σ R) ⊗ₜ a)
      = MvPolynomial.C a
theorem

awayMapX_chart_compat

L283 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.awayMapX_chart_compat
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayBC
variable (j : Fin (n + 1))
local instance algebra_away_R :
    Algebra R (Away 𝒜A (MvPolynomial.X j)) :=
  ((algebraMap A (Away 𝒜A (X j))).comp (algebraMap R A)).toAlgebra
Lean source · full declaration
theorem awayMapX_chart_compat :
    (awayMapXₐ R A n j).comp
        (awayChartEquiv (S := R) n j).toAlgHom
      = AlgHom.comp
          ({ toRingHom := (awayChartEquiv (S := A) n j).toRingEquiv.toRingHom
             commutes' := fun r => by
               exact (awayChartEquiv (S := A) n j).commutes (algebraMap R A r) }
            : MvPolynomial {k // k ≠ j} A →ₐ[R] Away 𝒜A (X j))
          (MvPolynomial.mapAlgHom (Algebra.ofId R A)) := by
  refine MvPolynomial.algHom_ext fun k => ?_
  simp only [AlgHom.comp_apply, MvPolynomial.mapAlgHom_apply,
    MvPolynomial.map_X, awayMapXₐ, AlgHom.coe_mk]
  erw [awayChartEquiv_X (S := R) n j k]
  rw [awayMapX_ratio]
  exact (awayChartEquiv_X (S := A) n j k).symm
def

awayMvPolyBaseChangeEquiv

L300 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.awayMvPolyBaseChangeEquiv
Documentation

The ring equivalence identifying the scalar extension of a homogeneous localization chart.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayBC
variable (j : Fin (n + 1))
local instance algebra_away_R :
    Algebra R (Away 𝒜A (MvPolynomial.X j)) :=
  ((algebraMap A (Away 𝒜A (X j))).comp (algebraMap R A)).toAlgebra
Lean source · statement
def awayMvPolyBaseChangeEquiv :
    (Away 𝒜R (MvPolynomial.X j)) ⊗[R] A ≃+* Away 𝒜A (MvPolynomial.X j)
theorem

awayMvPolyBaseChangeEquiv_tmul_one

L364 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.awayMvPolyBaseChangeEquiv_tmul_one
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayBC
variable (j : Fin (n + 1))
local instance algebra_away_R :
    Algebra R (Away 𝒜A (MvPolynomial.X j)) :=
  ((algebraMap A (Away 𝒜A (X j))).comp (algebraMap R A)).toAlgebra
Lean source · statement
theorem awayMvPolyBaseChangeEquiv_tmul_one (x : Away 𝒜R (MvPolynomial.X j)) :
    awayMvPolyBaseChangeEquiv R A n j (x ⊗ₜ 1)
      = awayMapX R A n j x
theorem

awayMvPolyBaseChangeEquiv_one_tmul

L370 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.awayMvPolyBaseChangeEquiv_one_tmul
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
section AwayBC
variable (j : Fin (n + 1))
local instance algebra_away_R :
    Algebra R (Away 𝒜A (MvPolynomial.X j)) :=
  ((algebraMap A (Away 𝒜A (X j))).comp (algebraMap R A)).toAlgebra
Lean source · statement
theorem awayMvPolyBaseChangeEquiv_one_tmul (a : A) :
    awayMvPolyBaseChangeEquiv R A n j (1 ⊗ₜ a)
      = algebraMap A (Away 𝒜A (X j)) a
theorem

awayMap_fromZero_compat

L378 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.awayMap_fromZero_compat
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem awayMap_fromZero_compat (s : MvPolynomial (Fin (n + 1)) R) :
    (Away.map (mvMapGraded R A n) s).comp
        ((HomogeneousLocalization.fromZeroRingHom 𝒜R _).comp
          (grad0Equiv R n).toRingHom)
      = ((HomogeneousLocalization.fromZeroRingHom 𝒜A _).comp
          (grad0Equiv A n).toRingHom).comp (algebraMap R A)
theorem

w_chart

L390 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.w_chart
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem w_chart {d : ℕ} (hd : 0 < d)
    (s : MvPolynomial (Fin (n + 1)) R) (hs : s ∈ 𝒜R d) :
    Proj.awayι 𝒜A ((mvMapGraded R A n) s)
        ((mvMapGraded R A n).map_mem hs) hd
      ≫ (Proj.map (mvMapGraded R A n)
          (irrelevant_le_map_mvMapGraded R A n)) ≫ π R n
    = Proj.awayι 𝒜A ((mvMapGraded R A n) s)
        ((mvMapGraded R A n).map_mem hs) hd
      ≫ π A n ≫ Spec.map (CommRingCat.ofHom (algebraMap R A))
theorem

w

L409 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.w
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem w :
    (Proj.map (mvMapGraded R A n)
        (irrelevant_le_map_mvMapGraded R A n)) ≫ π R n
      = π A n ≫ Spec.map (CommRingCat.ofHom (algebraMap R A))
def

chartIso

L420 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.chartIso
Documentation

The isomorphism from the pullback of a standard affine chart to the corresponding chart after coefficient extension.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
def chartIso (j : Fin (n + 1)) :
    (Scheme.Pullback.openCoverOfLeft (affineOpenCover R n).openCover
        (π R n) (Spec.map (CommRingCat.ofHom (algebraMap R A)))).X j
      ≅ Spec (.of (Away 𝒜A (MvPolynomial.X j)))
theorem

projMap_preimage_basicOpen_X

L429 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.projMap_preimage_basicOpen_X
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem projMap_preimage_basicOpen_X (j : Fin (n + 1)) :
    Proj.map (mvMapGraded R A n) (irrelevant_le_map_mvMapGraded R A n)
        ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen _ (X j : MvPolynomial (Fin (n + 1)) R)
      = AlgebraicGeometry.Proj.basicOpen _ (X j : MvPolynomial (Fin (n + 1)) A)
theorem

map_preimage_basicOpen_X'

L436 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.map_preimage_basicOpen_X'
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem map_preimage_basicOpen_X' (j : Fin (n + 1)) :
    map R A n ⁻¹ᵁ AlgebraicGeometry.Proj.basicOpen _ (X j : MvPolynomial (Fin (n + 1)) R)
      = AlgebraicGeometry.Proj.basicOpen _ (X j : MvPolynomial (Fin (n + 1)) A)
theorem

isPullback_map'

L441 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map.AlgebraicGeometry.ProjSpace.isPullback_map'
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
section ProjBaseChange
variable (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (n : ℕ)
local notation "𝒜R" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
local notation "𝒜A" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem isPullback_map' :
    IsPullback (map R A n) (π A n) (π R n)
      (Spec.map (CommRingCat.ofHom (algebraMap R A)))
theorem

isPullback_map

L558 ↗
AlgebraicGeometry.ProjSpace.isPullback_map
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_map
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace MvPolynomial
open HomogeneousLocalization TensorProduct
Lean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.isPullback_map (R A : Type u) [CommRing R] [CommRing A]
    [Algebra R A] (n : ℕ) :
    IsPullback (AlgebraicGeometry.ProjSpace.map R A n) (AlgebraicGeometry.ProjSpace.π A n)
        (AlgebraicGeometry.ProjSpace.π R n)
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R A)))

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