Module

OverTotalOpenChart.lean

Nyll.SchemeTheory.LocalGeometry.OverTotalOpenChart

12 declarations indexed from sourceView source ↗

Module documentation

Charts of a total presheaf over an open subscheme

A representable restriction supplies a chart of the total presheaf. Its pointwise factorization and pullback properties make this chart a relative open immersion.

Imports13

Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Restrict
Mathlib.AlgebraicGeometry.Scheme
Mathlib.CategoryTheory.Category.Basic
Mathlib.CategoryTheory.Comma.Over.Basic
Mathlib.CategoryTheory.ConcreteCategory.Basic
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Mathlib.CategoryTheory.MorphismProperty.Representable
Mathlib.CategoryTheory.Types.Basic
Mathlib.CategoryTheory.Yoneda
Nyll.SchemeTheory.CategoryTheory.OverTotalPresheaf
Mathlib.Util.WithWeakNamespace

Imported by2

def

chart

L52 ↗

AlgebraicCurves.Foundations.CategoryTheory.Proofs.CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map.TotRestrict.chart

Documentation

The chart of the total presheaf induced by the object representing the restriction over the open subscheme U.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace
  CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits Opposite AlgebraicGeometry
namespace TotRestrict
variable {S U : Scheme.{u}} (j : U ⟶ S) [IsOpenImmersion j]
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {Y : Scheme.{u}} (p : Y ⟶ U)
  (e : ((Over.map j).op ⋙ G).RepresentableBy (Over.mk p))

Lean source · statement

def chart : uliftYoneda.{u + 1}.obj Y ⟶ G.overTotal

theorem

uliftYonedaEquiv_chart

L56 ↗

AlgebraicCurves.Foundations.CategoryTheory.Proofs.CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map.TotRestrict.uliftYonedaEquiv_chart

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace
  CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits Opposite AlgebraicGeometry
namespace TotRestrict
variable {S U : Scheme.{u}} (j : U ⟶ S) [IsOpenImmersion j]
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {Y : Scheme.{u}} (p : Y ⟶ U)
  (e : ((Over.map j).op ⋙ G).RepresentableBy (Over.mk p))
omit [IsOpenImmersion j] in

Lean source · statement

theorem uliftYonedaEquiv_chart :
    uliftYonedaEquiv (chart j G p e) = ⟨p ≫ j, e.homEquiv (𝟙 (Over.mk p))⟩

theorem

chart_apply

L61 ↗

AlgebraicCurves.Foundations.CategoryTheory.Proofs.CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map.TotRestrict.chart_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace
  CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits Opposite AlgebraicGeometry
namespace TotRestrict
variable {S U : Scheme.{u}} (j : U ⟶ S) [IsOpenImmersion j]
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {Y : Scheme.{u}} (p : Y ⟶ U)
  (e : ((Over.map j).op ⋙ G).RepresentableBy (Over.mk p))
omit [IsOpenImmersion j] in

Lean source · statement

theorem chart_apply {T : Scheme.{u}} (y : T ⟶ Y) :
    uliftYonedaEquiv (uliftYoneda.{u + 1}.map y ≫ chart j G p e) =
      ⟨(y ≫ p) ≫ j, e.homEquiv (Over.homMk y rfl : Over.mk (y ≫ p) ⟶ Over.mk p)⟩

theorem

chart_apply_fst

L74 ↗

AlgebraicCurves.Foundations.CategoryTheory.Proofs.CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map.TotRestrict.chart_apply_fst

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace
  CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits Opposite AlgebraicGeometry
namespace TotRestrict
variable {S U : Scheme.{u}} (j : U ⟶ S) [IsOpenImmersion j]
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {Y : Scheme.{u}} (p : Y ⟶ U)
  (e : ((Over.map j).op ⋙ G).RepresentableBy (Over.mk p))
omit [IsOpenImmersion j] in

Lean source · statement

theorem chart_apply_fst {T : Scheme.{u}} (y : T ⟶ Y) :
    (uliftYonedaEquiv (uliftYoneda.{u + 1}.map y ≫ chart j G p e)).1 = (y ≫ p) ≫ j

theorem

toFibre_chart_apply

L79 ↗

AlgebraicCurves.Foundations.CategoryTheory.Proofs.CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map.TotRestrict.toFibre_chart_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace
  CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits Opposite AlgebraicGeometry
