Module

AffineTransitionOverComparison.lean

Nyll.SchemeTheory.Descent.AffineTransitionOverComparison

13 declarations indexed from sourceView source ↗

Module documentation

Actual pullback comparisons for a cone in an over category

The comparison is built from the chosen scheme pullbacks. Its components preserve both projections, and their naturality is proved by those projections. No limiting or cofilteredness hypothesis is needed.

Imports3

Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Comma.Over.Pullback
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Imported by2

def

overInverseLimitTransition

L32 ↗

AlgebraicGeometry.AffineTransitionHom.overInverseLimitTransition

Documentation

The actual map from a pulled-back model at the cone point to its original stage pullback, preserving the model coordinate and the cone leg.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S : Scheme.{u}}
variable (D : I ⥤ Over S) (c : Cone D)

Lean source · statement

def overInverseLimitTransition (A : Over S) (i : I) :
    pullback A.hom c.pt.hom ⟶ pullback A.hom (D.obj i).hom

theorem

overInverseLimitTransition_fst

L41 ↗

AlgebraicGeometry.AffineTransitionHom.overInverseLimitTransition_fst

Documentation

The transition preserves the original model projection.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S : Scheme.{u}}
variable (D : I ⥤ Over S) (c : Cone D)

Lean source · statement

theorem overInverseLimitTransition_fst (A : Over S) (i : I) :
    overInverseLimitTransition D c A i ≫ pullback.fst A.hom (D.obj i).hom =
      pullback.fst A.hom c.pt.hom

theorem

overInverseLimitTransition_snd

L47 ↗

AlgebraicGeometry.AffineTransitionHom.overInverseLimitTransition_snd

Documentation

The transition's coefficient projection is the original cone leg.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S : Scheme.{u}}
variable (D : I ⥤ Over S) (c : Cone D)

Lean source · statement

theorem overInverseLimitTransition_snd (A : Over S) (i : I) :
    overInverseLimitTransition D c A i ≫ pullback.snd A.hom (D.obj i).hom =
      pullback.snd A.hom c.pt.hom ≫ (c.π.app i).left

def

overInverseLimitComponent

L52 ↗

AlgebraicGeometry.AffineTransitionHom.overInverseLimitComponent

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S : Scheme.{u}}
variable (D : I ⥤ Over S) (c : Cone D)

Lean source · statement

def overInverseLimitComponent (A : Over S) (i : I) :
    pullback A.hom c.pt.hom ≅
      pullback (pullback.snd A.hom (D.obj i).hom) (c.π.app i).left

theorem

overInverseLimitComponent_hom_fst_fst

L58 ↗

AlgebraicGeometry.AffineTransitionHom.overInverseLimitComponent_hom_fst_fst

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S : Scheme.{u}}
variable (D : I ⥤ Over S) (c : Cone D)

Lean source · statement

theorem overInverseLimitComponent_hom_fst_fst (A : Over S) (i : I) :
    (overInverseLimitComponent D c A i).hom ≫
        pullback.fst (pullback.snd A.hom (D.obj i).hom) (c.π.app i).left ≫
        pullback.fst A.hom (D.obj i).hom = pullback.fst A.hom c.pt.hom

theorem

overInverseLimitComponent_hom_snd

L67 ↗

AlgebraicGeometry.AffineTransitionHom.overInverseLimitComponent_hom_snd

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S : Scheme.{u}}
variable (D : I ⥤ Over S) (c : Cone D)

Lean source · statement

theorem overInverseLimitComponent_hom_snd (A : Over S) (i : I) :
    (overInverseLimitComponent D c A i).hom ≫
        pullback.snd (pullback.snd A.hom (D.obj i).hom) (c.π.app i).left =
      pullback.snd A.hom c.pt.hom

theorem

overInverseLimitComponent_hom_fst

L76 ↗

AlgebraicGeometry.AffineTransitionHom.overInverseLimitComponent_hom_fst

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S : Scheme.{u}}
variable (D : I ⥤ Over S) (c : Cone D)

Lean source · statement

theorem overInverseLimitComponent_hom_fst (A : Over S) (i : I) :
    (overInverseLimitComponent D c A i).hom ≫
        pullback.fst (pullback.snd A.hom (D.obj i).hom) (c.π.app i).left =
      overInverseLimitTransition D c A i

