NYLL
Module

RepresentableMatching.lean

Nyll.AlgebraicCurves.Geometry.Descent.RepresentableMatching
9 declarations indexed from sourceView source ↗

Module documentation

Points of an effective descent as matching local points

This identifies points of a descended scheme with the compatible elements of the presheaf represented after base change. The presheaf is not assumed to be a sheaf.

Imports2
Imported by3

Declarations

def

Matching

L35 ↗
AlgebraicGeometry.DescentAction.Matching
Documentation

The descent compatibility condition for a local presheaf element.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
Lean source · statement
def Matching (T : Over S)
    (z : G.obj (op ((Over.map s).obj ((Over.pullback s).obj T)))) : Prop
def

localPoint

L46 ↗
AlgebraicGeometry.DescentAction.localPoint
Documentation

The local presheaf element attached to a point of the descended scheme.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
Lean source · statement
def localPoint {T : Over S} (m : T ⟶ Over.mk f) :
    G.obj (op ((Over.map s).obj ((Over.pullback s).obj T)))
theorem

localPoint_eq_map_univBC

L50 ↗
AlgebraicGeometry.DescentAction.localPoint_eq_map_univBC
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
Lean source · statement
theorem localPoint_eq_map_univBC {T : Over S} (m : T ⟶ Over.mk f) :
    localPoint s G x' hX' f e he m =
      G.map ((Over.map s).map ((Over.pullback s).map m)).op
        (univBC s G x' hX' f e he)
theorem

localPoint_injective

L57 ↗
AlgebraicGeometry.DescentAction.localPoint_injective
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
Lean source · statement
theorem localPoint_injective {T : Over S} [Epi (pullback.fst T.hom s)] :
    Function.Injective (localPoint s G x' hX' f e he (T := T))
theorem

localPoint_matching

L75 ↗
AlgebraicGeometry.DescentAction.localPoint_matching
Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
variable (hcompat : eRel s x' f e he ≫ repAct s G x' hX' =
  (canonical s f).act ≫ e.hom)
include hcompat in
Lean source · statement
theorem localPoint_matching {T : Over S} (m : T ⟶ Over.mk f) :
    Matching s G T (localPoint s G x' hX' f e he m)
theorem

matching_flip

L86 ↗
AlgebraicGeometry.DescentAction.matching_flip
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
variable (hcompat : eRel s x' f e he ≫ repAct s G x' hX' =
  (canonical s f).act ≫ e.hom)
Lean source · statement
theorem matching_flip {T : Over S}
    (z : G.obj (op ((Over.map s).obj ((Over.pullback s).obj T))))
    (hz : Matching s G T z) :
    flipMap s T.hom ≫ leftHom s x' (hX'.homEquiv.symm z) =
      nRel s x' (hX'.homEquiv.symm z) ≫ repAct s G x' hX'
theorem

matching_desc_condition

L122 ↗
AlgebraicGeometry.DescentAction.matching_desc_condition
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
variable (hcompat : eRel s x' f e he ≫ repAct s G x' hX' =
  (canonical s f).act ≫ e.hom)
Lean source · statement
theorem matching_desc_condition
    (hcompat : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫ e.hom)
    {T : Over S}
    (z : G.obj (op ((Over.map s).obj ((Over.pullback s).obj T))))
    (hz : Matching s G T z) {W : Scheme.{u}} (g₁ g₂ : W ⟶ pullback T.hom s)
    (hg : g₁ ≫ pullback.fst T.hom s = g₂ ≫ pullback.fst T.hom s) :
    g₁ ≫ (leftHom s x' (hX'.homEquiv.symm z) ≫ e.inv ≫ pullback.fst f s) =
      g₂ ≫ (leftHom s x' (hX'.homEquiv.symm z) ≫ e.inv ≫ pullback.fst f s)
theorem

exists_localPoint_of_matching

L168 ↗
AlgebraicGeometry.DescentAction.exists_localPoint_of_matching
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
variable (hcompat : eRel s x' f e he ≫ repAct s G x' hX' =
  (canonical s f).act ≫ e.hom)
Lean source · statement
theorem exists_localPoint_of_matching
    (hcompat : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫
  e.hom)
    {T : Over S} [EffectiveEpi (pullback.fst T.hom s)]
    (z : G.obj (op ((Over.map s).obj ((Over.pullback s).obj T))))
    (hmatch : Matching s G T z) :
    ∃ m : T ⟶ Over.mk f, localPoint s G x' hX' f e he m = z
def

matchingEquiv

L210 ↗
AlgebraicGeometry.DescentAction.matchingEquiv
Documentation

Effective descent identifies scheme points with matching local presheaf elements.

Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
noncomputable section
namespace AlgebraicGeometry.DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
  (G : (Over S)ᵒᵖ ⥤ Type (u + 1))
variable {X' : Scheme.{u}} (x' : X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
  {X : Scheme.{u}} (f : X ⟶ S) (e : pullback f s ≅ X')
  (he : e.hom ≫ x' = pullback.snd f s)
variable (hcompat : eRel s x' f e he ≫ repAct s G x' hX' =
  (canonical s f).act ≫ e.hom)
Lean source · statement
def matchingEquiv {T : Over S} [EffectiveEpi (pullback.fst T.hom s)] :
    (T ⟶ Over.mk f) ≃
      {z : G.obj (op ((Over.map s).obj ((Over.pullback s).obj T))) // Matching s G T z}

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