NYLL
Module

DescentAction.lean

Nyll.AlgebraicCurves.Geometry.Descent.DescentAction
65 declarations indexed from sourceView source ↗

Module documentation

Descent Action

Imports17
  • Mathlib.AlgebraicGeometry.Pullbacks
  • Mathlib.AlgebraicGeometry.Scheme
  • Mathlib.CategoryTheory.Category.Basic
  • Mathlib.CategoryTheory.Comma.Over.Basic
  • Mathlib.CategoryTheory.Comma.Over.Pullback
  • Mathlib.CategoryTheory.EffectiveEpi.Basic
  • Mathlib.CategoryTheory.Functor.Basic
  • Mathlib.CategoryTheory.Iso
  • Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
  • Mathlib.CategoryTheory.Opposites
  • Mathlib.CategoryTheory.Sites.IsSheafFor
  • Mathlib.CategoryTheory.Sites.Sieves.Presieve
  • Mathlib.CategoryTheory.Types.Basic
  • Mathlib.CategoryTheory.Yoneda
  • Mathlib.Logic.Equiv.Defs
  • Mathlib.Tactic.CategoryTheory.Reassoc
  • Mathlib.Tactic.Set
Imported by10

Declarations

def

unitMap

L46 ↗
AlgebraicGeometry.DescentAction.unitMap
Documentation

The unit morphism into the pullback used to express the unit law for descent.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
Lean source · statement
def unitMap : X' ⟶ pullback (x' ≫ s) s
def

proj₁₃

L50 ↗
AlgebraicGeometry.DescentAction.proj₁₃
Documentation

Projection from the iterated pullback to its first and third factors.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
Lean source · statement
def proj₁₃ :
    pullback (pullback.snd (x' ≫ s) s ≫ s) s ⟶ pullback (x' ≫ s) s
theorem

unitMap_fst

L55 ↗
AlgebraicGeometry.DescentAction.unitMap_fst
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
Lean source · statement
theorem unitMap_fst : unitMap s x' ≫ pullback.fst _ _ = 𝟙 X'
theorem

unitMap_snd

L57 ↗
AlgebraicGeometry.DescentAction.unitMap_snd
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
Lean source · statement
theorem unitMap_snd : unitMap s x' ≫ pullback.snd _ _ = x'
theorem

proj₁₃_fst

L59 ↗
AlgebraicGeometry.DescentAction.proj₁₃_fst
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
Lean source · statement
theorem proj₁₃_fst :
    proj₁₃ s x' ≫ pullback.fst _ _ = pullback.fst _ _ ≫ pullback.fst _ _
theorem

proj₁₃_snd

L61 ↗
AlgebraicGeometry.DescentAction.proj₁₃_snd
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
Lean source · statement
theorem proj₁₃_snd : proj₁₃ s x' ≫ pullback.snd _ _ = pullback.snd _ _
def

toTriple

L65 ↗
AlgebraicGeometry.DescentAction.toTriple
Documentation

The morphism into the iterated pullback obtained from the original structure map.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
Lean source · statement
def toTriple : pullback (x' ≫ s) s ⟶ pullback (pullback.snd (x' ≫ s) s ≫ s) s
theorem

toTriple_fst

L69 ↗
AlgebraicGeometry.DescentAction.toTriple_fst
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
Lean source · statement
theorem toTriple_fst : toTriple s x' ≫ pullback.fst _ _ = 𝟙 _
theorem

toTriple_snd

L71 ↗
AlgebraicGeometry.DescentAction.toTriple_snd
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
Lean source · statement
theorem toTriple_snd : toTriple s x' ≫ pullback.snd _ _ = pullback.fst _
  _ ≫ x'
theorem

toTriple_proj₁₃

L75 ↗
AlgebraicGeometry.DescentAction.toTriple_proj₁₃
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
Lean source · statement
theorem toTriple_proj₁₃ : toTriple s x' ≫ proj₁₃ s x' = pullback.fst _ _ ≫ unitMap s x'
def

