Module

CoefficientCover.lean

Nyll.SchemeTheory.Gluing.CoefficientCover

3 declarations indexed from sourceView source ↗

Module documentation

Open covers under coefficient pullback

Imports6

Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Mathlib.AlgebraicGeometry.Cover.Open
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Comma.Over.Pullback
Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Imported by4

theorem

overCoefficientPullback_isPullback

L23 ↗

AlgebraicGeometry.Scheme.Cover.overCoefficientPullback_isPullback

Documentation

The actual map produced by coefficient pullback has its canonical cartesian square.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Cover

Lean source · statement

theorem overCoefficientPullback_isPullback
    {B B' : Scheme.{u}} (ψ : B' ⟶ B) {A C : Over B} (m : A ⟶ C) :
    IsPullback ((Over.pullback ψ).map m).left (pullback.fst A.hom ψ)
      (pullback.fst C.hom ψ) m.left

theorem

overCoefficientPullback_map_isPullback

L37 ↗

AlgebraicGeometry.Scheme.Cover.overCoefficientPullback_map_isPullback

Documentation

A cartesian square of schemes over the coefficient base remains cartesian under the actual coefficient-pullback functor.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Cover

Lean source · statement

theorem overCoefficientPullback_map_isPullback
    {B B' : Scheme.{u}} (ψ : B' ⟶ B) {P A C Y : Over B}
    (d : P ⟶ A) (r : P ⟶ C) (a : A ⟶ Y) (c : C ⟶ Y)
    (h : IsPullback d.left r.left a.left c.left) :
    IsPullback ((Over.pullback ψ).map d).left ((Over.pullback ψ).map r).left
      ((Over.pullback ψ).map a).left ((Over.pullback ψ).map c).left

def

overCoefficientPullbackCover

L49 ↗

AlgebraicGeometry.Scheme.Cover.overCoefficientPullbackCover

Documentation

An actual open cover over the coefficient base remains an open cover after pullback, with precisely the objects and maps of Over.pullback.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Cover

Lean source · statement

def overCoefficientPullbackCover
    {B B' : Scheme.{u}} (ψ : B' ⟶ B) {ι : Type u}
    (Y : Over B) (A : ι → Over B) (m : ∀ i : ι, A i ⟶ Y)
    [∀ i : ι, IsOpenImmersion (m i).left]
    (hc : ∀ y : Y.left, ∃ (i : ι) (a : (A i).left), (m i).left a = y) :
    ((Over.pullback ψ).obj Y).left.OpenCover

Module documentation

Open covers under coefficient pullback

Declarations

overCoefficientPullback_isPullback

overCoefficientPullback_map_isPullback

overCoefficientPullbackCover