Module

AlgebraCoaction.lean

Nyll.SchemeTheory.Descent.AlgebraCoaction

15 declarations indexed from sourceView source ↗

Module documentation

From tensor-form descent isomorphisms to algebra coactions

An overlap isomorphism is written as C ⊗[R] B ≃ₐ[B] B ⊗[R] C. Its diagonal normalization is an equality after the two multiplication maps. Its triple cocycle compares two explicit maps from C ⊗[R] (B ⊗[R] B) to B ⊗[R] (B ⊗[R] C), using the tensor associator and exchanges of factors. Evaluating these genuine overlap laws on c ⊗ 1 and c ⊗ 1 ⊗ 1 gives the counit and coassociativity of the native scalar-extension comonad.

Imports4

Nyll.SchemeTheory.Descent.FaithfullyFlatAlgebra
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
Mathlib.CategoryTheory.Monad.Adjunction
Mathlib.RingTheory.TensorProduct.Maps

Imported by10

def

tensorCoaction

L41 ↗

Algebra.Descent.tensorCoaction

Documentation

The coaction extracted from the actual overlap isomorphism.

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Tensor
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 tensorCoaction (θ : C ⊗[R] B ≃ₐ[B] B ⊗[R] C) : C →ₐ[B] B ⊗[R] C

theorem

tensorCoaction_apply

L45 ↗

Algebra.Descent.tensorCoaction_apply

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Tensor
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 tensorCoaction_apply (θ : C ⊗[R] B ≃ₐ[B] B ⊗[R] C) (c : C) :
    tensorCoaction R B C θ c = θ (c ⊗ₜ[R] (1 : B))

def

tensorSourceDiagonal

L49 ↗

Algebra.Descent.tensorSourceDiagonal

Documentation

Restricting the source of the overlap comparison to the diagonal.

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Tensor
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 tensorSourceDiagonal : C ⊗[R] B →ₐ[B] C

def

tensorTargetDiagonal

L54 ↗

Algebra.Descent.tensorTargetDiagonal

Documentation

Restricting the target of the overlap comparison to the diagonal.

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Tensor
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 tensorTargetDiagonal : B ⊗[R] C →ₐ[B] C

def

tensorFirstTransition

L59 ↗

Algebra.Descent.tensorFirstTransition

Documentation

The overlap comparison on the first two of three coordinates.

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Tensor
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 tensorFirstTransition (θ : C ⊗[R] B ≃ₐ[B] B ⊗[R] C) :
    C ⊗[R] (B ⊗[R] B) →ₐ[R] B ⊗[R] (C ⊗[R] B)

def

tensorCocycleLeft

L66 ↗

Algebra.Descent.tensorCocycleLeft

Documentation

The successive first-second and second-third comparisons.

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Tensor
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 tensorCocycleLeft (θ : C ⊗[R] B ≃ₐ[B] B ⊗[R] C) :
    C ⊗[R] (B ⊗[R] B) →ₐ[R] B ⊗[R] (B ⊗[R] C)

def

tensorCocycleRight

L72 ↗

Algebra.Descent.tensorCocycleRight

Documentation

The direct first-third comparison, leaving the middle coordinate fixed.

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Tensor
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 tensorCocycleRight (θ : C ⊗[R] B ≃ₐ[B] B ⊗[R] C) :
    C ⊗[R] (B ⊗[R] B) →ₐ[R] B ⊗[R] (B ⊗[R] C)

theorem

tensorFirstTransition_one

L78 ↗

Algebra.Descent.tensorFirstTransition_one

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Tensor
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 tensorFirstTransition_one
    (θ : C ⊗[R] B ≃ₐ[B] B ⊗[R] C) (c : C) :
    tensorFirstTransition R B C θ (c ⊗ₜ[R] ((1 : B) ⊗ₜ[R] (1 : B))) =
      Algebra.TensorProduct.assoc R R R B C B
        (tensorCoaction R B C θ c ⊗ₜ[R] (1 : B))

theorem

tensorCocycleLeft_one

L88 ↗

Algebra.Descent.tensorCocycleLeft_one

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Tensor
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 tensorCocycleLeft_one
    (θ : C ⊗[R] B ≃ₐ[B] B ⊗[R] C) (c : C) :
    tensorCocycleLeft R B C θ (c ⊗ₜ[R] ((1 : B) ⊗ₜ[R] (1 : B))) =
      Algebra.TensorProduct.map (.id R B) ((tensorCoaction R B C θ).restrictScalars R)
        (tensorCoaction R B C θ c)

theorem

tensorCocycleRight_one

L99 ↗

Algebra.Descent.tensorCocycleRight_one

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Tensor
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 tensorCocycleRight_one
    (θ : C ⊗[R] B ≃ₐ[B] B ⊗[R] C) (c : C) :
    tensorCocycleRight R B C θ (c ⊗ₜ[R] ((1 : B) ⊗ₜ[R] (1 : B))) =
      Algebra.TensorProduct.map (.id R B)
        (Algebra.TensorProduct.includeRight : C →ₐ[R] B ⊗[R] C)
        (tensorCoaction R B C θ c)

