Module

AffineAlgebraCoaction.lean

Nyll.SchemeTheory.Descent.AffineAlgebraCoaction

9 declarations indexed from sourceView source ↗

Module documentation

Algebra coactions from affine overlap isomorphisms

The two affine overlap schemes have coordinate rings C ⊗[R] B and B ⊗[R] C. An isomorphism between them over Spec (B ⊗[R] B) determines an actual algebra equivalence by the full faithfulness of Spec. Its linearity follows from the given square over the overlap base. The scheme diagonal normalization gives the literal diagonal law used by Algebra.Descent.tensorCoaction_counit.

Imports8

Nyll.SchemeTheory.Descent.AlgebraCoaction
Mathlib.Algebra.Algebra.Equiv
Mathlib.Algebra.Category.Ring.Basic
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.AlgebraicGeometry.Scheme
Mathlib.CategoryTheory.Functor.FullyFaithful
Mathlib.CategoryTheory.Opposites
Mathlib.RingTheory.TensorProduct.Maps

Imported by6

def

affineOverlapSourceBase

L42 ↗

Algebra.Descent.affineOverlapSourceBase

Documentation

The structure map of the first affine overlap over the tensor-square base.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory 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

def affineOverlapSourceBase : B ⊗[R] B →ₐ[B] C ⊗[R] B

def

affineOverlapTargetBase

L46 ↗

Algebra.Descent.affineOverlapTargetBase

Documentation

The structure map of the second affine overlap over the tensor-square base.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory 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

def affineOverlapTargetBase : B ⊗[R] B →ₐ[B] B ⊗[R] C

def

affineOverlapRingEquiv

L50 ↗

Algebra.Descent.affineOverlapRingEquiv

Documentation

The ring equivalence induced contravariantly by an isomorphism of the affine overlap schemes.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory 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

def affineOverlapRingEquiv
    (α : Spec (.of (B ⊗[R] C)) ≅ Spec (.of (C ⊗[R] B))) :
    C ⊗[R] B ≃+* B ⊗[R] C

theorem

affineOverlapRingEquiv_spec

L58 ↗

Algebra.Descent.affineOverlapRingEquiv_spec

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory 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]
omit [Algebra B C] [IsScalarTower R B C] in

Lean source · statement

theorem affineOverlapRingEquiv_spec
    (α : Spec (.of (B ⊗[R] C)) ≅ Spec (.of (C ⊗[R] B))) :
    Spec.map (CommRingCat.ofHom (affineOverlapRingEquiv R B C α).toRingHom) =
      α.hom

theorem

affineOverlapRingEquiv_base

L64 ↗

Algebra.Descent.affineOverlapRingEquiv_base

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory 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 affineOverlapRingEquiv_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))
    (z : B ⊗[R] B) :
    affineOverlapRingEquiv R B C α (affineOverlapSourceBase R B C z) =
      affineOverlapTargetBase R B C z

def

affineOverlapAlgEquiv

L83 ↗

Algebra.Descent.affineOverlapAlgEquiv

Documentation

The algebra overlap equivalence extracted from a scheme isomorphism over the actual affine overlap base. The direction reverses under Spec.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory 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

def affineOverlapAlgEquiv
    (α : 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)) :
    C ⊗[R] B ≃ₐ[B] B ⊗[R] C

theorem

affineOverlapAlgEquiv_spec

L101 ↗

Algebra.Descent.affineOverlapAlgEquiv_spec

Documentation

The constructed algebra equivalence induces the given overlap map exactly.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory 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_spec
    (α : 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)) :
    Spec.map (CommRingCat.ofHom (affineOverlapAlgEquiv R B C α hα).toRingHom) =
      α.hom

theorem

affineOverlapAlgEquiv_base

L111 ↗

Algebra.Descent.affineOverlapAlgEquiv_base

Documentation

The whole tensor-square structure map is preserved, including its second coordinate, not only the scalar action used to bundle the equivalence.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory 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_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)) :
    (affineOverlapAlgEquiv R B C α hα).toAlgHom.comp (affineOverlapSourceBase R B C) =
      affineOverlapTargetBase R B C

theorem

affineOverlapAlgEquiv_diagonal

L121 ↗

Algebra.Descent.affineOverlapAlgEquiv_diagonal

Documentation

Diagonal normalization of the scheme overlap isomorphism yields the exact algebra diagonal law required by the coaction construction.

Source context 7 commands

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

@[expose] public noncomputable section
open CategoryTheory 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_diagonal
    (α : 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))
    (hdiag : Spec.map (CommRingCat.ofHom (tensorTargetDiagonal R B C).toRingHom) ≫
        α.hom = Spec.map (CommRingCat.ofHom (tensorSourceDiagonal R B C).toRingHom)) :
    (tensorTargetDiagonal R B C).comp (affineOverlapAlgEquiv R B C α hα).toAlgHom =
      tensorSourceDiagonal R B C

Module documentation

Algebra coactions from affine overlap isomorphisms

Declarations