NYLL
Module

AffineCocycle.lean

Nyll.SchemeTheory.Descent.AffineCocycle
16 declarations indexed from sourceView source ↗

Module documentation

The affine cocycle from geometric descent actions

The geometric action law is an equality of maps from an actual iterated pullback. Tensor-product coordinates identify it with coassociativity. Together with the overlap square over the tensor-square base, this supplies the full tensor cocycle used for faithfully flat algebra descent.

Imports9
Imported by7

Declarations

def

pullbackActionStep

L40 ↗
AlgebraicGeometry.pullbackActionStep
Documentation

Apply an action on the last two coordinates of a genuine triple fiber product.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace AlgebraicGeometry
variable {S Y Z : Scheme.{u}} (f : Y ⟶ S) (g : Z ⟶ S)
Lean source · statement
def pullbackActionStep (a : pullback f g ⟶ Z)
    (ha : a ≫ g = pullback.fst f g ≫ f) :
    pullback f (pullback.fst f g ≫ f) ⟶ pullback f g
def

pullbackSkipMiddle

L48 ↗
AlgebraicGeometry.pullbackSkipMiddle
Documentation

Forget the middle coordinate of a genuine triple fiber product.

Source context 6 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace AlgebraicGeometry
variable {S Y Z : Scheme.{u}} (f : Y ⟶ S) (g : Z ⟶ S)
Lean source · statement
def pullbackSkipMiddle : pullback f (pullback.fst f g ≫ f) ⟶ pullback f g
theorem

tensorCocycle_eq_of_coaction_coassoc

L62 ↗
Algebra.Descent.tensorCocycle_eq_of_coaction_coassoc
Documentation

Compatibility with both overlap-base coordinates promotes coassociativity of the extracted coaction to the full triple-overlap cocycle.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
Lean source · statement
theorem tensorCocycle_eq_of_coaction_coassoc
    (θ : C ⊗[R] B ≃ₐ[B] B ⊗[R] C)
    (hbase : θ.toAlgHom.comp (affineOverlapSourceBase R B C) =
      affineOverlapTargetBase R B C)
    (hcoassoc : ∀ c : C,
      Algebra.TensorProduct.map (.id R B) ((tensorCoaction R B C θ).restrictScalars R)
          (tensorCoaction R B C θ c) =
        Algebra.TensorProduct.map (.id R B)
          (Algebra.TensorProduct.includeRight : C →ₐ[R] B ⊗[R] C)
          (tensorCoaction R B C θ c)) :
    tensorCocycleLeft R B C θ = tensorCocycleRight R B C θ
def

affineCoactionAction

L140 ↗
Algebra.Descent.affineCoactionAction
Documentation

The map on actual affine pullbacks represented by an algebra coaction.

Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
section Coaction
omit [Algebra B C] [IsScalarTower R B C]
Lean source · statement
def affineCoactionAction (ρ : C →ₐ[R] B ⊗[R] C) :
    pullback (Spec.map (CommRingCat.ofHom (algebraMap R B)))
      (Spec.map (CommRingCat.ofHom (algebraMap R C))) ⟶ Spec (.of C)
theorem

affineCoactionAction_base

L145 ↗
Algebra.Descent.affineCoactionAction_base
Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
section Coaction
omit [Algebra B C] [IsScalarTower R B C]
Lean source · statement
theorem affineCoactionAction_base (ρ : C →ₐ[R] B ⊗[R] C) :
    affineCoactionAction R B C ρ ≫ Spec.map (CommRingCat.ofHom (algebraMap R C)) =
      pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap R B)))
        (Spec.map (CommRingCat.ofHom (algebraMap R C))) ≫
          Spec.map (CommRingCat.ofHom (algebraMap R B))
def

affineTripleChart

L158 ↗
Algebra.Descent.affineTripleChart
Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
section Coaction
omit [Algebra B C] [IsScalarTower R B C]
Lean source · statement
def affineTripleChart :
    Spec (.of (B ⊗[R] (B ⊗[R] C))) ⟶
      pullback (Spec.map (CommRingCat.ofHom (algebraMap R B)))
        (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap R B)))
          (Spec.map (CommRingCat.ofHom (algebraMap R C))) ≫
            Spec.map (CommRingCat.ofHom (algebraMap R B)))
