NYLL
Module

CechInjectiveDegreeZero.lean

Nyll.EtaleFundamentalGroups.Purity.CechInjectiveDegreeZero
11 declarations indexed from sourceView source ↗

Module documentation

Degree-zero maps in the injective Čech contraction

The degree-zero map of the injective Čech contraction is identified with the canonical torsion inclusion using the tensor coefficient comparisons.

Imports14
Imported by2

Declarations

theorem

singleTensorComplexIso_hom_f_zero

L40 ↗
EtaleFundamentalGroups.Purity.singleTensorComplexIso_hom_f_zero
Documentation

The coefficient comparison inserts the unique zero-degree summand.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem singleTensorComplexIso_hom_f_zero (M : ModuleCat.{u} R)
    (K : CochainComplex (ModuleCat.{u} R) ℕ) :
    (singleTensorComplexIso M K).hom.f 0 =
      (tensorComplexZeroIso ((CochainComplex.single₀ (ModuleCat.{u} R)).obj M) K).hom
theorem

singleTensorComplexIso_inv_f_zero

L55 ↗
EtaleFundamentalGroups.Purity.singleTensorComplexIso_inv_f_zero
Documentation

The inverse coefficient comparison projects the unique zero-degree summand.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem singleTensorComplexIso_inv_f_zero (M : ModuleCat.{u} R)
    (K : CochainComplex (ModuleCat.{u} R) ℕ) :
    (singleTensorComplexIso M K).inv.f 0 =
      (tensorComplexZeroIso ((CochainComplex.single₀ (ModuleCat.{u} R)).obj M) K).inv
theorem

principalLocalizationTensorCoefficientsIso_inv_f_zero

L66 ↗
EtaleFundamentalGroups.Purity.principalLocalizationTensorCoefficientsIso_inv_f_zero
Documentation

The principal coefficient comparison is the right unitor in degree zero.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem principalLocalizationTensorCoefficientsIso_inv_f_zero
    (x : R) (M : ModuleCat.{u} R) :
    (principalLocalizationTensorCoefficientsIso x M).inv.f 0 = (ρ_ M).inv
theorem

tensorComplexZeroIso_hom_naturality

L72 ↗
EtaleFundamentalGroups.Purity.tensorComplexZeroIso_hom_naturality
Documentation

Tensor maps act on the unique degree-zero summand by their two zeroth components.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem tensorComplexZeroIso_hom_naturality
    {K L K' L' : CochainComplex (ModuleCat.{u} R) ℕ} (f : K ⟶ K') (g : L ⟶ L') :
    (tensorComplexZeroIso K L).hom ≫ (HomologicalComplex.tensorHom f g).f 0 =
      (f.f 0 ⊗ₘ g.f 0) ≫ (tensorComplexZeroIso K' L').hom
theorem

tensorComplexZeroIso_inv_naturality

L87 ↗
EtaleFundamentalGroups.Purity.tensorComplexZeroIso_inv_naturality
Documentation

The inverse degree-zero identification also commutes with tensor maps.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem tensorComplexZeroIso_inv_naturality
    {K L K' L' : CochainComplex (ModuleCat.{u} R) ℕ} (f : K ⟶ K') (g : L ⟶ L') :
    (HomologicalComplex.tensorHom f g).f 0 ≫ (tensorComplexZeroIso K' L').inv =
      (tensorComplexZeroIso K L).inv ≫ (f.f 0 ⊗ₘ g.f 0)
theorem

tensorComplexZeroIso_associator_hom

L98 ↗
EtaleFundamentalGroups.Purity.tensorComplexZeroIso_associator_hom
Documentation

The associator on complexes is the usual tensor associator on the unique summands in degree zero.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem tensorComplexZeroIso_associator_hom
    (K L B : CochainComplex (ModuleCat.{u} R) ℕ) :
    ((tensorComplexZeroIso K L).hom ▷ B.X 0) ≫
      (tensorComplexZeroIso (HomologicalComplex.tensorObj K L) B).hom ≫
      (HomologicalComplex.associator K L B).hom.f 0 =
    (α_ (K.X 0) (L.X 0) (B.X 0)).hom ≫
      (K.X 0 ◁ (tensorComplexZeroIso L B).hom) ≫
      (tensorComplexZeroIso K (HomologicalComplex.tensorObj L B)).hom
theorem

tensorComplexZeroIso_associator_hom_normalized