theorem

overInverseLimitTransition_naturality

L86 ↗

AlgebraicGeometry.AffineTransitionHom.overInverseLimitTransition_naturality

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S : Scheme.{u}}
variable (D : I ⥤ Over S) (c : Cone D)

Lean source · statement

theorem overInverseLimitTransition_naturality
    {A B : Over S} (f : A ⟶ B) (i : I) :
    ((Over.pullback c.pt.hom).map f).left ≫ overInverseLimitTransition D c B i =
      overInverseLimitTransition D c A i ≫ ((Over.pullback (D.obj i).hom).map f).left

def

overInverseLimitPullbackComparison

L100 ↗

AlgebraicGeometry.AffineTransitionHom.overInverseLimitPullbackComparison

Documentation

The native comparison between pulling back directly to the cone point and pulling back through an original stage.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S : Scheme.{u}}
variable (D : I ⥤ Over S) (c : Cone D)

Lean source · statement

def overInverseLimitPullbackComparison (i : I) :
    Over.pullback c.pt.hom ≅
      Over.pullback (D.obj i).hom ⋙ Over.pullback (c.π.app i).left

theorem

overInverseLimitPullbackComparison_hom_fst

L134 ↗

AlgebraicGeometry.AffineTransitionHom.overInverseLimitPullbackComparison_hom_fst

Documentation

The forward comparison's first projection is the actual scheme transition used in raw model recovery.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S : Scheme.{u}}
variable (D : I ⥤ Over S) (c : Cone D)

Lean source · statement

theorem overInverseLimitPullbackComparison_hom_fst (A : Over S) (i : I) :
    ((overInverseLimitPullbackComparison D c i).hom.app A).left ≫
        pullback.fst (pullback.snd A.hom (D.obj i).hom) (c.π.app i).left =
      overInverseLimitTransition D c A i

theorem

overInverseLimitPullbackComparison_hom_snd

L141 ↗

AlgebraicGeometry.AffineTransitionHom.overInverseLimitPullbackComparison_hom_snd

Documentation

The forward comparison preserves the projection to the cone point.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S : Scheme.{u}}
variable (D : I ⥤ Over S) (c : Cone D)

Lean source · statement

theorem overInverseLimitPullbackComparison_hom_snd (A : Over S) (i : I) :
    ((overInverseLimitPullbackComparison D c i).hom.app A).left ≫
        pullback.snd (pullback.snd A.hom (D.obj i).hom) (c.π.app i).left =
      pullback.snd A.hom c.pt.hom

theorem

overInverseLimitPullbackComparison_inv_fst

L148 ↗

AlgebraicGeometry.AffineTransitionHom.overInverseLimitPullbackComparison_inv_fst

Documentation

The inverse comparison preserves the original model coordinate.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S : Scheme.{u}}
variable (D : I ⥤ Over S) (c : Cone D)

Lean source · statement

theorem overInverseLimitPullbackComparison_inv_fst (A : Over S) (i : I) :
    ((overInverseLimitPullbackComparison D c i).inv.app A).left ≫
        pullback.fst A.hom c.pt.hom =
      pullback.fst (pullback.snd A.hom (D.obj i).hom) (c.π.app i).left ≫
        pullback.fst A.hom (D.obj i).hom

theorem

overInverseLimitPullbackComparison_inv_snd

L160 ↗

AlgebraicGeometry.AffineTransitionHom.overInverseLimitPullbackComparison_inv_snd

Documentation

The inverse comparison preserves the coefficient coordinate.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.AffineTransitionHom
variable {I : Type u} [Category.{u} I] {S : Scheme.{u}}
variable (D : I ⥤ Over S) (c : Cone D)

Lean source · statement

theorem overInverseLimitPullbackComparison_inv_snd (A : Over S) (i : I) :
    ((overInverseLimitPullbackComparison D c i).inv.app A).left ≫
        pullback.snd A.hom c.pt.hom =
      pullback.snd (pullback.snd A.hom (D.obj i).hom) (c.π.app i).left

Module documentation

Actual pullback comparisons for a cone in an over category

Declarations