Module

AlgebraCoactionTransport.lean

Nyll.SchemeTheory.Descent.AlgebraCoactionTransport

10 declarations indexed from sourceView source ↗

Module documentation

Transporting the canonical algebra coaction

A concrete scalar-extension equivalence gives a concrete coaction. Its two laws follow from the pure-tensor formula for the canonical coaction. These are the upper coactions used when descending a finite radicial local model.

Imports2

Nyll.SchemeTheory.Descent.AlgebraCoaction
Mathlib.RingTheory.TensorProduct.Maps

Imported by4

def

canonicalCoaction

L35 ↗

Algebra.Descent.canonicalCoaction

Documentation

The canonical coaction on a scalar extension.

Source context 8 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Transport
variable (S E U A : Type u) [CommRing S] [CommRing E] [CommRing U] [CommRing A]
variable [Algebra S E] [Algebra S U] [Algebra E U] [IsScalarTower S E U]
variable [Algebra S A]

Lean source · statement

def canonicalCoaction : E ⊗[S] A →ₐ[E] E ⊗[S] (E ⊗[S] A)

def

transportedCoaction

L40 ↗

Algebra.Descent.transportedCoaction

Documentation

The actual coaction obtained by transporting the canonical coaction along the chosen scalar-extension equivalence.

Source context 8 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Transport
variable (S E U A : Type u) [CommRing S] [CommRing E] [CommRing U] [CommRing A]
variable [Algebra S E] [Algebra S U] [Algebra E U] [IsScalarTower S E U]
variable [Algebra S A]

Lean source · statement

def transportedCoaction (e : U ≃ₐ[E] E ⊗[S] A) : U →ₐ[E] E ⊗[S] U

theorem

transportedCoaction_symm_tmul

L44 ↗

Algebra.Descent.transportedCoaction_symm_tmul

Source context 8 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Transport
variable (S E U A : Type u) [CommRing S] [CommRing E] [CommRing U] [CommRing A]
variable [Algebra S E] [Algebra S U] [Algebra E U] [IsScalarTower S E U]
variable [Algebra S A]

Lean source · statement

theorem transportedCoaction_symm_tmul (e : U ≃ₐ[E] E ⊗[S] A) (b : E) (a : A) :
    transportedCoaction S E U A e (e.symm (b ⊗ₜ[S] a)) =
      b ⊗ₜ[S] e.symm ((1 : E) ⊗ₜ[S] a)

theorem

transportedCoaction_comparison

L53 ↗

Algebra.Descent.transportedCoaction_comparison

Documentation

The defining comparison with the actual canonical coaction.

Source context 8 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Transport
variable (S E U A : Type u) [CommRing S] [CommRing E] [CommRing U] [CommRing A]
variable [Algebra S E] [Algebra S U] [Algebra E U] [IsScalarTower S E U]
variable [Algebra S A]

Lean source · statement

theorem transportedCoaction_comparison (e : U ≃ₐ[E] E ⊗[S] A) (x : U) :
    Algebra.TensorProduct.map (.id E E) (e.restrictScalars S).toAlgHom
        (transportedCoaction S E U A e x) = canonicalCoaction S E A (e x)

theorem

transportedCoaction_counit

L67 ↗

Algebra.Descent.transportedCoaction_counit

Documentation

The transported canonical coaction satisfies its actual counit equation.

Source context 8 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Transport
variable (S E U A : Type u) [CommRing S] [CommRing E] [CommRing U] [CommRing A]
variable [Algebra S E] [Algebra S U] [Algebra E U] [IsScalarTower S E U]
variable [Algebra S A]

Lean source · statement

theorem transportedCoaction_counit (e : U ≃ₐ[E] E ⊗[S] A) (x : U) :
    tensorTargetDiagonal S E U (transportedCoaction S E U A e x) = x

theorem

transportedCoaction_coassoc

L82 ↗

Algebra.Descent.transportedCoaction_coassoc

Documentation