actMap

L83 ↗
AlgebraicGeometry.DescentAction.actMap
Documentation

The morphism on the iterated pullback obtained by applying the candidate descent action.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
variable {s x'} in
Lean source · statement
def actMap (act : pullback (x' ≫ s) s ⟶ X') (h : act ≫ x' = pullback.snd _ _) :
    pullback (pullback.snd (x' ≫ s) s ≫ s) s ⟶ pullback (x' ≫ s) s
theorem

actMap_fst

L89 ↗
AlgebraicGeometry.DescentAction.actMap_fst
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
variable {s x'} in
variable {s x'} in
Lean source · statement
theorem actMap_fst (act : pullback (x' ≫ s) s ⟶ X') (h : act ≫ x' =
  pullback.snd _ _) :
    actMap act h ≫ pullback.fst _ _ = pullback.fst _ _ ≫ act
theorem

actMap_snd

L93 ↗
AlgebraicGeometry.DescentAction.actMap_snd
Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
variable {s x'} in
variable {s x'} in
variable {s x'} in
Lean source · statement
theorem actMap_snd (act : pullback (x' ≫ s) s ⟶ X') (h : act ≫ x' =
  pullback.snd _ _) :
    actMap act h ≫ pullback.snd _ _ = pullback.snd _ _
def

flipMap

L98 ↗
AlgebraicGeometry.DescentAction.flipMap
Documentation

The pullback projection that defines the canonical action on a base-changed scheme.

Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
variable {s x'} in
variable {s x'} in
variable {s x'} in
Lean source · statement
def flipMap {X : Scheme.{u}} (f : X ⟶ S) :
    pullback (pullback.snd f s ≫ s) s ⟶ pullback f s
theorem

flipMap_fst

L103 ↗
AlgebraicGeometry.DescentAction.flipMap_fst
Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
variable {s x'} in
variable {s x'} in
variable {s x'} in
Lean source · statement
theorem flipMap_fst {X : Scheme.{u}} (f : X ⟶ S) :
    flipMap s f ≫ pullback.fst f s = pullback.fst _ _ ≫ pullback.fst f s
theorem

flipMap_snd

L105 ↗
AlgebraicGeometry.DescentAction.flipMap_snd
Source context 8 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S')
variable {s x'} in
variable {s x'} in
variable {s x'} in
Lean source · statement
theorem flipMap_snd {X : Scheme.{u}} (f : X ⟶ S) :
    flipMap s f ≫ pullback.snd f s = pullback.snd _ _
structure

DescentAction

L111 ↗
AlgebraicGeometry.DescentAction
Documentation

An action of the base-change relation satisfying the unit and composition laws for descent.

Source context 3 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
Lean source · full declaration
structure DescentAction {S S' : Scheme.{u}} (s : S' ⟶ S) {X' : Scheme.{u}} (x' : X' ⟶ S') where
  /-- The action morphism on the pullback along the covering map. -/
  act : pullback (x' ≫ s) s ⟶ X'
  /-- The action lies over the second projection to the covering scheme. -/
  act_comp : act ≫ x' = pullback.snd _ _
  /-- Acting along the unit map is the identity. -/
  unit_act : DescentAction.unitMap s x' ≫ act = 𝟙 X'
  /-- The two successive actions agree with the direct action. -/
  trans : DescentAction.actMap act act_comp ≫ act = DescentAction.proj₁₃ s x' ≫ act
def

canonical

L126 ↗
AlgebraicGeometry.DescentAction.canonical
Documentation

The canonical descent action on a scheme obtained by base change.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
Lean source · full declaration
def canonical {X : Scheme.{u}} (f : X ⟶ S) : DescentAction s (pullback.snd f s) where
  act := flipMap s f
  act_comp := flipMap_snd s f
  unit_act := by
    apply pullback.hom_ext
    · rw [Category.assoc, flipMap_fst, unitMap_fst_assoc, Category.id_comp]
    · rw [Category.assoc, flipMap_snd, unitMap_snd, Category.id_comp]
  trans := by
    apply pullback.hom_ext
    · rw [Category.assoc, flipMap_fst, actMap_fst_assoc, flipMap_fst, Category.assoc, flipMap_fst,
        proj₁₃_fst_assoc]
    · rw [Category.assoc, flipMap_snd, actMap_snd, Category.assoc, flipMap_snd, proj₁₃_snd]
def

Effective

L141 ↗
AlgebraicGeometry.DescentAction.Effective
Documentation

The condition that the descent action comes from a scheme over the original base.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} (s : S' ⟶ S)
variable {s} in
Lean source · statement
def Effective {X' : Scheme.{u}} {x' : X' ⟶ S'} (A : DescentAction s x') : Prop
def

invol

L155 ↗
AlgebraicGeometry.DescentAction.invol
Documentation

The involution on the relation pullback induced by the descent action.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} {s : S' ⟶ S} {X' : Scheme.{u}} {x' : X' ⟶ S'} (A : DescentAction s x')
Lean source · statement
def invol : pullback (x' ≫ s) s ⟶ pullback (x' ≫ s) s
theorem

invol_fst

L159 ↗
AlgebraicGeometry.DescentAction.invol_fst
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} {s : S' ⟶ S} {X' : Scheme.{u}} {x' : X' ⟶ S'} (A : DescentAction s x')
Lean source · statement
theorem invol_fst : A.invol ≫ pullback.fst _ _ = A.act
theorem

invol_snd

L161 ↗
AlgebraicGeometry.DescentAction.invol_snd
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} {s : S' ⟶ S} {X' : Scheme.{u}} {x' : X' ⟶ S'} (A : DescentAction s x')
Lean source · statement
theorem invol_snd : A.invol ≫ pullback.snd _ _ = pullback.fst _ _ ≫ x'
theorem

toTriple_actMap

L164 ↗
AlgebraicGeometry.DescentAction.toTriple_actMap
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} {s : S' ⟶ S} {X' : Scheme.{u}} {x' : X' ⟶ S'} (A : DescentAction s x')
Lean source · statement
theorem toTriple_actMap : toTriple s x' ≫ actMap A.act A.act_comp = A.invol
theorem

invol_act

L169 ↗
AlgebraicGeometry.DescentAction.invol_act
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} {s : S' ⟶ S} {X' : Scheme.{u}} {x' : X' ⟶ S'} (A : DescentAction s x')
Lean source · statement
theorem invol_act : A.invol ≫ A.act = pullback.fst _ _
theorem

invol_invol

L174 ↗
AlgebraicGeometry.DescentAction.invol_invol
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} {s : S' ⟶ S} {X' : Scheme.{u}} {x' : X' ⟶ S'} (A : DescentAction s x')
Lean source · statement
theorem invol_invol : A.invol ≫ A.invol = 𝟙 _
def

involIso

L180 ↗
AlgebraicGeometry.DescentAction.involIso
Documentation

The isomorphism associated with the involution of the descent relation.

Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} {s : S' ⟶ S} {X' : Scheme.{u}} {x' : X' ⟶ S'} (A : DescentAction s x')
Lean source · statement
def involIso : pullback (x' ≫ s) s ≅ pullback (x' ≫ s) s
theorem

act_eq_invol_fst

L183 ↗
AlgebraicGeometry.DescentAction.act_eq_invol_fst
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} {s : S' ⟶ S} {X' : Scheme.{u}} {x' : X' ⟶ S'} (A : DescentAction s x')
Lean source · statement
theorem act_eq_invol_fst : A.act = A.involIso.hom ≫ pullback.fst _ _
theorem

hom_ext

L185 ↗
AlgebraicGeometry.DescentAction.hom_ext
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} {s : S' ⟶ S} {X' : Scheme.{u}} {x' : X' ⟶ S'} (A : DescentAction s x')
Lean source · statement
theorem hom_ext {T : Scheme.{u}} {a b : T ⟶ pullback (x' ≫ s) s} (h₁ : a ≫ pullback.fst _ _ = b ≫
  pullback.fst _ _)
    (h₂ : a ≫ A.act = b ≫ A.act) : a = b
theorem

equivalence

L191 ↗
AlgebraicGeometry.DescentAction.equivalence
Source context 5 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
variable {S S' : Scheme.{u}} {s : S' ⟶ S} {X' : Scheme.{u}} {x' : X' ⟶ S'} (A : DescentAction s x')
Lean source · full declaration
theorem equivalence (T : Scheme.{u}) :
    _root_.Equivalence fun x y : T ⟶ X' => ∃ φ : T ⟶ pullback (x' ≫ s) s, φ ≫ pullback.fst _ _ = x
      ∧ φ ≫ A.act = y where
  refl x := ⟨x ≫ unitMap s x', by rw [Category.assoc, unitMap_fst, Category.comp_id],
    by rw [Category.assoc, A.unit_act, Category.comp_id]⟩
  symm := by
    rintro x y ⟨φ, hφ, hφ'⟩
    exact ⟨φ ≫ A.invol,
      by rw [Category.assoc, invol_fst, hφ'], by rw [Category.assoc, invol_act, hφ]⟩
  trans := by
    rintro x y z ⟨φ, hφ, hφ'⟩ ⟨ψ, hψ, hψ'⟩
    have w : φ ≫ pullback.snd (x' ≫ s) s ≫ s = (ψ ≫ pullback.snd (x' ≫ s) s) ≫ s := by
      rw [Category.assoc, ← pullback.condition, reassoc_of% hψ, ← reassoc_of% hφ', reassoc_of%
        A.act_comp,
        pullback.condition]
    let k : T ⟶ pullback (pullback.snd (x' ≫ s) s ≫ s) s := pullback.lift φ (ψ ≫ pullback.snd _ _) w
    have hk₁ : k ≫ actMap A.act A.act_comp = ψ := by
      apply pullback.hom_ext
      · rw [Category.assoc, actMap_fst, pullback.lift_fst_assoc, hφ', hψ]
      · rw [Category.assoc, actMap_snd, pullback.lift_snd]
    refine ⟨k ≫ proj₁₃ s x', by rw [Category.assoc, proj₁₃_fst, pullback.lift_fst_assoc, hφ], ?_⟩
    rw [Category.assoc, ← A.trans, ← Category.assoc, hk₁, hψ']
def

fstOver

L225 ↗
AlgebraicGeometry.DescentAction.fstOver
Documentation

The first projection of the relation pullback as a morphism over the original base.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section repAct
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {X' : Scheme.{u}} (x' :
  X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
Lean source · statement
def fstOver : (Over.map s).obj (Over.mk (pullback.snd (x' ≫ s) s)) ⟶ (Over.map s).obj
  (Over.mk x')
def

univ

L230 ↗
AlgebraicGeometry.DescentAction.univ
Documentation

The universal element corresponding to the identity of the representing object.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section repAct
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {X' : Scheme.{u}} (x' :
  X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
Lean source · statement
def univ : G.obj (op ((Over.map s).obj (Over.mk x')))
def

repActOver

L233 ↗
AlgebraicGeometry.DescentAction.repActOver
Documentation

The morphism over the new base represented by pullback of the universal element.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section repAct
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {X' : Scheme.{u}} (x' :
  X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
Lean source · statement
def repActOver : Over.mk (pullback.snd (x' ≫ s) s) ⟶ Over.mk x'
def

repAct

L237 ↗
AlgebraicGeometry.DescentAction.repAct
Documentation

The underlying scheme morphism of the represented descent action.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section repAct
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {X' : Scheme.{u}} (x' :
  X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
Lean source · statement
def repAct : pullback (x' ≫ s) s ⟶ X'
theorem

repAct_comp

L239 ↗
AlgebraicGeometry.DescentAction.repAct_comp
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section repAct
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {X' : Scheme.{u}} (x' :
  X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
Lean source · statement
theorem repAct_comp : repAct s G x' hX' ≫ x' = pullback.snd _ _
theorem

map_repActOver_univ

L241 ↗
AlgebraicGeometry.DescentAction.map_repActOver_univ
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section repAct
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {X' : Scheme.{u}} (x' :
  X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
Lean source · statement
theorem map_repActOver_univ :
    G.map ((Over.map s).map (repActOver s G x' hX')).op (univ s G x' hX') =
      G.map (fstOver s x').op (univ s G x' hX')
theorem

homEquiv_eq_map_univ

L250 ↗
AlgebraicGeometry.DescentAction.homEquiv_eq_map_univ
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section repAct
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {X' : Scheme.{u}} (x' :
  X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
Lean source · statement
theorem homEquiv_eq_map_univ {U : Over S'} (g : U ⟶ Over.mk x') :
    hX'.homEquiv g = G.map ((Over.map s).map g).op (univ s G x' hX')
theorem

unitMap_repAct

L256 ↗
AlgebraicGeometry.DescentAction.unitMap_repAct
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section repAct
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {X' : Scheme.{u}} (x' :
  X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
Lean source · statement
theorem unitMap_repAct : unitMap s x' ≫ repAct s G x' hX' = 𝟙 X'
theorem

actMap_repAct

L272 ↗
AlgebraicGeometry.DescentAction.actMap_repAct
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section repAct
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {X' : Scheme.{u}} (x' :
  X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
Lean source · statement
theorem actMap_repAct :
    actMap (repAct s G x' hX') (repAct_comp s G x' hX') ≫ repAct s G x' hX' =
      proj₁₃ s x' ≫ repAct s G x' hX'
def

ofRepresentableBy

L306 ↗
AlgebraicGeometry.DescentAction.ofRepresentableBy
Documentation

The descent action on an object representing the pulled-back functor.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section repAct
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {X' : Scheme.{u}} (x' :
  X' ⟶ S')
  (hX' : ((Over.map s).op ⋙ G).RepresentableBy (Over.mk x'))
Lean source · full declaration
def ofRepresentableBy : DescentAction s x' where
  act := repAct s G x' hX'
  act_comp := repAct_comp s G x' hX'
  unit_act := unitMap_repAct s G x' hX'
  trans := actMap_repAct s G x' hX'
def

cover

L326 ↗
AlgebraicGeometry.DescentAction.cover
Documentation

The covering projection from a base-changed scheme, regarded over the original base.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 cover : (Over.map s).obj (Over.mk (pullback.snd f s)) ⟶ Over.mk f
theorem

counit_app_eq_cover

L329 ↗
AlgebraicGeometry.DescentAction.counit_app_eq_cover
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 counit_app_eq_cover : (Over.mapPullbackAdj s).counit.app (Over.mk f) = cover s f
def

eOver

L334 ↗
AlgebraicGeometry.DescentAction.eOver
Documentation

The specified comparison isomorphism regarded in the category over the new base.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 eOver : Over.mk (pullback.snd f s) ≅ Over.mk x'
def

univBC

L337 ↗
AlgebraicGeometry.DescentAction.univBC
Documentation

The universal element transported along the comparison isomorphism after base change.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 univBC : G.obj (op ((Over.map s).obj (Over.mk (pullback.snd f s))))
def

eRel

L341 ↗
AlgebraicGeometry.DescentAction.eRel
Documentation

The morphism of relation pullbacks induced by the comparison isomorphism.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 eRel : pullback (pullback.snd f s ≫ s) s ⟶ pullback (x' ≫ s) s
theorem

eRel_fst

L345 ↗
AlgebraicGeometry.DescentAction.eRel_fst
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 eRel_fst : eRel s x' f e he ≫ pullback.fst _ _ = pullback.fst _ _
  ≫ e.hom
theorem

eRel_snd

L348 ↗
AlgebraicGeometry.DescentAction.eRel_snd
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 eRel_snd : eRel s x' f e he ≫ pullback.snd _ _ = pullback.snd _ _
theorem

univBC_compatible

L352 ↗
AlgebraicGeometry.DescentAction.univBC_compatible
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 univBC_compatible
    (hcompat : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫ e.hom)
    {Z : Over S} (p₁ p₂ : Z ⟶ (Over.map s).obj (Over.mk (pullback.snd f s)))
    (hp : p₁ ≫ cover s f = p₂ ≫ cover s f) :
    G.map p₁.op (univBC s G x' hX' f e he) = G.map p₂.op (univBC s G x' hX' f e he)
theorem

existsUnique_univX

L405 ↗
AlgebraicGeometry.DescentAction.existsUnique_univX
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 existsUnique_univX (hG : Presieve.IsSheafFor G (Presieve.singleton (cover s f)))
    (hcompat : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫ e.hom) :
    ∃! ζ : G.obj (op (Over.mk f)), G.map (cover s f).op ζ = univBC s G x' hX' f e he
def

coverT

L412 ↗
AlgebraicGeometry.DescentAction.coverT
Documentation

The canonical covering projection for an arbitrary scheme over the base.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 coverT (T : Over S) : (Over.map s).obj ((Over.pullback s).obj T) ⟶ T
theorem

counit_app_eq_coverT

L415 ↗
AlgebraicGeometry.DescentAction.counit_app_eq_coverT
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 counit_app_eq_coverT (T : Over S) : (Over.mapPullbackAdj s).counit.app T = coverT s T
theorem

hom_mk_w

L419 ↗
AlgebraicGeometry.DescentAction.hom_mk_w
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 hom_mk_w {T : Over S} (m : T ⟶ Over.mk f) : m.left ≫ f = T.hom
def

bc

L422 ↗
AlgebraicGeometry.DescentAction.bc
Documentation

Base change of a morphism followed by the specified comparison isomorphism.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 bc {T : Over S} (m : T ⟶ Over.mk f) : (Over.pullback s).obj T ⟶ Over.mk x'
theorem

bc_left

L425 ↗
AlgebraicGeometry.DescentAction.bc_left
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 · full declaration
theorem bc_left {T : Over S} (m : T ⟶ Over.mk f) :
    (bc s x' f e he m).left = pullback.lift (pullback.fst T.hom s ≫ m.left) (pullback.snd T.hom s)
      (by rw [Category.assoc, hom_mk_w]; exact pullback.condition) ≫ e.hom := rfl
theorem

coverT_comp

L429 ↗
AlgebraicGeometry.DescentAction.coverT_comp
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 coverT_comp {T : Over S} (m : T ⟶ Over.mk f) :
    coverT s T ≫ m = (Over.map s).map ((Over.pullback s).map m) ≫ cover s f
abbrev

leftHom

L438 ↗
AlgebraicGeometry.DescentAction.leftHom
Documentation

The underlying scheme morphism of a morphism over the new base.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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
abbrev leftHom {T : Over S} (n : (Over.pullback s).obj T ⟶ Over.mk x') : pullback
  T.hom s ⟶ X'
theorem

leftHom_comp

L441 ↗
AlgebraicGeometry.DescentAction.leftHom_comp
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 leftHom_comp {T : Over S} (n : (Over.pullback s).obj T ⟶ Over.mk x') :
    leftHom s x' n ≫ x' = pullback.snd T.hom s
def

nRel

L445 ↗
AlgebraicGeometry.DescentAction.nRel
Documentation

The induced morphism between the relation pullbacks of the source and target.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 nRel {T : Over S} (n : (Over.pullback s).obj T ⟶ Over.mk x') :
    pullback (pullback.snd T.hom s ≫ s) s ⟶ pullback (x' ≫ s) s
theorem

nRel_fst

L451 ↗
AlgebraicGeometry.DescentAction.nRel_fst
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 nRel_fst {T : Over S} (n : (Over.pullback s).obj T ⟶ Over.mk x') :
    nRel s x' n ≫ pullback.fst _ _ = pullback.fst _ _ ≫ leftHom s x' n
theorem

nRel_snd

L453 ↗
AlgebraicGeometry.DescentAction.nRel_snd
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 nRel_snd {T : Over S} (n : (Over.pullback s).obj T ⟶ Over.mk x') :
    nRel s x' n ≫ pullback.snd _ _ = pullback.snd _ _
theorem

flipMap_comp_leftHom

L457 ↗
AlgebraicGeometry.DescentAction.flipMap_comp_leftHom
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 flipMap_comp_leftHom {T : Over S} (z : G.obj (op T)) :
    flipMap s T.hom ≫ leftHom s x' (hX'.homEquiv.symm (G.map (coverT s T).op z)) =
      nRel s x' (hX'.homEquiv.symm (G.map (coverT s T).op z)) ≫ repAct s G x' hX'
theorem

desc_condition

L487 ↗
AlgebraicGeometry.DescentAction.desc_condition
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 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 T)) {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 (G.map (coverT s T).op z)) ≫ e.inv ≫ pullback.fst f s) =
      g₂ ≫ (leftHom s x' (hX'.homEquiv.symm (G.map (coverT s T).op z)) ≫ e.inv ≫ pullback.fst f s)
theorem

map_coverT_map_eq_homEquiv_bc

L535 ↗
AlgebraicGeometry.DescentAction.map_coverT_map_eq_homEquiv_bc
Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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)
section withζ
variable (ζ : G.obj (op (Over.mk f))) (hζ : G.map (cover s f).op ζ = univBC s G x' hX' f e he)
include hζ in
Lean source · statement
theorem map_coverT_map_eq_homEquiv_bc {T : Over S} (m : T ⟶ Over.mk f) :
    G.map (coverT s T).op (G.map m.op ζ) = hX'.homEquiv (bc s x' f e he m)
theorem

map_ζ_injective

L549 ↗
AlgebraicGeometry.DescentAction.map_ζ_injective
Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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)
section withζ
variable (ζ : G.obj (op (Over.mk f))) (hζ : G.map (cover s f).op ζ = univBC s G x' hX' f e he)
include hζ in
Lean source · statement
theorem map_ζ_injective {T : Over S} [Epi (pullback.fst T.hom s)] {m₁ m₂ : T ⟶ Over.mk f}
    (h : G.map m₁.op ζ = G.map m₂.op ζ) : m₁ = m₂
theorem

map_ζ_surjective

L566 ↗
AlgebraicGeometry.DescentAction.map_ζ_surjective
Source context 9 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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)
section withζ
variable (ζ : G.obj (op (Over.mk f))) (hζ : G.map (cover s f).op ζ = univBC s G x' hX' f e he)
include hζ in
Lean source · statement
theorem map_ζ_surjective (hcompat : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫
  e.hom)
    {T : Over S} (hsep : Presieve.IsSeparatedFor G (Presieve.singleton (coverT s T)))
    [EffectiveEpi (pullback.fst T.hom s)] (z : G.obj (op T)) :
    ∃ m : T ⟶ Over.mk f, G.map m.op ζ = z
theorem

representableBy_of_compatible

L609 ↗
AlgebraicGeometry.DescentAction.representableBy_of_compatible
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite
namespace AlgebraicGeometry
namespace DescentAction
section rep
variable {S S' : Scheme.{u}} (s : S' ⟶ S) (G : (Over S)ᵒᵖ ⥤ Type (u + 1)) {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 representableBy_of_compatible
    (hG : ∀ T : Over S, Presieve.IsSheafFor G (Presieve.singleton (coverT s T)))
    [∀ T : Over S, EffectiveEpi (pullback.fst T.hom s)]
    (hcompat : eRel s x' f e he ≫ repAct s G x' hX' = (canonical s f).act ≫ e.hom) :
    Nonempty (G.RepresentableBy (Over.mk f))

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