NYLL
Module

ProjSpace_exists_algHom_away_apply_ratio_eq.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_algHom_away_apply_ratio_eq
6 declarations indexed from sourceView source ↗

Module documentation

Algebra maps from projective affine charts

Imports1
Imported by5

Declarations

def

lift0

L46 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_algHom_away_apply_ratio_eq.AlgebraicGeometry.ProjSpace.ChartLift.lift0
Documentation

Evaluation on the localization where the chosen projective coordinate is invertible.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_algHom_away_apply_ratio_eq
universe u v
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ChartLift
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable (R : Type u) [CommRing R] (n : ℕ) (i : Fin (n + 1))
  {B : Type v} [CommRing B] [Algebra R B] (b : Fin (n + 1) → B) (hb : b i = 1)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
def lift0 : Localization.Away (X i : MvPolynomial (Fin (n + 1)) R) →+* B
theorem

lift0_algebraMap

L51 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_algHom_away_apply_ratio_eq.AlgebraicGeometry.ProjSpace.ChartLift.lift0_algebraMap
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_algHom_away_apply_ratio_eq
universe u v
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ChartLift
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable (R : Type u) [CommRing R] (n : ℕ) (i : Fin (n + 1))
  {B : Type v} [CommRing B] [Algebra R B] (b : Fin (n + 1) → B) (hb : b i = 1)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem lift0_algebraMap (p : MvPolynomial (Fin (n + 1)) R) :
    lift0 R n i b hb (algebraMap _ _ p) = MvPolynomial.aeval b p
def

liftAway

L56 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_algHom_away_apply_ratio_eq.AlgebraicGeometry.ProjSpace.ChartLift.liftAway
Documentation

Evaluation of homogeneous affine-chart coordinates as an algebra homomorphism.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_algHom_away_apply_ratio_eq
universe u v
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ChartLift
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable (R : Type u) [CommRing R] (n : ℕ) (i : Fin (n + 1))
  {B : Type v} [CommRing B] [Algebra R B] (b : Fin (n + 1) → B) (hb : b i = 1)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · full declaration
def liftAway : Away 𝒜 (X i : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B where
  toRingHom := (lift0 R n i b hb).comp (algebraMap (Away 𝒜 (X i : MvPolynomial (Fin (n + 1)) R))
      (Localization.Away (X i : MvPolynomial (Fin (n + 1)) R)))
  commutes' r := by
    change lift0 R n i b hb ((algebraMap R (Away 𝒜 (X i : MvPolynomial (Fin (n + 1)) R)) r).val) =
        algebraMap R B r
    rw [ProjSpace.val_algebraMap, lift0_algebraMap, MvPolynomial.aeval_C]
theorem

liftAway_ratio

L64 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_algHom_away_apply_ratio_eq.AlgebraicGeometry.ProjSpace.ChartLift.liftAway_ratio
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_algHom_away_apply_ratio_eq
universe u v
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ChartLift
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable (R : Type u) [CommRing R] (n : ℕ) (i : Fin (n + 1))
  {B : Type v} [CommRing B] [Algebra R B] (b : Fin (n + 1) → B) (hb : b i = 1)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
Lean source · statement
theorem liftAway_ratio (k : Fin (n + 1)) : liftAway R n i b hb (ProjSpace.ratio R n i k) = b k
theorem

exists_algHom

L72 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_algHom_away_apply_ratio_eq.AlgebraicGeometry.ProjSpace.ChartLift.exists_algHom
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_algHom_away_apply_ratio_eq
universe u v
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProjSpace
open _root_.AlgebraicGeometry.ProjSpace
namespace ChartLift
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
attribute [local instance] MvPolynomial.gradedAlgebra
variable (R : Type u) [CommRing R] (n : ℕ) (i : Fin (n + 1))
  {B : Type v} [CommRing B] [Algebra R B] (b : Fin (n + 1) → B) (hb : b i = 1)
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R
include hb in
Lean source · statement
theorem exists_algHom :
    ∃ φ : Away 𝒜 (X i : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B, ∀ k, φ (ProjSpace.ratio R n i k) = b
        k
theorem

exists_algHom_away_apply_ratio_eq

L81 ↗
AlgebraicGeometry.ProjSpace.exists_algHom_away_apply_ratio_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_algHom_away_apply_ratio_eq
universe u v
open _root_.MvPolynomial
open _root_.HomogeneousLocalization
open _root_.AlgebraicGeometry
section
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.exists_algHom_away_apply_ratio_eq
    (R : Type u) [CommRing R] (n : ℕ) (i : Fin (n + 1))
    {B : Type v} [CommRing B] [Algebra R B] (b : Fin (n + 1) → B) (hb : b i = 1) :
    ∃ φ : HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) R)
        (MvPolynomial.X i : MvPolynomial (Fin (n + 1)) R) →ₐ[R] B,
      ∀ k, φ (ProjSpace.ratio R n i k) = b k

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