NYLL
Module

TensorDualComplexTorsionLifting.lean

Nyll.EtaleFundamentalGroups.Purity.TensorDualComplexTorsionLifting
2 declarations indexed from sourceView source ↗

Module documentation

Degree-zero tensor vanishing and dual torsion lifting

Vanishing of degree-zero homology after tensoring with ideal quotients makes every map from those quotients into the degree-zero dual lift to degree one. Cofinality then gives surjectivity of the differential on ideal-power torsion. This is the base of the injective-chain argument.

Imports9
Imported by2

Declarations

theorem

surjective_chain_d_zero_of_isZero_homology

L34 ↗
EtaleFundamentalGroups.Purity.surjective_chain_d_zero_of_isZero_homology
Source context 4 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits Opposite MonoidalCategory
variable {R : Type u} [CommRing R]
Lean source · statement
theorem surjective_chain_d_zero_of_isZero_homology
    (K : ChainComplex (ModuleCat.{u} R) ℕ) (h : IsZero (K.homology 0)) :
    Function.Surjective (K.d 1 0)
theorem

idealPowerTorsion_dual_d_surjective_of_tensor_zero

L48 ↗
EtaleFundamentalGroups.Purity.idealPowerTorsion_dual_d_surjective_of_tensor_zero
Documentation

Tensor vanishing over a cofinal ideal family supplies the degree-zero surjectivity of the power-torsion dual complex.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits Opposite MonoidalCategory
variable {R : Type u} [CommRing R]
Lean source · statement
theorem idealPowerTorsion_dual_d_surjective_of_tensor_zero
    (I : Ideal R) (J : ℕ → Ideal R)
    (hJI : ∀ n : ℕ, ∃ m : ℕ, J m ≤ I ^ n)
    (hIJ : ∀ m : ℕ, ∃ n : ℕ, I ^ n ≤ J m)
    (E : ModuleCat.{u} R) [Module.Injective R E]
    (C : CochainComplex (ModuleCat.{u} R) ℕ)
    (hzero : ∀ m : ℕ, IsZero
      ((((tensorLeft (ModuleCat.of R (R ⧸ J m))).mapHomologicalComplex
        (ComplexShape.up ℕ)).obj C).homology 0)) :
    Function.Surjective
      ((idealPowerTorsionFunctor I).map ((linearDualComplex E C).d 1 0))

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