theorem

tensorCoaction_counit

L114 ↗

Algebra.Descent.tensorCoaction_counit

Documentation

Diagonal normalization implies the counit identity of the extracted coaction.

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Tensor
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 tensorCoaction_counit
    (θ : C ⊗[R] B ≃ₐ[B] B ⊗[R] C)
    (hdiag : (tensorTargetDiagonal R B C).comp θ.toAlgHom = tensorSourceDiagonal R B C)
    (c : C) : tensorTargetDiagonal R B C (tensorCoaction R B C θ c) = c

theorem

tensorCoaction_coassoc

L125 ↗

Algebra.Descent.tensorCoaction_coassoc

Documentation

The actual triple cocycle implies coassociativity of the extracted coaction.

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Tensor
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 tensorCoaction_coassoc
    (θ : C ⊗[R] B ≃ₐ[B] B ⊗[R] C)
    (hcocycle : tensorCocycleLeft R B C θ = tensorCocycleRight R B C θ)
    (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)

theorem

nativeCoactionAxioms_of_pointwise

L147 ↗

Algebra.Descent.nativeCoactionAxioms_of_pointwise

Documentation

Pointwise counit and coassociativity for an algebra coaction are exactly the two equations of the native scalar-extension comonad.

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Native
variable {R B : Type u} [CommRing R] [CommRing B]
variable (f : R →+* B) (C : Type u) [CommRing C] [Algebra B C]

Lean source · full declaration

theorem nativeCoactionAxioms_of_pointwise :
    let : Algebra R B := f.toAlgebra;
    let : Algebra R C := Algebra.compHom C f;
    let : IsScalarTower R B C := IsScalarTower.of_compHom R B C;
    ∀ (ρ : C →ₐ[B] B ⊗[R] C),
      (∀ c : C, tensorTargetDiagonal R B C (ρ c) = c) →
      (∀ c : C,
        Algebra.TensorProduct.map (.id R B) (ρ.restrictScalars R) (ρ c) =
          Algebra.TensorProduct.map (.id R B)
            (Algebra.TensorProduct.includeRight : C →ₐ[R] B ⊗[R] C) (ρ c)) →
      (FaithfullyFlatDescent.coactionLinear f C ρ ≫
          (ModuleCat.extendRestrictScalarsAdj f).toComonad.ε.app (ModuleCat.of B C) =
        𝟙 (ModuleCat.of B C)) ∧
      (FaithfullyFlatDescent.coactionLinear f C ρ ≫
          (ModuleCat.extendRestrictScalarsAdj f).toComonad.δ.app (ModuleCat.of B C) =
        FaithfullyFlatDescent.coactionLinear f C ρ ≫
          (ModuleCat.extendRestrictScalarsAdj f).toComonad.map
            (FaithfullyFlatDescent.coactionLinear f C ρ)) := by
  intro hRB hRC hTower ρ hcounit hcoassoc
  have hε (z : B ⊗[R] C) :
      (ModuleCat.extendRestrictScalarsAdj f).toComonad.ε.app (ModuleCat.of B C) z =
        tensorTargetDiagonal R B C z := by
    induction z using TensorProduct.inductionOn with
    | tmul b c =>
      change b • c = algebraMap B C b * c
      exact Algebra.smul_def b c
    | add x y hx hy =>
      have hadd :=
        ((ModuleCat.extendRestrictScalarsAdj f).toComonad.ε.app (ModuleCat.of B C)).hom.map_add x y
      have hsum := hadd.trans (congrArg₂ (· + ·) hx hy)
      change ((ModuleCat.extendRestrictScalarsAdj f).toComonad.ε.app
        (ModuleCat.of B C)).hom (x + y) = _
      rw [map_add]
      exact hsum
  have hδ (z : B ⊗[R] C) :
      (ModuleCat.extendRestrictScalarsAdj f).toComonad.δ.app (ModuleCat.of B C) z =
        Algebra.TensorProduct.map (.id R B)
          (Algebra.TensorProduct.includeRight : C →ₐ[R] B ⊗[R] C) z := by
    induction z using TensorProduct.inductionOn with
    | tmul b c => rfl
    | add x y hx hy =>
      have hadd :=
        ((ModuleCat.extendRestrictScalarsAdj f).toComonad.δ.app (ModuleCat.of B C)).hom.map_add x y
      have hsum := hadd.trans (congrArg₂ (· + ·) hx hy)
      change ((ModuleCat.extendRestrictScalarsAdj f).toComonad.δ.app
        (ModuleCat.of B C)).hom (x + y) = _
      rw [map_add]
      exact hsum
  have hmap (z : B ⊗[R] C) :
      (ModuleCat.extendRestrictScalarsAdj f).toComonad.map
          (FaithfullyFlatDescent.coactionLinear f C ρ) z =
        Algebra.TensorProduct.map (.id R B) (ρ.restrictScalars R) z := by
    induction z using TensorProduct.inductionOn with
    | tmul b c => rfl
    | add x y hx hy =>
      have hadd := ((ModuleCat.extendRestrictScalarsAdj f).toComonad.map
        (FaithfullyFlatDescent.coactionLinear f C ρ)).hom.map_add x y
      have hsum := hadd.trans (congrArg₂ (· + ·) hx hy)
      change ((ModuleCat.extendRestrictScalarsAdj f).toComonad.map
        (FaithfullyFlatDescent.coactionLinear f C ρ)).hom (x + y) = _
      rw [map_add]
      exact hsum
  constructor
  · apply ModuleCat.hom_ext
    apply LinearMap.ext
    intro c
    change (ModuleCat.extendRestrictScalarsAdj f).toComonad.ε.app
      (ModuleCat.of B C) (ρ c) = c
    rw [hε]
    exact hcounit c
  · apply ModuleCat.hom_ext
    apply LinearMap.ext
    intro c
    change (ModuleCat.extendRestrictScalarsAdj f).toComonad.δ.app
        (ModuleCat.of B C) (ρ c) =
      (ModuleCat.extendRestrictScalarsAdj f).toComonad.map
        (FaithfullyFlatDescent.coactionLinear f C ρ) (ρ c)
    rw [hδ, hmap]
    exact (hcoassoc c).symm

