NYLL
Module

ActionOverlap.lean

Nyll.SchemeTheory.Descent.ActionOverlap
13 declarations indexed from sourceView source ↗

Module documentation

The overlap isomorphism associated with a descent action

An action of the cover groupoid on a scheme over the cover gives an actual isomorphism between the two overlap pullbacks. Its inverse is obtained by exchanging the two cover coordinates and applying the same action.

The only hypotheses are the action's compatibility with its projection, unit law, and associativity law. In particular, no geometric property of the cover morphism is required. The isomorphism preserves both coordinates over the cover's self-pullback and restricts to the identity on the diagonal.

Imports3
Imported by3

Declarations

def

pullbackActionFlip

L41 ↗
AlgebraicGeometry.pullbackActionFlip
Documentation

Exchange the cover coordinates and act on the scheme coordinate.

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {X Y W : Scheme.{u}} (f : Y ⟶ X) (p : W ⟶ Y)
  (a : pullback f (p ≫ f) ⟶ W)
  (ha : a ≫ p = pullback.fst f (p ≫ f))
Lean source · statement
def pullbackActionFlip : pullback f (p ≫ f) ⟶ pullback f (p ≫ f)
lemma

pullbackActionFlip_fst

L45 ↗
AlgebraicGeometry.pullbackActionFlip_fst
Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {X Y W : Scheme.{u}} (f : Y ⟶ X) (p : W ⟶ Y)
  (a : pullback f (p ≫ f) ⟶ W)
  (ha : a ≫ p = pullback.fst f (p ≫ f))
Lean source · statement
lemma pullbackActionFlip_fst : pullbackActionFlip f p a ha ≫ pullback.fst f (p ≫ f) =
    pullback.snd f (p ≫ f) ≫ p
lemma

pullbackActionFlip_snd

L49 ↗
AlgebraicGeometry.pullbackActionFlip_snd
Source context 6 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {X Y W : Scheme.{u}} (f : Y ⟶ X) (p : W ⟶ Y)
  (a : pullback f (p ≫ f) ⟶ W)
  (ha : a ≫ p = pullback.fst f (p ≫ f))
Lean source · statement
lemma pullbackActionFlip_snd : pullbackActionFlip f p a ha ≫ pullback.snd f (p ≫ f) = a
lemma

pullbackActionFlip_action

L60 ↗
AlgebraicGeometry.pullbackActionFlip_action
Source context 8 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {X Y W : Scheme.{u}} (f : Y ⟶ X) (p : W ⟶ Y)
  (a : pullback f (p ≫ f) ⟶ W)
  (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 W)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 W)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
include hunit hassoc
Lean source · statement
lemma pullbackActionFlip_action :
    pullbackActionFlip f p a ha ≫ a = pullback.snd f (p ≫ f)
lemma

pullbackActionFlip_sq

L88 ↗
AlgebraicGeometry.pullbackActionFlip_sq
Documentation

The unit and associativity laws make the action flip an involution.

Source context 8 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {X Y W : Scheme.{u}} (f : Y ⟶ X) (p : W ⟶ Y)
  (a : pullback f (p ≫ f) ⟶ W)
  (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 W)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 W)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
include hunit hassoc
Lean source · statement
lemma pullbackActionFlip_sq : pullbackActionFlip f p a ha ≫ pullbackActionFlip f p a ha = 𝟙 _
def

pullbackActionOverlapIso

L96 ↗
AlgebraicGeometry.pullbackActionOverlapIso
Documentation

The overlap isomorphism of an action, constructed from its unit and associativity laws.

Source context 8 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {X Y W : Scheme.{u}} (f : Y ⟶ X) (p : W ⟶ Y)
  (a : pullback f (p ≫ f) ⟶ W)
  (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 W)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 W)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
include hunit hassoc
Lean source · statement
def pullbackActionOverlapIso : pullback f (p ≫ f) ≅ pullback (p ≫ f) f
lemma

pullbackActionOverlapIso_hom_fst

L103 ↗
AlgebraicGeometry.pullbackActionOverlapIso_hom_fst
Documentation

The first coordinate of the overlap map is the action itself.

Source context 8 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {X Y W : Scheme.{u}} (f : Y ⟶ X) (p : W ⟶ Y)
  (a : pullback f (p ≫ f) ⟶ W)
  (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 W)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 W)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
include hunit hassoc
Lean source · statement
lemma pullbackActionOverlapIso_hom_fst : (pullbackActionOverlapIso f p a ha hunit hassoc).hom ≫
    pullback.fst (p ≫ f) f = a
lemma

pullbackActionOverlapIso_hom_snd

L109 ↗
AlgebraicGeometry.pullbackActionOverlapIso_hom_snd
Documentation

The second coordinate is the original point's image on the cover.

Source context 8 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {X Y W : Scheme.{u}} (f : Y ⟶ X) (p : W ⟶ Y)
  (a : pullback f (p ≫ f) ⟶ W)
  (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 W)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 W)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
include hunit hassoc
Lean source · statement
lemma pullbackActionOverlapIso_hom_snd : (pullbackActionOverlapIso f p a ha hunit hassoc).hom ≫
    pullback.snd (p ≫ f) f = pullback.snd f (p ≫ f) ≫ p