theorem

affineTripleChart_fst

L169 ↗
Algebra.Descent.affineTripleChart_fst
Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
section Coaction
omit [Algebra B C] [IsScalarTower R B C]
Lean source · statement
theorem affineTripleChart_fst :
    affineTripleChart R B C ≫ pullback.fst _ _ =
      Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeLeft :
        B →ₐ[R] B ⊗[R] (B ⊗[R] C)).toRingHom)
theorem

affineTripleChart_snd

L176 ↗
Algebra.Descent.affineTripleChart_snd
Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
section Coaction
omit [Algebra B C] [IsScalarTower R B C]
Lean source · statement
theorem affineTripleChart_snd :
    affineTripleChart R B C ≫ pullback.snd _ _ =
      Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeRight :
        B ⊗[R] C →ₐ[R] B ⊗[R] (B ⊗[R] C)).toRingHom) ≫
          (pullbackSpecIso R B C).inv
theorem

affineTripleChart_actionStep

L185 ↗
Algebra.Descent.affineTripleChart_actionStep
Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
section Coaction
omit [Algebra B C] [IsScalarTower R B C]
Lean source · statement
theorem affineTripleChart_actionStep (ρ : C →ₐ[R] B ⊗[R] C) :
    affineTripleChart R B C ≫
        pullbackActionStep (Spec.map (CommRingCat.ofHom (algebraMap R B)))
          (Spec.map (CommRingCat.ofHom (algebraMap R C))) (affineCoactionAction R B C ρ)
          (affineCoactionAction_base R B C ρ) =
      Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.map (.id R B) ρ).toRingHom) ≫
        (pullbackSpecIso R B C).inv
theorem

affineTripleChart_skipMiddle

L209 ↗
Algebra.Descent.affineTripleChart_skipMiddle
Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
section Coaction
omit [Algebra B C] [IsScalarTower R B C]
Lean source · statement
theorem affineTripleChart_skipMiddle :
    affineTripleChart R B C ≫
        pullbackSkipMiddle (Spec.map (CommRingCat.ofHom (algebraMap R B)))
          (Spec.map (CommRingCat.ofHom (algebraMap R C))) =
      Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.map (.id R B)
        (Algebra.TensorProduct.includeRight : C →ₐ[R] B ⊗[R] C)).toRingHom) ≫
          (pullbackSpecIso R B C).inv
theorem

affineCoaction_coassoc_of_actionLaw

L229 ↗
Algebra.Descent.affineCoaction_coassoc_of_actionLaw
Documentation

The ordinary associativity law on the actual triple fiber product gives coassociativity on the coordinate ring.

Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
section Coaction
omit [Algebra B C] [IsScalarTower R B C]
Lean source · statement
theorem affineCoaction_coassoc_of_actionLaw (ρ : C →ₐ[R] B ⊗[R] C)
    (htrans :
      pullbackActionStep (Spec.map (CommRingCat.ofHom (algebraMap R B)))
          (Spec.map (CommRingCat.ofHom (algebraMap R C))) (affineCoactionAction R B C ρ)
          (affineCoactionAction_base R B C ρ) ≫ affineCoactionAction R B C ρ =
        pullbackSkipMiddle (Spec.map (CommRingCat.ofHom (algebraMap R B)))
          (Spec.map (CommRingCat.ofHom (algebraMap R C))) ≫ affineCoactionAction R B C ρ)
    (c : C) :
    Algebra.TensorProduct.map (.id R B) ρ (ρ c) =
      Algebra.TensorProduct.map (.id R B)
        (Algebra.TensorProduct.includeRight : C →ₐ[R] B ⊗[R] C) (ρ c)
def

affineOverlapAction

L250 ↗
Algebra.Descent.affineOverlapAction
Documentation

The actual action on the affine pullback extracted from an overlap isomorphism.

Source context 9 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
section Coaction
omit [Algebra B C] [IsScalarTower R B C]
Lean source · statement
def affineOverlapAction
    (α : Spec (.of (B ⊗[R] C)) ≅ Spec (.of (C ⊗[R] B))) :
    pullback (Spec.map (CommRingCat.ofHom (algebraMap R B)))
      (Spec.map (CommRingCat.ofHom (algebraMap R C))) ⟶ Spec (.of C)
theorem