The transported canonical coaction satisfies coassociativity.

Source context 8 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Transport
variable (S E U A : Type u) [CommRing S] [CommRing E] [CommRing U] [CommRing A]
variable [Algebra S E] [Algebra S U] [Algebra E U] [IsScalarTower S E U]
variable [Algebra S A]

Lean source · statement

theorem transportedCoaction_coassoc (e : U ≃ₐ[E] E ⊗[S] A) (x : U) :
    Algebra.TensorProduct.map (.id E E)
        ((transportedCoaction S E U A e).restrictScalars S)
        (transportedCoaction S E U A e x) =
      Algebra.TensorProduct.map (.id E E)
        (Algebra.TensorProduct.includeRight : U →ₐ[S] E ⊗[S] U)
        (transportedCoaction S E U A e x)

def

scalarTensorIso

L105 ↗

Algebra.Descent.scalarTensorIso

Documentation

The tensor-product comparison that changes the coefficients of a coaction.

Source context 7 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
section TensorComparison
variable (R S B M : Type u) [CommRing R] [CommRing S] [CommRing B] [CommRing M]
variable [Algebra R S] [Algebra R B] [Algebra R M]

Lean source · statement

def scalarTensorIso :
    (S ⊗[R] B) ⊗[S] (S ⊗[R] M) ≃ₐ[S] S ⊗[R] (B ⊗[R] M)

theorem

scalarTensorIso_tmul

L111 ↗

Algebra.Descent.scalarTensorIso_tmul

Source context 7 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
section TensorComparison
variable (R S B M : Type u) [CommRing R] [CommRing S] [CommRing B] [CommRing M]
variable [Algebra R S] [Algebra R B] [Algebra R M]

Lean source · statement

theorem scalarTensorIso_tmul (s t : S) (b : B) (m : M) :
    scalarTensorIso R S B M ((s ⊗ₜ[R] b) ⊗ₜ[S] (t ⊗ₜ[R] m)) =
      (s * t) ⊗ₜ[R] (b ⊗ₜ[R] m)

theorem

scalarTensorIso_natural

L121 ↗

Algebra.Descent.scalarTensorIso_natural

Documentation

Naturality of the coefficient comparison in the algebra carrying the coaction.

Source context 7 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
section TensorComparison
variable (R S B M : Type u) [CommRing R] [CommRing S] [CommRing B] [CommRing M]
variable [Algebra R S] [Algebra R B] [Algebra R M]

Lean source · statement

theorem scalarTensorIso_natural
    {N : Type u} [CommRing N] [Algebra R N] (g : M →ₐ[R] N)
    (z : (S ⊗[R] B) ⊗[S] (S ⊗[R] M)) :
    Algebra.TensorProduct.map (.id S S)
        ((Algebra.TensorProduct.map (.id B B) g).restrictScalars R)
        (scalarTensorIso R S B M z) =
      scalarTensorIso R S B N
        (Algebra.TensorProduct.map (.id S (S ⊗[R] B))
          (Algebra.TensorProduct.map (.id S S) g) z)

theorem

scalarTensorIso_one_tmul

L143 ↗

Algebra.Descent.scalarTensorIso_one_tmul

Documentation

The unit inclusion is preserved by the coefficient comparison.

Source context 7 commands

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

@[expose] public noncomputable section
open scoped TensorProduct
universe u
namespace Algebra.Descent
section TensorComparison
variable (R S B M : Type u) [CommRing R] [CommRing S] [CommRing B] [CommRing M]
variable [Algebra R S] [Algebra R B] [Algebra R M]

Lean source · statement

theorem scalarTensorIso_one_tmul (z : S ⊗[R] M) :
    scalarTensorIso R S B M ((1 : S ⊗[R] B) ⊗ₜ[S] z) =
      Algebra.TensorProduct.map (.id S S)
        (Algebra.TensorProduct.includeRight : M →ₐ[R] B ⊗[R] M) z

Module documentation

Transporting the canonical algebra coaction

Declarations