namespace TotRestrict
variable {S U : Scheme.{u}} (j : U ⟶ S) [IsOpenImmersion j]
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {Y : Scheme.{u}} (p : Y ⟶ U)
  (e : ((Over.map j).op ⋙ G).RepresentableBy (Over.mk p))
omit [IsOpenImmersion j] in

Lean source · statement

theorem toFibre_chart_apply {T : Scheme.{u}} (y : T ⟶ Y)
    (h : (uliftYonedaEquiv (uliftYoneda.{u + 1}.map y ≫ chart j G p e)).1 =
      (Over.mk ((y ≫ p) ≫ j)).hom) :
    Functor.OverTotal.toFibre (Over.mk ((y ≫ p) ≫ j))
      (uliftYonedaEquiv (uliftYoneda.{u + 1}.map y ≫ chart j G p e)) h =
      e.homEquiv (Over.homMk y rfl : Over.mk (y ≫ p) ⟶ Over.mk p)

theorem

eq_of_chart_eq

L89 ↗

AlgebraicCurves.Foundations.CategoryTheory.Proofs.CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map.TotRestrict.eq_of_chart_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace
  CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits Opposite AlgebraicGeometry
namespace TotRestrict
variable {S U : Scheme.{u}} (j : U ⟶ S) [IsOpenImmersion j]
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {Y : Scheme.{u}} (p : Y ⟶ U)
  (e : ((Over.map j).op ⋙ G).RepresentableBy (Over.mk p))

Lean source · statement

