Module

MaximalAdicCompletionModuleHomDescent.lean

Nyll.EtaleFundamentalGroups.Purity.Local.MaximalAdicCompletionModuleHomDescent

2 declarations indexed from sourceView source ↗

Module documentation

Hom descent along maximal-adic completion

This specializes faithfully flat Hom descent to the completion map of a Noetherian local ring. It is the full-faithfulness input for module formal gluing at the closed point.

Imports2

Imported by1

Nyll.EtaleFundamentalGroups.Purity.Local.All

def

maximalAdicCompletionModuleHomDescentEquiv

L29 ↗

EtaleFundamentalGroups.maximalAdicCompletionModuleHomDescentEquiv

Documentation

Linear maps over a Noetherian local ring are exactly the compatible maps between their maximal-adic completions.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open scoped TensorProduct
universe u v w

Lean source · statement

def maximalAdicCompletionModuleHomDescentEquiv
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (M : Type v) [AddCommGroup M] [Module R M]
    (N : Type w) [AddCommGroup N] [Module R N] :
    (M →ₗ[R] N) ≃ₗ[R]
      tensorProductDescentCompatibleLinearMaps
        (R := R) (S := AdicCompletion (maximalIdeal R) R)
        (M := M) (N := N)

theorem

maximalAdicCompletionModuleHomDescentEquiv_apply

L43 ↗

EtaleFundamentalGroups.maximalAdicCompletionModuleHomDescentEquiv_apply