Module

MaximalAdicCompletionExtTorsion.lean

Nyll.EtaleFundamentalGroups.Purity.Local.MaximalAdicCompletionExtTorsion

3 declarations indexed from sourceView source ↗

Module documentation

Torsion input for maximal-adic Ext base change

The completion comparison for Ext¹ starts with a finite module killed by a power of the adic ideal. This file records the two elementary facts needed before the flat base-change argument: the same ideal power annihilates every Ext group with that module in the first variable, and hence the canonical tensor unit into the adic completion is an equivalence on that Ext group.

Imports2

Nyll.EtaleFundamentalGroups.Purity.Local.AdicCompletionAnnihilatedBaseChange
Mathlib.Algebra.Category.ModuleCat.Ext.Basic

Imported by2

theorem

ext_isTorsionBySet_of_left

L33 ↗

EtaleFundamentalGroups.ext_isTorsionBySet_of_left

Documentation

An annihilator of the first variable annihilates the corresponding Ext group.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u v
open CategoryTheory CategoryTheory.Abelian
open scoped TensorProduct
variable {R : Type u} [CommRing R] [Small.{v} R]

Lean source · statement

theorem ext_isTorsionBySet_of_left
    {Q N : ModuleCat.{v} R} {s : Set R}
    (hQ : Module.IsTorsionBySet R Q s) (i : ℕ) :
    Module.IsTorsionBySet R (Ext Q N i) s

def

adicCompletionExtTensorEquivOfLeftTorsionPow

L47 ↗

EtaleFundamentalGroups.adicCompletionExtTensorEquivOfLeftTorsionPow

Documentation

If the first variable is killed by I ^ n, then completion does not change its Ext group at the tensor-unit stage.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u v
open CategoryTheory CategoryTheory.Abelian
open scoped TensorProduct
variable {R : Type u} [CommRing R] [Small.{v} R]

Lean source · statement

def adicCompletionExtTensorEquivOfLeftTorsionPow
    (I : Ideal R) (hI : I.FG) (n : ℕ)
    {Q N : ModuleCat.{v} R}
    (hQ : Module.IsTorsionBySet R Q (I ^ n : Ideal R)) (i : ℕ) :
    Ext Q N i ≃ₗ[R]
      (AdicCompletion I R ⊗[R] Ext Q N i)

theorem

adicCompletionExtTensorEquivOfLeftTorsionPow_apply

L57 ↗

EtaleFundamentalGroups.adicCompletionExtTensorEquivOfLeftTorsionPow_apply

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u v
open CategoryTheory CategoryTheory.Abelian
open scoped TensorProduct
variable {R : Type u} [CommRing R] [Small.{v} R]

Lean source · statement

theorem adicCompletionExtTensorEquivOfLeftTorsionPow_apply
    (I : Ideal R) (hI : I.FG) (n : ℕ)
    {Q N : ModuleCat.{v} R}
    (hQ : Module.IsTorsionBySet R Q (I ^ n : Ideal R)) (i : ℕ)
    (x : Ext Q N i) :
    adicCompletionExtTensorEquivOfLeftTorsionPow I hI n hQ i x =
      1 ⊗ₜ[R] x

Module documentation

Torsion input for maximal-adic Ext base change

Declarations

ext_isTorsionBySet_of_left

adicCompletionExtTensorEquivOfLeftTorsionPow

adicCompletionExtTensorEquivOfLeftTorsionPow_apply