NYLL
Module

Algebra_DescentCofaces.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_DescentCofaces
21 declarations indexed from sourceView source ↗

Module documentation

Algebra Descent Cofaces

Imports4
  • Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
  • Mathlib.Algebra.Category.Ring.Basic
  • Mathlib.RingTheory.TensorProduct.Basic
  • Mathlib.RingTheory.TensorProduct.Maps
Imported by3

Declarations

def

compareScalarExtensions

L31 ↗
Algebra.DescentCofaces.compareScalarExtensions
Documentation

Compare two iterated scalar extensions whose composite ring maps agree.

Source context 4 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
Lean source · statement
def compareScalarExtensions
    {R S T : Type u} [CommRing R] [CommRing S] [CommRing T]
    (f : R →+* S) (g₁ g₂ : S →+* T) (h : g₁.comp f = g₂.comp f)
    (M : ModuleCat.{u} R) :
    (ModuleCat.extendScalars g₁).obj ((ModuleCat.extendScalars f).obj M) ⟶
      (ModuleCat.extendScalars g₂).obj ((ModuleCat.extendScalars f).obj M)
abbrev

R₂

L44 ↗
Algebra.DescentCofaces.R₂
Documentation

The double tensor product of the algebra, regarded as a commutative ring object.

Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
abbrev R₂ : CommRingCat.{u}
abbrev

R₃

L47 ↗
Algebra.DescentCofaces.R₃
Documentation

The triple tensor product of the algebra, regarded as a commutative ring object.

Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
abbrev R₃ : CommRingCat.{u}
def

i₁

L50 ↗
Algebra.DescentCofaces.i₁
Documentation

The inclusion into the first factor of the double tensor product.

Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
def i₁ : CommRingCat.of B ⟶ R₂ A B
def

i₂

L53 ↗
Algebra.DescentCofaces.i₂
Documentation

The inclusion into the second factor of the double tensor product.

Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
def i₂ : CommRingCat.of B ⟶ R₂ A B
def

c₁₂

L57 ↗
Algebra.DescentCofaces.c₁₂
Documentation

The map inserting one in the third factor of the triple tensor product.

Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
def c₁₂ : R₂ A B ⟶ R₃ A B
def

c₂₃

L62 ↗
Algebra.DescentCofaces.c₂₃
Documentation

The map inserting one in the first factor of the triple tensor product.

Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
def c₂₃ : R₂ A B ⟶ R₃ A B
def

c₁₃

L66 ↗
Algebra.DescentCofaces.c₁₃
Documentation

The map inserting one in the middle factor of the triple tensor product.

Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
def c₁₃ : R₂ A B ⟶ R₃ A B
theorem

i₁_apply

L70 ↗
Algebra.DescentCofaces.i₁_apply
Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem i₁_apply (b : B) : (i₁ A B).hom b = b ⊗ₜ 1
theorem

i₂_apply

L71 ↗
Algebra.DescentCofaces.i₂_apply
Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem i₂_apply (b : B) : (i₂ A B).hom b = 1 ⊗ₜ b
theorem

c₁₂_tmul

L72 ↗
Algebra.DescentCofaces.c₁₂_tmul
Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem c₁₂_tmul (b b' : B) : (c₁₂ A B).hom (b ⊗ₜ b') = b ⊗ₜ (b' ⊗ₜ 1)
theorem

c₂₃_tmul

L73 ↗
Algebra.DescentCofaces.c₂₃_tmul
Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem c₂₃_tmul (b b' : B) : (c₂₃ A B).hom (b ⊗ₜ b') = 1 ⊗ₜ (b ⊗ₜ b')
theorem

c₁₃_tmul

L74 ↗
Algebra.DescentCofaces.c₁₃_tmul
Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem c₁₃_tmul (b b' : B) : (c₁₃ A B).hom (b ⊗ₜ b') = b ⊗ₜ (1 ⊗ₜ b')
theorem

i₁_c₁₂

L76 ↗
Algebra.DescentCofaces.i₁_c₁₂
Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem i₁_c₁₂ : i₁ A B ≫ c₁₂ A B = i₁ A B ≫ c₁₃ A B
theorem

i₂_c₁₂

L77 ↗
Algebra.DescentCofaces.i₂_c₁₂
Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem i₂_c₁₂ : i₂ A B ≫ c₁₂ A B = i₁ A B ≫ c₂₃ A B
theorem

i₂_c₁₃

L78 ↗
Algebra.DescentCofaces.i₂_c₁₃
Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem i₂_c₁₃ : i₂ A B ≫ c₁₃ A B = i₂ A B ≫ c₂₃ A B
theorem

algebraMap_i₁_eq_i₂

L80 ↗
Algebra.DescentCofaces.algebraMap_i₁_eq_i₂
Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem algebraMap_i₁_eq_i₂ :
    CommRingCat.ofHom (algebraMap A B) ≫ i₁ A B = CommRingCat.ofHom (algebraMap A B) ≫ i₂ A B
theorem

i₁_comp_algebraMap_eq

L86 ↗
Algebra.DescentCofaces.i₁_comp_algebraMap_eq
Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
theorem i₁_comp_algebraMap_eq :
    (i₁ A B).hom.comp (algebraMap A B) = (i₂ A B).hom.comp (algebraMap A B)
def

canonical

L91 ↗
Algebra.DescentCofaces.canonical
Documentation

The canonical descent comparison between the two scalar extensions of a base module.

Source context 5 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
Lean source · statement
def canonical (M : ModuleCat.{u} A) :
    (ModuleCat.extendScalars (i₁ A B).hom).obj ((ModuleCat.extendScalars (algebraMap A B)).obj M) ⟶
      (ModuleCat.extendScalars (i₂ A B).hom).obj ((ModuleCat.extendScalars (algebraMap A B)).obj M)
def

T

L101 ↗
Algebra.DescentCofaces.T
Documentation

Transport a descent morphism to the triple tensor product along a coface map.

Source context 6 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
variable {A B} in
Lean source · statement
def T (N : ModuleCat.{u} B) (c : R₂ A B ⟶ R₃ A B)
    (φ' : (ModuleCat.extendScalars (i₁ A B).hom).obj N ⟶ (ModuleCat.extendScalars (i₂ A B).hom).obj
      N) :
    (ModuleCat.extendScalars (i₁ A B ≫ c).hom).obj N ⟶ (ModuleCat.extendScalars (i₂ A B ≫
      c).hom).obj N
def

Cocycle

L112 ↗
Algebra.DescentCofaces.Cocycle
Documentation

The cocycle condition for the three transported descent morphisms.

Source context 7 commands

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

universe u
open TensorProduct CategoryTheory
noncomputable section
namespace Algebra.DescentCofaces
variable (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
variable {A B} in
variable {A B} in
Lean source · statement
def Cocycle (N : ModuleCat.{u} B)
    (φ' : (ModuleCat.extendScalars (i₁ A B).hom).obj N ⟶ (ModuleCat.extendScalars (i₂ A B).hom).obj
      N) : Prop

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