Module

RelEffCartierDiv_isSheaf_functor.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isSheaf_functor

4 declarations indexed from sourceView source ↗

Module documentation

The relative divisor functor is a sheaf.

Imports5

Mathlib.AlgebraicGeometry.Sites.BigZariski
Mathlib.AlgebraicGeometry.Cover.Open
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivFunctor
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_exists_comap_eq_of_openCover
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_eq_of_forall_comap_openCover_eq

Imported by2

def

prodCover

L45 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isSheaf_functor.AlgebraicGeometry.RelEffCartierDiv.SheafProof.prodCover

Documentation

The open cover of the fibre product obtained by pulling back the given base cover.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isSheaf_functor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
namespace SheafProof
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)

Lean source · statement

def prodCover {T : Scheme.{u}} (g : T ⟶ S) (𝒰 : T.OpenCover) (gi : ∀ i, 𝒰.X i ⟶ S)
    (hgi : ∀ i, 𝒰.f i ≫ g = gi i) : (pullback f g).OpenCover

lemma

prodCover_f

L57 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isSheaf_functor.AlgebraicGeometry.RelEffCartierDiv.SheafProof.prodCover_f

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isSheaf_functor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
namespace SheafProof
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)

Lean source · statement

lemma prodCover_f {T : Scheme.{u}} (g : T ⟶ S) (𝒰 : T.OpenCover) (gi : ∀ i, 𝒰.X i
    ⟶ S)
    (hgi : ∀ i, 𝒰.f i ≫ g = gi i) (i : 𝒰.I₀) :
    (prodCover f g 𝒰 gi hgi).f i = mapOnProdOver f (𝒰.f i) (hgi i)

theorem

isSheaf

L63 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isSheaf_functor.AlgebraicGeometry.RelEffCartierDiv.SheafProof.isSheaf

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isSheaf_functor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
namespace SheafProof
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
open _root_.CategoryTheory.Presieve in

Lean source · statement

theorem isSheaf : Presieve.IsSheaf Scheme.zariskiTopology (RelEffCartierDiv.functor f r)

theorem

isSheaf_functor

L246 ↗

AlgebraicGeometry.RelEffCartierDiv.isSheaf_functor

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isSheaf_functor
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.RelEffCartierDiv.isSheaf_functor {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S)
    (r : ℕ) :
    Presieve.IsSheaf Scheme.zariskiTopology (RelEffCartierDiv.functor f r)

Module documentation

Declarations

prodCover

prodCover_f

isSheaf

isSheaf_functor