theorem eq_of_chart_eq {T : Scheme.{u}} (y y' : T ⟶ Y)
    (h : uliftYonedaEquiv (uliftYoneda.{u + 1}.map y ≫ chart j G p e) =
      uliftYonedaEquiv (uliftYoneda.{u + 1}.map y' ≫ chart j G p e)) : y = y'

theorem

chart_apply_over

L116 ↗

AlgebraicCurves.Foundations.CategoryTheory.Proofs.CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map.TotRestrict.chart_apply_over

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace
  CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits Opposite AlgebraicGeometry
namespace TotRestrict
variable {S U : Scheme.{u}} (j : U ⟶ S) [IsOpenImmersion j]
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {Y : Scheme.{u}} (p : Y ⟶ U)
  (e : ((Over.map j).op ⋙ G).RepresentableBy (Over.mk p))
omit [IsOpenImmersion j] in

Lean source · statement

theorem chart_apply_over {X : Over U} (k : X ⟶ Over.mk p) :
    uliftYonedaEquiv (uliftYoneda.{u + 1}.map k.left ≫ chart j G p e) =
      Functor.OverTotal.ofFibre ((Over.map j).obj X) (e.homEquiv k)

theorem

app_eq

L135 ↗

AlgebraicCurves.Foundations.CategoryTheory.Proofs.CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map.TotRestrict.app_eq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace
  CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits Opposite AlgebraicGeometry
namespace TotRestrict
variable {S U : Scheme.{u}} (j : U ⟶ S) [IsOpenImmersion j]
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {Y : Scheme.{u}} (p : Y ⟶ U)
  (e : ((Over.map j).op ⋙ G).RepresentableBy (Over.mk p))
omit [IsOpenImmersion j] in

Lean source · statement

theorem app_eq {X : Scheme.{u}} {F : Scheme.{u}ᵒᵖ ⥤ Type (u + 1)}
    (τ : uliftYoneda.{u + 1}.obj X ⟶ F)
    (Z : Scheme.{u}ᵒᵖ) (a : (uliftYoneda.{u + 1}.obj X).obj Z) :
    τ.app Z a = uliftYonedaEquiv (uliftYoneda.{u + 1}.map a.down ≫ τ)

theorem

exists_fac

L144 ↗

AlgebraicCurves.Foundations.CategoryTheory.Proofs.CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map.TotRestrict.exists_fac

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace
  CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits Opposite AlgebraicGeometry
namespace TotRestrict
variable {S U : Scheme.{u}} (j : U ⟶ S) [IsOpenImmersion j]
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {Y : Scheme.{u}} (p : Y ⟶ U)
  (e : ((Over.map j).op ⋙ G).RepresentableBy (Over.mk p))

Lean source · statement

theorem exists_fac {T : Scheme.{u}} (x : uliftYoneda.{u + 1}.obj T ⟶ G.overTotal)
    (hx : Set.range ((uliftYonedaEquiv x).1).base ⊆ Set.range j.base) :
    ∃ ψ : T ⟶ Y, uliftYoneda.{u + 1}.map ψ ≫ chart j G p e = x

theorem

isPullback

L162 ↗

AlgebraicCurves.Foundations.CategoryTheory.Proofs.CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map.TotRestrict.isPullback

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace
  CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits Opposite AlgebraicGeometry
namespace TotRestrict
variable {S U : Scheme.{u}} (j : U ⟶ S) [IsOpenImmersion j]
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {Y : Scheme.{u}} (p : Y ⟶ U)
  (e : ((Over.map j).op ⋙ G).RepresentableBy (Over.mk p))

Lean source · statement

theorem isPullback {T : Scheme.{u}} (g : uliftYoneda.{u + 1}.obj T ⟶ G.overTotal) :
    ∃ (ψ : ((((uliftYonedaEquiv g).1) ⁻¹ᵁ (Scheme.Hom.opensRange j) : T.Opens) : Scheme.{u}) ⟶ Y),
      IsPullback (uliftYoneda.{u + 1}.map ψ)
        (uliftYoneda.{u + 1}.map (((uliftYonedaEquiv g).1) ⁻¹ᵁ (Scheme.Hom.opensRange j)).ι)
        (chart j G p e) g

theorem

main

L245 ↗

AlgebraicCurves.Foundations.CategoryTheory.Proofs.CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map.TotRestrict.main

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace
  CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits Opposite AlgebraicGeometry
namespace TotRestrict
variable {S U : Scheme.{u}} (j : U ⟶ S) [IsOpenImmersion j]
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {Y : Scheme.{u}} (p : Y ⟶ U)
  (e : ((Over.map j).op ⋙ G).RepresentableBy (Over.mk p))

Lean source · statement

theorem main :
    ∃ φ : uliftYoneda.{u + 1}.obj Y ⟶ G.overTotal,
      (∀ {T : Scheme.{u}} (y : T ⟶ Y),
        uliftYonedaEquiv (uliftYoneda.{u + 1}.map y ≫ φ) =
          ⟨(y ≫ p) ≫ j, e.homEquiv (Over.homMk y rfl : Over.mk (y ≫ p) ⟶ Over.mk p)⟩) ∧
      MorphismProperty.relative uliftYoneda.{u + 1} @IsOpenImmersion φ ∧
      ∀ {T : Scheme.{u}} (x : uliftYoneda.{u + 1}.obj T ⟶ G.overTotal),
        Set.range ((uliftYonedaEquiv x).1).base ⊆ Set.range j.base →
        ∃ ψ : T ⟶ Y, uliftYoneda.{u + 1}.map ψ ≫ φ = x

theorem

exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map

L266 ↗

CategoryTheory.Functor.exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CategoryTheory.Proofs
namespace
  CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits Opposite AlgebraicGeometry
open
  CategoryTheory_Functor_exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
in
with_weak_namespace _root_.CategoryTheory.Functor

Lean source · statement

theorem exists_overTotal_chart_relative_isOpenImmersion_of_representableBy_over_map
    {S U : Scheme.{u}} (j : U ⟶ S) [IsOpenImmersion j]
    (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
    {Y : Scheme.{u}} (p : Y ⟶ U) (e : ((Over.map j).op ⋙ G).RepresentableBy (Over.mk p)) :
    ∃ φ : uliftYoneda.{u + 1}.obj Y ⟶ G.overTotal,
      (∀ {T : Scheme.{u}} (y : T ⟶ Y),
        uliftYonedaEquiv (uliftYoneda.{u + 1}.map y ≫ φ) =
          ⟨(y ≫ p) ≫ j, e.homEquiv (Over.homMk y rfl : Over.mk (y ≫ p) ⟶ Over.mk p)⟩) ∧
      MorphismProperty.relative uliftYoneda.{u + 1} @IsOpenImmersion φ ∧
      ∀ {T : Scheme.{u}} (x : uliftYoneda.{u + 1}.obj T ⟶ G.overTotal),
        Set.range ((uliftYonedaEquiv x).1).base ⊆ Set.range j.base →
        ∃ ψ : T ⟶ Y, uliftYoneda.{u + 1}.map ψ ≫ φ = x

Module documentation

Charts of a total presheaf over an open subscheme

Declarations