NYLL
Module

MaximalAdicCompletionExtOneBaseChange.lean

Nyll.EtaleFundamentalGroups.Purity.Local.MaximalAdicCompletionExtOneBaseChange
4 declarations indexed from sourceView source ↗

Module documentation

Ext¹ base change to a maximal-adic completion

Let R be a noetherian local ring and let R̂ be its completion at the maximal ideal. For a finitely presented module Q killed by a power of the maximal ideal, the canonical functorial map

Ext¹_R(Q, N) → Ext¹_R̂(R̂ ⊗ Q, R̂ ⊗ N)

is an equivalence of R-modules. The proof is the direct composite of the torsion tensor-unit equivalence with flat finite-presentation base change for Ext¹.

Imports3
Imported by1

Declarations

def

maximalAdicCompletionExtOneEquivOfLeftTorsionPow

L48 ↗
EtaleFundamentalGroups.maximalAdicCompletionExtOneEquivOfLeftTorsionPow
Documentation

The canonical Ext¹ map to the maximal-adic completion, packaged as an R-linear equivalence when its finitely presented first variable is killed by a power of the maximal ideal.

Source context 8 commands

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

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

-- Re-enable, only in this file, the functorial linear/exact structures used
-- to define the canonical map in `FinitePresentationExtOneBaseChange`.
attribute [local instance]
  moduleCatExtendScalarsLinearOverBase
  moduleCatExtendScalarsPreservesFiniteLimits
  moduleCatExtendScalarsAdditive
  extIsScalarTowerOfAlgebra
Lean source · statement
def maximalAdicCompletionExtOneEquivOfLeftTorsionPow
    (n : ℕ) (Q N : ModuleCat.{u} R) [Module.FinitePresentation R Q]
    (hQ : Module.IsTorsionBySet R Q
      ((maximalIdeal R) ^ n : Ideal R)) :
    Ext Q N 1 ≃ₗ[R]
      Ext
        ((ModuleCat.extendScalars
          (algebraMap R (AdicCompletion (maximalIdeal R) R))).obj Q)
        ((ModuleCat.extendScalars
          (algebraMap R (AdicCompletion (maximalIdeal R) R))).obj N)
        1
theorem

maximalAdicCompletionExtOneEquivOfLeftTorsionPow_apply

L65 ↗
EtaleFundamentalGroups.maximalAdicCompletionExtOneEquivOfLeftTorsionPow_apply
Source context 8 commands

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

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

-- Re-enable, only in this file, the functorial linear/exact structures used
-- to define the canonical map in `FinitePresentationExtOneBaseChange`.
attribute [local instance]
  moduleCatExtendScalarsLinearOverBase
  moduleCatExtendScalarsPreservesFiniteLimits
  moduleCatExtendScalarsAdditive
  extIsScalarTowerOfAlgebra
Lean source · statement
theorem maximalAdicCompletionExtOneEquivOfLeftTorsionPow_apply
    (n : ℕ) (Q N : ModuleCat.{u} R) [Module.FinitePresentation R Q]
    (hQ : Module.IsTorsionBySet R Q
      ((maximalIdeal R) ^ n : Ideal R)) (x : Ext Q N 1) :
    maximalAdicCompletionExtOneEquivOfLeftTorsionPow n Q N hQ x =
      (ModuleCat.extendScalars
        (algebraMap R (AdicCompletion (maximalIdeal R) R))).mapExtLinearMap
          R Q N 1 x
theorem

maximalAdicCompletionExtOneEquivOfLeftTorsionPow_toLinearMap

L77 ↗
EtaleFundamentalGroups.maximalAdicCompletionExtOneEquivOfLeftTorsionPow_toLinearMap
Documentation

The underlying linear map of the completion equivalence is exactly the canonical functorial map on Ext¹.

Source context 8 commands

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

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

-- Re-enable, only in this file, the functorial linear/exact structures used
-- to define the canonical map in `FinitePresentationExtOneBaseChange`.
attribute [local instance]
  moduleCatExtendScalarsLinearOverBase
  moduleCatExtendScalarsPreservesFiniteLimits
  moduleCatExtendScalarsAdditive
  extIsScalarTowerOfAlgebra
Lean source · statement
theorem maximalAdicCompletionExtOneEquivOfLeftTorsionPow_toLinearMap
    (n : ℕ) (Q N : ModuleCat.{u} R) [Module.FinitePresentation R Q]
    (hQ : Module.IsTorsionBySet R Q
      ((maximalIdeal R) ^ n : Ideal R)) :
    (maximalAdicCompletionExtOneEquivOfLeftTorsionPow n Q N hQ).toLinearMap =
      (ModuleCat.extendScalars
        (algebraMap R (AdicCompletion (maximalIdeal R) R))).mapExtLinearMap
          R Q N 1
theorem

maximalAdicCompletion_mapExtOne_bijective_of_left_torsionPow

L89 ↗
EtaleFundamentalGroups.maximalAdicCompletion_mapExtOne_bijective_of_left_torsionPow
Documentation

In particular, the canonical map on Ext¹ is bijective.

Source context 8 commands

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

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

-- Re-enable, only in this file, the functorial linear/exact structures used
-- to define the canonical map in `FinitePresentationExtOneBaseChange`.
attribute [local instance]
  moduleCatExtendScalarsLinearOverBase
  moduleCatExtendScalarsPreservesFiniteLimits
  moduleCatExtendScalarsAdditive
  extIsScalarTowerOfAlgebra
Lean source · statement
theorem maximalAdicCompletion_mapExtOne_bijective_of_left_torsionPow
    (n : ℕ) (Q N : ModuleCat.{u} R) [Module.FinitePresentation R Q]
    (hQ : Module.IsTorsionBySet R Q
      ((maximalIdeal R) ^ n : Ideal R)) :
    Function.Bijective
      ((ModuleCat.extendScalars
        (algebraMap R (AdicCompletion (maximalIdeal R) R))).mapExtLinearMap
          R Q N 1)

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