NYLL
Module

ProjSpace_isPullback_comp_and_comp_eq_map_of_isScalarTower.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_isPullback_comp_and_comp_eq_map_of_isScalarTower
5 declarations indexed from sourceView source ↗

Module documentation

Proj Space is Pullback comp and comp eq map of is Scalar Tower

Imports5
Imported by1

Declarations

theorem

projMap_congr

L36 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_comp_and_comp_eq_map_of_isScalarTower.P2mK4G.projMap_congr
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_isPullback_comp_and_comp_eq_map_of_isScalarTower
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mK4G
Lean source · statement
theorem projMap_congr {A C : Type u} [CommRing A] [CommRing C] {n : ℕ}
    (φ ψ : MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A →+*ᵍ MvPolynomial.homogeneousSubmodule
      (Fin (n + 1)) C)
    (hφ : HomogeneousIdeal.irrelevant (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) C) ≤
      (HomogeneousIdeal.irrelevant (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)).map φ)
    (hψ : HomogeneousIdeal.irrelevant (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) C) ≤
      (HomogeneousIdeal.irrelevant (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)).map ψ) (h :
        φ = ψ) :
    Proj.map φ hφ = Proj.map ψ hψ
theorem

mvMapGraded_comp

L47 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_comp_and_comp_eq_map_of_isScalarTower.P2mK4G.mvMapGraded_comp
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_isPullback_comp_and_comp_eq_map_of_isScalarTower
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mK4G
Lean source · statement
theorem mvMapGraded_comp (A B C : Type u) [CommRing A] [CommRing B] [CommRing C]
    [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (n : ℕ) :
    (ProjSpace.mvMapGraded B C n).comp (ProjSpace.mvMapGraded A B n) = ProjSpace.mvMapGraded A C n
theorem

map_comp_map

L56 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_comp_and_comp_eq_map_of_isScalarTower.P2mK4G.map_comp_map
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_isPullback_comp_and_comp_eq_map_of_isScalarTower
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mK4G
Lean source · statement
theorem map_comp_map (A B C : Type u) [CommRing A] [CommRing B] [CommRing C]
    [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] (n : ℕ) :
    ProjSpace.map B C n ≫ ProjSpace.map A B n = ProjSpace.map A C n
theorem

specMap_comp

L62 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_isPullback_comp_and_comp_eq_map_of_isScalarTower.P2mK4G.specMap_comp
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_isPullback_comp_and_comp_eq_map_of_isScalarTower
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace P2mK4G
Lean source · statement
theorem specMap_comp (A B C : Type u) [CommRing A] [CommRing B] [CommRing C]
    [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] :
    Spec.map (CommRingCat.ofHom (algebraMap B C)) ≫ Spec.map (CommRingCat.ofHom (algebraMap A B)) =
      Spec.map (CommRingCat.ofHom (algebraMap A C))
theorem

isPullback_comp_and_comp_eq_map_of_isScalarTower

L70 ↗
AlgebraicGeometry.ProjSpace.isPullback_comp_and_comp_eq_map_of_isScalarTower
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_isPullback_comp_and_comp_eq_map_of_isScalarTower
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.isPullback_comp_and_comp_eq_map_of_isScalarTower
    {A : Type u} [CommRing A] (B C : Type u) [CommRing B] [CommRing C]
    [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] {n : ℕ}
    {Z ZB ZC : Scheme.{u}}
    (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)) (ιB : ZB ⟶ Proj
      (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) B)) (ιC : ZC ⟶ Proj
      (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) C))
    (e : ZB ⟶ Z) (f : ZC ⟶ ZB)
    (hpb : IsPullback e (ιB ≫ ProjSpace.π B n) (ι ≫ ProjSpace.π A n) (Spec.map (CommRingCat.ofHom
      (algebraMap A B))))
    (hcomp : e ≫ ι = ιB ≫ ProjSpace.map A B n)
    (hpb' : IsPullback f (ιC ≫ ProjSpace.π C n) (ιB ≫ ProjSpace.π B n) (Spec.map (CommRingCat.ofHom
      (algebraMap B C))))
    (hcomp' : f ≫ ιB = ιC ≫ ProjSpace.map B C n) :
    IsPullback (f ≫ e) (ιC ≫ ProjSpace.π C n) (ι ≫ ProjSpace.π A n) (Spec.map (CommRingCat.ofHom
      (algebraMap A C))) ∧
    (f ≫ e) ≫ ι = ιC ≫ ProjSpace.map A C n

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