NYLL
Module

prodKerGraph_comap_mapOnProdOver.lean

Nyll.AlgebraicCurves.Geometry.Schemes.prodKerGraph_comap_mapOnProdOver
4 declarations indexed from sourceView source ↗

Module documentation

Base change of products of graph ideals

The ideal kernels of graphs commute with base change, as do their finite products.

Imports4
Imported by10

Declarations

theorem

ker_graphOver_comap

L42 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.prodKerGraph_comap_mapOnProdOver.AlgebraicGeometry.ProdKerGraphNaturality.ker_graphOver_comap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.prodKerGraph_comap_mapOnProdOver
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProdKerGraphNaturality
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] {T T' : Scheme.{u}} {g : T ⟶ S}
  {g' : T' ⟶ S}
Lean source · full declaration
theorem ker_graphOver_comap (a : T' ⟶ 𝒞) (ha : a ≫ f = g') (φ : T ⟶ T') (hφ : φ ≫ g' = g) :
    (graphOver f a ha).ker.comap (mapOnProdOver f φ hφ) =
      (graphOver f (φ ≫ a) (by rw [Category.assoc, ha, hφ])).ker :=
  congrArg RelEffCartierDiv.I (RelEffCartierDiv.pullbackAlong_ofPoint f a ha φ hφ)
theorem

comap_finsetProd

L47 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.prodKerGraph_comap_mapOnProdOver.AlgebraicGeometry.ProdKerGraphNaturality.comap_finsetProd
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.prodKerGraph_comap_mapOnProdOver
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProdKerGraphNaturality
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] {T T' : Scheme.{u}} {g : T ⟶ S}
  {g' : T' ⟶ S}
omit [IsSeparated f] in
Lean source · statement
theorem comap_finsetProd {ι : Type*} (s : Finset ι)
    (I : ι → (pullback f g').IdealSheafData) (φ : T ⟶ T') (hφ : φ ≫ g' = g) :
    (∏ i ∈ s, I i).comap (mapOnProdOver f φ hφ) = ∏ i ∈ s, (I i).comap (mapOnProdOver f φ hφ)
theorem

prodKerGraph_comap

L56 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.prodKerGraph_comap_mapOnProdOver.AlgebraicGeometry.ProdKerGraphNaturality.prodKerGraph_comap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.prodKerGraph_comap_mapOnProdOver
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace ProdKerGraphNaturality
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] {T T' : Scheme.{u}} {g : T ⟶ S}
  {g' : T' ⟶ S}
Lean source · full declaration
theorem prodKerGraph_comap {r : ℕ} (a : Fin r → (T' ⟶ 𝒞)) (ha : ∀ i, a i ≫ f = g')
    (φ : T ⟶ T') (hφ : φ ≫ g' = g) :
    (prodKerGraph f a ha).comap (mapOnProdOver f φ hφ) =
      prodKerGraph f (fun i => φ ≫ a i) (fun i => by rw [Category.assoc, ha, hφ]) := by
  simp only [prodKerGraph_eq_prod, comap_finsetProd, ker_graphOver_comap]
theorem

prodKerGraph_comap_mapOnProdOver

L64 ↗
AlgebraicGeometry.prodKerGraph_comap_mapOnProdOver
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.prodKerGraph_comap_mapOnProdOver
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
Lean source · full declaration
theorem _root_.AlgebraicGeometry.prodKerGraph_comap_mapOnProdOver
    {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] {r : ℕ} {T T' : Scheme.{u}} {g : T ⟶ S}
    {g' : T' ⟶ S} (a : Fin r → (T' ⟶ 𝒞)) (ha : ∀ i, a i ≫ f = g') (φ : T ⟶ T')
    (hφ : φ ≫ g' = g) :
    (prodKerGraph f a ha).comap (mapOnProdOver f φ hφ) =
      prodKerGraph f (fun i => φ ≫ a i) (fun i => by rw [Category.assoc, ha, hφ]) :=
  AlgebraicGeometry.ProdKerGraphNaturality.prodKerGraph_comap a ha φ hφ

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