NYLL
Module

PrincipalLocalizationTensorCoefficients.lean

Nyll.EtaleFundamentalGroups.Purity.PrincipalLocalizationTensorCoefficients
4 declarations indexed from sourceView source ↗

Module documentation

Tensor coefficients for the principal localization complex

The usual tensor description of module localization identifies tensoring the ring's principal localization complex with the principal complex of the coefficient module. Compatibility with the differential is checked on pure tensors using the actual localization maps.

Imports6
Imported by3

Declarations

def

tensorLocalizedRingEquiv

L34 ↗
EtaleFundamentalGroups.Purity.tensorLocalizedRingEquiv
Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits MonoidalCategory
open scoped TensorProduct
variable {R : Type u} [CommRing R]
Lean source · statement
def tensorLocalizedRingEquiv (S : Submonoid R) (M : ModuleCat.{u} R) :
    M ⊗[R] LocalizedModule S R ≃ₗ[R] LocalizedModule S M
theorem

tensorLocalizedRingEquiv_mk

L42 ↗
EtaleFundamentalGroups.Purity.tensorLocalizedRingEquiv_mk
Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits MonoidalCategory
open scoped TensorProduct
variable {R : Type u} [CommRing R]
Lean source · statement
theorem tensorLocalizedRingEquiv_mk (S : Submonoid R)
    (M : ModuleCat.{u} R) (m : M) (r : R) :
    tensorLocalizedRingEquiv S M
      (m ⊗ₜ[R] LocalizedModule.mkLinearMap S R r) =
        LocalizedModule.mkLinearMap S M (r • m)
def

principalTensorCoefficientXIso

L60 ↗
EtaleFundamentalGroups.Purity.principalTensorCoefficientXIso
Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits MonoidalCategory
open scoped TensorProduct
variable {R : Type u} [CommRing R]
Lean source · full declaration
def principalTensorCoefficientXIso (x : R) (M : ModuleCat.{u} R) :
    ∀ n : ℕ,
      (((tensorLeft M).mapHomologicalComplex (ComplexShape.up ℕ)).obj
        (principalLocalizationComplex x (ModuleCat.of R R))).X n ≅
          (principalLocalizationComplex x M).X n
  | 0 => ρ_ M
  | 1 => (tensorLocalizedRingEquiv (Submonoid.powers x) M).toModuleIso
  | n + 2 =>
    ((tensorLeft M).map_isZero
      (principalLocalizationComplex_isZero_X x (ModuleCat.of R R) (n + 2) (by omega))).iso
      (principalLocalizationComplex_isZero_X x M (n + 2) (by omega))
def

principalLocalizationTensorCoefficientsIso

L74 ↗
EtaleFundamentalGroups.Purity.principalLocalizationTensorCoefficientsIso
Documentation

Tensoring the principal complex of the ring with a coefficient module gives its actual principal localization complex.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits MonoidalCategory
open scoped TensorProduct
variable {R : Type u} [CommRing R]
Lean source · statement
def principalLocalizationTensorCoefficientsIso (x : R) (M : ModuleCat.{u} R) :
    ((tensorLeft M).mapHomologicalComplex (ComplexShape.up ℕ)).obj
      (principalLocalizationComplex x (ModuleCat.of R R)) ≅
        principalLocalizationComplex x M

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