Module

AdicCompletionTorsionReflection.lean

Nyll.EtaleFundamentalGroups.Purity.Local.AdicCompletionTorsionReflection

4 declarations indexed from sourceView source ↗

Module documentation

Reflecting power-torsion through adic completion

For a finitely generated ideal I, an element of \hat R \otimes_R M annihilated by I ^ n already comes from an I ^ n-annihilated element of M. This is the torsion-reflection calculation used in the mixed completion/localization equalizer.

Imports5

Nyll.EtaleFundamentalGroups.Purity.Local.AdicCompletionAnnihilatedBaseChange
Mathlib.LinearAlgebra.TensorProduct.Pi
Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Mathlib.RingTheory.Flat.Equalizer
Mathlib.RingTheory.Finiteness.Ideal

Imported by2

def

idealGeneratorAction

L34 ↗

EtaleFundamentalGroups.idealGeneratorAction

Documentation

Simultaneous multiplication by a chosen generating family of an ideal.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · full declaration

def idealGeneratorAction (J : Ideal R) :
    M →ₗ[R] (J.generators → M) where
  toFun m i := i.1 • m
  map_add' x y := by
    funext i
    exact smul_add _ _ _
  map_smul' r x := by
    funext i
    exact smul_comm _ _ _

theorem

idealGeneratorAction_mem_ker_iff

L44 ↗

EtaleFundamentalGroups.idealGeneratorAction_mem_ker_iff

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem idealGeneratorAction_mem_ker_iff
    (J : Ideal R) (m : M) :
    m ∈ LinearMap.ker (idealGeneratorAction (M := M) J) ↔
      ∀ r : J, r.1 • m = 0

theorem

idealGeneratorAction_lTensor_piRight_apply

L68 ↗

EtaleFundamentalGroups.idealGeneratorAction_lTensor_piRight_apply

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · full declaration

theorem idealGeneratorAction_lTensor_piRight_apply
    (S : Type*) [CommRing S] [Algebra R S]
    (J : Ideal R) [Fintype J.generators] [DecidableEq J.generators]
    (x : S ⊗[R] M) (i : J.generators) :
    TensorProduct.piRight R S S (fun _ : J.generators ↦ M)
        ((idealGeneratorAction (M := M) J).lTensor S x) i =
      i.1 • x := by
  classical
  induction x using TensorProduct.inductionOn with
  | add x y hx hy =>
      simpa only [map_add, smul_add, Pi.add_apply] using
        congrArg₂ (fun a b ↦ a + b) hx hy
  | tmul s m => simp [idealGeneratorAction]

theorem

adicCompletion_exists_eq_tmul_of_isTorsionBySet_pow

L84 ↗

EtaleFundamentalGroups.adicCompletion_exists_eq_tmul_of_isTorsionBySet_pow

Documentation

Power-torsion in a completed tensor product is already defined over the source. The returned source element is annihilated by the same power.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe u v
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem adicCompletion_exists_eq_tmul_of_isTorsionBySet_pow
    [IsNoetherianRing R] (I : Ideal R) (hI : I.FG) (n : ℕ)
    (x : AdicCompletion I R ⊗[R] M)
    (hx : ∀ r : (I ^ n : Ideal R), r.1 • x = 0) :
    ∃ m : M, (∀ r : (I ^ n : Ideal R), r.1 • m = 0) ∧
      x = 1 ⊗ₜ[R] m

Module documentation

Reflecting power-torsion through adic completion

Declarations

idealGeneratorAction

idealGeneratorAction_mem_ker_iff

idealGeneratorAction_lTensor_piRight_apply

adicCompletion_exists_eq_tmul_of_isTorsionBySet_pow