affineOverlapAction_eq_coaction

L261 ↗
Algebra.Descent.affineOverlapAction_eq_coaction
Documentation

Its coordinate-ring map is the coaction extracted from the overlap algebra equivalence.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
Lean source · statement
theorem affineOverlapAction_eq_coaction
    (α : Spec (.of (B ⊗[R] C)) ≅ Spec (.of (C ⊗[R] B)))
    (hα : α.hom ≫ Spec.map (CommRingCat.ofHom (affineOverlapSourceBase R B C).toRingHom) =
      Spec.map (CommRingCat.ofHom (affineOverlapTargetBase R B C).toRingHom)) :
    affineOverlapAction R B C α =
      affineCoactionAction R B C
        ((tensorCoaction R B C (affineOverlapAlgEquiv R B C α hα)).restrictScalars R)
theorem

affineOverlapAction_base

L274 ↗
Algebra.Descent.affineOverlapAction_base
Documentation

The extracted geometric action is a morphism over the original base.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
Lean source · statement
theorem affineOverlapAction_base
    (α : Spec (.of (B ⊗[R] C)) ≅ Spec (.of (C ⊗[R] B)))
    (hα : α.hom ≫ Spec.map (CommRingCat.ofHom (affineOverlapSourceBase R B C).toRingHom) =
      Spec.map (CommRingCat.ofHom (affineOverlapTargetBase R B C).toRingHom)) :
    affineOverlapAction R B C α ≫ Spec.map (CommRingCat.ofHom (algebraMap R C)) =
      pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap R B)))
        (Spec.map (CommRingCat.ofHom (algebraMap R C))) ≫
          Spec.map (CommRingCat.ofHom (algebraMap R B))
theorem

affineOverlapAction_coverBase

L287 ↗
Algebra.Descent.affineOverlapAction_coverBase
Documentation

The action lands over the first coordinate of the cover, as required by the usual geometric descent-action interface.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
Lean source · statement
theorem affineOverlapAction_coverBase
    (α : Spec (.of (B ⊗[R] C)) ≅ Spec (.of (C ⊗[R] B)))
    (hα : α.hom ≫ Spec.map (CommRingCat.ofHom (affineOverlapSourceBase R B C).toRingHom) =
      Spec.map (CommRingCat.ofHom (affineOverlapTargetBase R B C).toRingHom)) :
    affineOverlapAction R B C α ≫ Spec.map (CommRingCat.ofHom (algebraMap B C)) =
      pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap R B)))
        (Spec.map (CommRingCat.ofHom (algebraMap R C)))
theorem

affineOverlapAlgEquiv_cocycle_of_actionLaw

L308 ↗
Algebra.Descent.affineOverlapAlgEquiv_cocycle_of_actionLaw
Documentation

A genuine geometric action law on the triple pullback supplies the full algebra cocycle required for effective faithfully flat descent.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open scoped TensorProduct
universe u
namespace Algebra.Descent
variable (R B C : Type u) [CommRing R] [CommRing B] [CommRing C]
variable [Algebra R B] [Algebra R C] [Algebra B C] [IsScalarTower R B C]
Lean source · statement
theorem affineOverlapAlgEquiv_cocycle_of_actionLaw
    (α : Spec (.of (B ⊗[R] C)) ≅ Spec (.of (C ⊗[R] B)))
    (hα : α.hom ≫ Spec.map (CommRingCat.ofHom (affineOverlapSourceBase R B C).toRingHom) =
      Spec.map (CommRingCat.ofHom (affineOverlapTargetBase R B C).toRingHom))
    (htrans :
      pullbackActionStep (Spec.map (CommRingCat.ofHom (algebraMap R B)))
          (Spec.map (CommRingCat.ofHom (algebraMap R C))) (affineOverlapAction R B C α)
          (affineOverlapAction_base R B C α hα) ≫ affineOverlapAction R B C α =
        pullbackSkipMiddle (Spec.map (CommRingCat.ofHom (algebraMap R B)))
          (Spec.map (CommRingCat.ofHom (algebraMap R C))) ≫ affineOverlapAction R B C α) :
    tensorCocycleLeft R B C (affineOverlapAlgEquiv R B C α hα) =
      tensorCocycleRight R B C (affineOverlapAlgEquiv R B C α hα)

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