lemma

pullbackActionOverlapIso_inv_fst

L115 ↗
AlgebraicGeometry.pullbackActionOverlapIso_inv_fst
Documentation

The inverse's cover coordinate is the image of its scheme coordinate.

Source context 8 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {X Y W : Scheme.{u}} (f : Y ⟶ X) (p : W ⟶ Y)
  (a : pullback f (p ≫ f) ⟶ W)
  (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 W)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 W)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
include hunit hassoc
Lean source · statement
lemma pullbackActionOverlapIso_inv_fst : (pullbackActionOverlapIso f p a ha hunit hassoc).inv ≫
    pullback.fst f (p ≫ f) = pullback.fst (p ≫ f) f ≫ p
lemma

pullbackActionOverlapIso_inv_snd

L121 ↗
AlgebraicGeometry.pullbackActionOverlapIso_inv_snd
Documentation

The inverse applies the same action after exchanging the input coordinates.

Source context 8 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {X Y W : Scheme.{u}} (f : Y ⟶ X) (p : W ⟶ Y)
  (a : pullback f (p ≫ f) ⟶ W)
  (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 W)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 W)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
include hunit hassoc
Lean source · statement
lemma pullbackActionOverlapIso_inv_snd : (pullbackActionOverlapIso f p a ha hunit hassoc).inv ≫
    pullback.snd f (p ≫ f) = (pullbackSymmetry f (p ≫ f)).inv ≫ a
lemma

pullbackActionOverlapIso_hom_eq_lift

L126 ↗
AlgebraicGeometry.pullbackActionOverlapIso_hom_eq_lift
Documentation

Explicit pullback-lift formula for the forward overlap map.

Source context 8 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {X Y W : Scheme.{u}} (f : Y ⟶ X) (p : W ⟶ Y)
  (a : pullback f (p ≫ f) ⟶ W)
  (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 W)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 W)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
include hunit hassoc
Lean source · full declaration
lemma pullbackActionOverlapIso_hom_eq_lift : (pullbackActionOverlapIso f p a ha hunit hassoc).hom =
    pullback.lift a (pullback.snd f (p ≫ f) ≫ p) (by
      rw [← Category.assoc, ha, Category.assoc, pullback.condition]) := by
  apply pullback.hom_ext
  · rw [pullbackActionOverlapIso_hom_fst, pullback.lift_fst]
  · rw [pullbackActionOverlapIso_hom_snd, pullback.lift_snd]
lemma

pullbackActionOverlapIso_over

L134 ↗
AlgebraicGeometry.pullbackActionOverlapIso_over
Documentation

The overlap isomorphism lies over the cover's self-pullback.

Source context 8 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {X Y W : Scheme.{u}} (f : Y ⟶ X) (p : W ⟶ Y)
  (a : pullback f (p ≫ f) ⟶ W)
  (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 W)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 W)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
include hunit hassoc
Lean source · full declaration
lemma pullbackActionOverlapIso_over :
    (pullbackActionOverlapIso f p a ha hunit hassoc).hom ≫
      pullback.lift (f := f) (g := f) (pullback.fst (p ≫ f) f ≫ p)
        (pullback.snd (p ≫ f) f) (by rw [Category.assoc, pullback.condition]) =
    pullback.lift (f := f) (g := f) (pullback.fst f (p ≫ f))
      (pullback.snd f (p ≫ f) ≫ p) (by rw [Category.assoc, pullback.condition]) := by
  apply pullback.hom_ext
  · rw [Category.assoc, pullback.lift_fst, ← Category.assoc, pullbackActionOverlapIso_hom_fst,
      ha, pullback.lift_fst]
  · rw [Category.assoc, pullback.lift_snd, pullbackActionOverlapIso_hom_snd, pullback.lift_snd]
lemma

pullbackActionOverlapIso_diagonal

L146 ↗
AlgebraicGeometry.pullbackActionOverlapIso_diagonal
Documentation

The overlap isomorphism restricts to the identity over the diagonal.

Source context 8 commands

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

@[expose] public section
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
variable {X Y W : Scheme.{u}} (f : Y ⟶ X) (p : W ⟶ Y)
  (a : pullback f (p ≫ f) ⟶ W)
  (ha : a ≫ p = pullback.fst f (p ≫ f))
variable
  (hunit : pullback.lift (f := f) (g := p ≫ f) p (𝟙 W)
    (Category.id_comp (p ≫ f)).symm ≫ a = 𝟙 W)
  (hassoc : pullbackActionStep f (p ≫ f) a (by rw [← Category.assoc, ha]) ≫ a =
    pullbackSkipMiddle f (p ≫ f) ≫ a)
include hunit hassoc
Lean source · statement
lemma pullbackActionOverlapIso_diagonal :
    pullback.lift (f := f) (g := p ≫ f) p (𝟙 W)
        (Category.id_comp (p ≫ f)).symm ≫ (pullbackActionOverlapIso f p a ha hunit hassoc).hom =
      pullback.lift (f := p ≫ f) (g := f) (𝟙 W) p (Category.id_comp (p ≫ f))

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