Module

AdicCompletionAnnihilatedBaseChange.lean

Nyll.EtaleFundamentalGroups.Purity.Local.AdicCompletionAnnihilatedBaseChange

8 declarations indexed from sourceView source ↗

Module documentation

Base change of modules annihilated by the adic ideal

The first, torsion-level input to formal gluing is that extension of scalars from a ring to its adic completion does not change a module annihilated by the adic ideal. The proof uses the closed-fibre comparison and is valid without assuming that the original ring is complete.

Imports3

Nyll.EtaleFundamentalGroups.Purity.Local.AdicCompletionQuotient
Mathlib.Algebra.Module.Torsion.Basic
Mathlib.LinearAlgebra.TensorProduct.Quotient

Imported by3

theorem

adicCompletion_tmul_eq_zero_of_mem_map

L34 ↗

EtaleFundamentalGroups.adicCompletion_tmul_eq_zero_of_mem_map

Documentation

An element of the extended ideal tensors to zero against a module annihilated by the original ideal.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u v
open scoped TensorProduct
variable {R : Type u} [CommRing R]
variable (I : Ideal R) (hI : I.FG)
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem adicCompletion_tmul_eq_zero_of_mem_map
    (hM : Module.IsTorsionBySet R M I)
    {x : AdicCompletion I R}
    (hx : x ∈ I.map (algebraMap R (AdicCompletion I R))) (m : M) :
    x ⊗ₜ[R] m = 0

theorem

adicCompletion_tensorProduct_mk_bijective_of_isTorsionBySet

L54 ↗

EtaleFundamentalGroups.adicCompletion_tensorProduct_mk_bijective_of_isTorsionBySet

Documentation

If M is annihilated by I, then the canonical base-change map M → Â ⊗[R] M is bijective.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u v
open scoped TensorProduct
variable {R : Type u} [CommRing R]
variable (I : Ideal R) (hI : I.FG)
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem adicCompletion_tensorProduct_mk_bijective_of_isTorsionBySet
    (hI : I.FG)
    (hM : Module.IsTorsionBySet R M I) :
    Function.Bijective
      (TensorProduct.mk R (AdicCompletion I R) M 1)

def

adicCompletionTensorEquivOfIsTorsionBySet

L106 ↗

EtaleFundamentalGroups.adicCompletionTensorEquivOfIsTorsionBySet

Documentation

The canonical linear equivalence furnished by base change for an I-annihilated module.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u v
open scoped TensorProduct
variable {R : Type u} [CommRing R]
variable (I : Ideal R) (hI : I.FG)
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

def adicCompletionTensorEquivOfIsTorsionBySet
    (hI : I.FG)
    (hM : Module.IsTorsionBySet R M I) :
    M ≃ₗ[R] AdicCompletion I R ⊗[R] M

theorem

adicCompletionTensorEquivOfIsTorsionBySet_apply

L115 ↗

EtaleFundamentalGroups.adicCompletionTensorEquivOfIsTorsionBySet_apply

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u v
open scoped TensorProduct
variable {R : Type u} [CommRing R]
variable (I : Ideal R) (hI : I.FG)
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem adicCompletionTensorEquivOfIsTorsionBySet_apply
    (hI : I.FG)
    (hM : Module.IsTorsionBySet R M I) (m : M) :
    adicCompletionTensorEquivOfIsTorsionBySet I hI hM m = 1 ⊗ₜ[R] m

theorem

adicCompletion_tmul_eq_zero_of_mem_map_pow

L124 ↗

EtaleFundamentalGroups.adicCompletion_tmul_eq_zero_of_mem_map_pow

Documentation

An element of the extension of I ^ n tensors to zero against a module annihilated by I ^ n, while the completion remains the I-adic completion.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u v
open scoped TensorProduct
variable {R : Type u} [CommRing R]
variable (I : Ideal R) (hI : I.FG)
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem adicCompletion_tmul_eq_zero_of_mem_map_pow
    (n : ℕ) (hM : Module.IsTorsionBySet R M (I ^ n : Ideal R))
    {x : AdicCompletion I R}
    (hx : x ∈ (I ^ n).map (algebraMap R (AdicCompletion I R))) (m : M) :
    x ⊗ₜ[R] m = 0

theorem

adicCompletion_tensorProduct_mk_bijective_of_isTorsionBySet_pow

L144 ↗

EtaleFundamentalGroups.adicCompletion_tensorProduct_mk_bijective_of_isTorsionBySet_pow

Documentation

If M is annihilated by I ^ n, then the canonical map to its base change along the I-adic completion is bijective.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u v
open scoped TensorProduct
variable {R : Type u} [CommRing R]
variable (I : Ideal R) (hI : I.FG)
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem adicCompletion_tensorProduct_mk_bijective_of_isTorsionBySet_pow
    (hI : I.FG) (n : ℕ)
    (hM : Module.IsTorsionBySet R M (I ^ n : Ideal R)) :
    Function.Bijective
      (TensorProduct.mk R (AdicCompletion I R) M 1)

def

adicCompletionTensorEquivOfIsTorsionBySetPow

L198 ↗

EtaleFundamentalGroups.adicCompletionTensorEquivOfIsTorsionBySetPow

Documentation

The canonical linear equivalence for a module annihilated by a power of the adic ideal.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u v
open scoped TensorProduct
variable {R : Type u} [CommRing R]
variable (I : Ideal R) (hI : I.FG)
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

def adicCompletionTensorEquivOfIsTorsionBySetPow
    (hI : I.FG) (n : ℕ)
    (hM : Module.IsTorsionBySet R M (I ^ n : Ideal R)) :
    M ≃ₗ[R] AdicCompletion I R ⊗[R] M

theorem

adicCompletionTensorEquivOfIsTorsionBySetPow_apply

L208 ↗

EtaleFundamentalGroups.adicCompletionTensorEquivOfIsTorsionBySetPow_apply

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u v
open scoped TensorProduct
variable {R : Type u} [CommRing R]
variable (I : Ideal R) (hI : I.FG)
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem adicCompletionTensorEquivOfIsTorsionBySetPow_apply
    (hI : I.FG) (n : ℕ)
    (hM : Module.IsTorsionBySet R M (I ^ n : Ideal R)) (m : M) :
    adicCompletionTensorEquivOfIsTorsionBySetPow I hI n hM m =
      1 ⊗ₜ[R] m

Module documentation

Base change of modules annihilated by the adic ideal

Declarations