theorem

nativeCoactionAxioms

L229 ↗

Algebra.Descent.nativeCoactionAxioms

Documentation

Tensor-form overlap normalization and cocycle give precisely the two laws of the native scalar-extension comonad, for the constructed coaction.

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Native
variable {R B : Type u} [CommRing R] [CommRing B]
variable (f : R →+* B) (C : Type u) [CommRing C] [Algebra B C]

Lean source · full declaration

theorem nativeCoactionAxioms :
    letI : Algebra R B := f.toAlgebra
    letI : Algebra R C := Algebra.compHom C f
    letI : IsScalarTower R B C := IsScalarTower.of_compHom R B C
    ∀ (θ : C ⊗[R] B ≃ₐ[B] B ⊗[R] C),
      (tensorTargetDiagonal R B C).comp θ.toAlgHom = tensorSourceDiagonal R B C →
      tensorCocycleLeft R B C θ = tensorCocycleRight R B C θ →
      let ρ := tensorCoaction R B C θ
      (FaithfullyFlatDescent.coactionLinear f C ρ ≫
          (ModuleCat.extendRestrictScalarsAdj f).toComonad.ε.app (ModuleCat.of B C) =
        𝟙 (ModuleCat.of B C)) ∧
      (FaithfullyFlatDescent.coactionLinear f C ρ ≫
          (ModuleCat.extendRestrictScalarsAdj f).toComonad.δ.app (ModuleCat.of B C) =
        FaithfullyFlatDescent.coactionLinear f C ρ ≫
          (ModuleCat.extendRestrictScalarsAdj f).toComonad.map
            (FaithfullyFlatDescent.coactionLinear f C ρ)) := by
  let : Algebra R B := f.toAlgebra
  let : Algebra R C := Algebra.compHom C f
  let : IsScalarTower R B C := IsScalarTower.of_compHom R B C
  intro θ hdiag hcocycle
  exact nativeCoactionAxioms_of_pointwise f C (tensorCoaction R B C θ)
    (tensorCoaction_counit R B C θ hdiag)
    (tensorCoaction_coassoc R B C θ hcocycle)

def

tensorDescentEquiv

L255 ↗

Algebra.Descent.tensorDescentEquiv

Documentation

A genuine tensor-form descent isomorphism with its ordinary overlap laws is effective: the invariant subalgebra recovers the given algebra after base change.

Source context 8 commands

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

@[expose] public noncomputable section
open CategoryTheory
open scoped TensorProduct
universe u
namespace Algebra.Descent
section Native
variable {R B : Type u} [CommRing R] [CommRing B]
variable (f : R →+* B) (C : Type u) [CommRing C] [Algebra B C]

Lean source · full declaration

def tensorDescentEquiv (hf : f.FaithfullyFlat) :
    letI : Algebra R B := f.toAlgebra
    letI : Algebra R C := Algebra.compHom C f
    letI : IsScalarTower R B C := IsScalarTower.of_compHom R B C
    (θ : C ⊗[R] B ≃ₐ[B] B ⊗[R] C) →
      (tensorTargetDiagonal R B C).comp θ.toAlgHom = tensorSourceDiagonal R B C →
      tensorCocycleLeft R B C θ = tensorCocycleRight R B C θ →
      B ⊗[R] FaithfullyFlatDescent.invariants f C (tensorCoaction R B C θ) ≃ₐ[B] C := by
  letI : Algebra R B := f.toAlgebra
  letI : Algebra R C := Algebra.compHom C f
  letI : IsScalarTower R B C := IsScalarTower.of_compHom R B C
  intro θ hdiag hcocycle
  exact FaithfullyFlatDescent.invariantsBaseChangeEquiv f C hf (tensorCoaction R B C θ)
    (nativeCoactionAxioms f C θ hdiag hcocycle).1
    (nativeCoactionAxioms f C θ hdiag hcocycle).2

Module documentation

From tensor-form descent isomorphisms to algebra coactions

Declarations