L119 ↗
EtaleFundamentalGroups.Purity.tensorComplexZeroIso_associator_hom_normalized
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem tensorComplexZeroIso_associator_hom_normalized
    (K L B : CochainComplex (ModuleCat.{u} R) ℕ) :
    (tensorComplexZeroIso (HomologicalComplex.tensorObj K L) B).hom ≫
      (HomologicalComplex.associator K L B).hom.f 0 ≫
      (tensorComplexZeroIso K (HomologicalComplex.tensorObj L B)).inv =
    ((tensorComplexZeroIso K L).inv ▷ B.X 0) ≫
      (α_ (K.X 0) (L.X 0) (B.X 0)).hom ≫
      (K.X 0 ◁ (tensorComplexZeroIso L B).hom)
theorem

tensorComplexZeroIso_tensor_associator

L134 ↗
EtaleFundamentalGroups.Purity.tensorComplexZeroIso_tensor_associator
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem tensorComplexZeroIso_tensor_associator
    (K K' L B : CochainComplex (ModuleCat.{u} R) ℕ)
    (f : K ⟶ HomologicalComplex.tensorObj K' L) :
    (tensorComplexZeroIso K B).hom ≫
      (HomologicalComplex.tensorHom f (𝟙 B)).f 0 ≫
      (HomologicalComplex.associator K' L B).hom.f 0 ≫
      (tensorComplexZeroIso K' (HomologicalComplex.tensorObj L B)).inv =
    (f.f 0 ▷ B.X 0) ≫ ((tensorComplexZeroIso K' L).inv ▷ B.X 0) ≫
      (α_ (K'.X 0) (L.X 0) (B.X 0)).hom ≫
      (K'.X 0 ◁ (tensorComplexZeroIso L B).hom)
theorem

zeroTensorModuleCompatibility

L148 ↗
EtaleFundamentalGroups.Purity.zeroTensorModuleCompatibility
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem zeroTensorModuleCompatibility
    (M T B Y Z : ModuleCat.{u} R) (i : T ⟶ M) (f : T ⟶ Y)
    (u : M ⊗ ModuleCat.of R R ≅ Y) (v : ModuleCat.of R R ⊗ B ≅ Z)
    (b : B ⟶ ModuleCat.of R R) (hf : f = i ≫ (ρ_ M).inv ≫ u.hom) :
    ((f ▷ B) ≫ (u.inv ▷ B) ≫ (α_ M (ModuleCat.of R R) B).hom ≫ (M ◁ v.hom)) ≫
      ((M ◁ (v.inv ≫ (ModuleCat.of R R ◁ b) ≫ (λ_ (ModuleCat.of R R)).hom)) ≫
        (ρ_ M).hom) = ((T ◁ b) ≫ (ρ_ T).hom) ≫ i
theorem

cechPrincipalTensor_zero

L173 ↗
EtaleFundamentalGroups.Purity.cechPrincipalTensor_zero
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem cechPrincipalTensor_zero (x : R) (xs : List R) (M T : ModuleCat.{u} R) (i : T ⟶ M)
    (f : (CochainComplex.single₀ (ModuleCat.{u} R)).obj T ⟶
      HomologicalComplex.tensorObj ((CochainComplex.single₀ (ModuleCat.{u} R)).obj M)
        (principalLocalizationComplex x (ModuleCat.of R R)))
    (hf : f.f 0 = i ≫ (ρ_ M).inv ≫
      (tensorComplexZeroIso ((CochainComplex.single₀ (ModuleCat.{u} R)).obj M)
        (principalLocalizationComplex x (ModuleCat.of R R))).hom) :
    (singleTensorComplexIso T (cechLocalizationComplex xs)).hom.f 0 ≫
      (HomologicalComplex.tensorHom f (𝟙 (cechLocalizationComplex xs))).f 0 ≫
      (HomologicalComplex.associator
        ((CochainComplex.single₀ (ModuleCat.{u} R)).obj M)
        (principalLocalizationComplex x (ModuleCat.of R R))
        (cechLocalizationComplex xs)).hom.f 0 ≫
      (singleTensorComplexIso M (cechLocalizationComplex (x :: xs))).inv.f 0 ≫
      (cechCoefficientZeroIso (x :: xs) M).hom =
    (cechCoefficientZeroIso xs T).hom ≫ i
theorem

cechInjectiveHomotopyEquiv_inv_f_zero

L237 ↗
EtaleFundamentalGroups.Purity.cechInjectiveHomotopyEquiv_inv_f_zero
Documentation

The injection in the Čech contraction is the canonical torsion inclusion under the degree-zero coefficient identification.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem cechInjectiveHomotopyEquiv_inv_f_zero [IsNoetherianRing R]
    (xs : List R) (M : ModuleCat.{u} R) [Module.Injective R M] :
    (cechInjectiveHomotopyEquiv xs M).inv.f 0 ≫
      (cechCoefficientZeroIso xs M).hom =
    ModuleCat.ofHom (Ideal.primaryComponent M (Ideal.ofList xs)).subtype

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