Module

ModuleKernelLocalization.lean

Nyll.SchemeTheory.RingTheory.ModuleKernelLocalization

5 declarations indexed from sourceView source ↗

Module documentation

Localization of the actual kernel map in a commutative square

The native localization theorem identifies the kernel of the universal localized arrow with the localization of the original kernel. Here the lower arrow is the one supplied by an actual commutative square. Its universal property identifies it with that native arrow, so restriction of the vertical map to the two kernels is itself a localization.

This is the module-level kernel supplier for the quasicoherent extension construction in Stacks, Tag 01PE. It adds no kernel-comparison premise and does not yet assert a sheaf-extension or relative approximation theorem.

Imports4

Mathlib.Algebra.Module.LocalizedModule.Basic
Mathlib.Algebra.Module.LocalizedModule.Submodule
Mathlib.Algebra.Module.Submodule.Ker
Mathlib.Algebra.Module.Submodule.LinearMap

Imported by2

theorem

mapsTo_ker_of_comp_eq

L32 ↗

LinearMap.mapsTo_ker_of_comp_eq

Source context 3 commands

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

noncomputable section
universe u v₁ v₂ v₃ v₄
namespace LinearMap

Lean source · statement

theorem mapsTo_ker_of_comp_eq
    {R : Type u} [CommRing R]
    {M : Type v₁} [AddCommGroup M] [Module R M]
    {M' : Type v₂} [AddCommGroup M'] [Module R M']
    {N : Type v₃} [AddCommGroup N] [Module R N]
    {N' : Type v₄} [AddCommGroup N'] [Module R N']
    (f : M →ₗ[R] M') (g : N →ₗ[R] N')
    (φ : M →ₗ[R] N) (ψ : M' →ₗ[R] N')
    (h : ψ.comp f = g.comp φ) :
    ∀ x ∈ φ.ker, f x ∈ ψ.ker

def

kernelRestriction

L48 ↗

LinearMap.kernelRestriction

Documentation

The restriction of the left vertical arrow to the kernels of the two horizontal arrows of an actual commutative square.

Source context 3 commands

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

noncomputable section
universe u v₁ v₂ v₃ v₄
namespace LinearMap

Lean source · statement

def kernelRestriction
    {R : Type u} [CommRing R]
    {M : Type v₁} [AddCommGroup M] [Module R M]
    {M' : Type v₂} [AddCommGroup M'] [Module R M']
    {N : Type v₃} [AddCommGroup N] [Module R N]
    {N' : Type v₄} [AddCommGroup N'] [Module R N']
    (f : M →ₗ[R] M') (g : N →ₗ[R] N')
    (φ : M →ₗ[R] N) (ψ : M' →ₗ[R] N')
    (h : ψ.comp f = g.comp φ) : φ.ker →ₗ[R] ψ.ker

theorem

isLocalizedModule_restrict_of_localized₀_eq

L59 ↗

LinearMap.isLocalizedModule_restrict_of_localized₀_eq

Source context 3 commands

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

noncomputable section
universe u v₁ v₂ v₃ v₄
namespace LinearMap

Lean source · statement

theorem isLocalizedModule_restrict_of_localized₀_eq
    {R : Type u} [CommRing R]
    {M : Type v₁} [AddCommGroup M] [Module R M]
    {M' : Type v₂} [AddCommGroup M'] [Module R M']
    (S : Submonoid R) (f : M →ₗ[R] M') [IsLocalizedModule S f]
    (K : Submodule R M) (L : Submodule R M')
    (hf : ∀ x ∈ K, f x ∈ L) (h : K.localized₀ S f = L) :
    IsLocalizedModule S (f.restrict hf)

theorem

localized₀_ker_eq_of_comp_eq

L70 ↗

LinearMap.localized₀_ker_eq_of_comp_eq

Source context 3 commands

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

noncomputable section
universe u v₁ v₂ v₃ v₄
namespace LinearMap

Lean source · statement

theorem localized₀_ker_eq_of_comp_eq
    {R : Type u} [CommRing R]
    {M : Type v₁} [AddCommGroup M] [Module R M]
    {M' : Type v₂} [AddCommGroup M'] [Module R M']
    {N : Type v₃} [AddCommGroup N] [Module R N]
    {N' : Type v₄} [AddCommGroup N'] [Module R N']
    (S : Submonoid R)
    (f : M →ₗ[R] M') [IsLocalizedModule S f]
    (g : N →ₗ[R] N') [IsLocalizedModule S g]
    (φ : M →ₗ[R] N) (ψ : M' →ₗ[R] N')
    (h : ψ.comp f = g.comp φ) :
    φ.ker.localized₀ S f = ψ.ker

theorem

isLocalizedModule_kernelRestriction

L90 ↗

LinearMap.isLocalizedModule_kernelRestriction

Documentation

If both vertical arrows of a commutative square are localizations, the actual restriction map between the kernels is a localization too.

Source context 3 commands

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

noncomputable section
universe u v₁ v₂ v₃ v₄
namespace LinearMap

Lean source · statement

theorem isLocalizedModule_kernelRestriction
    {R : Type u} [CommRing R]
    {M : Type v₁} [AddCommGroup M] [Module R M]
    {M' : Type v₂} [AddCommGroup M'] [Module R M']
    {N : Type v₃} [AddCommGroup N] [Module R N]
    {N' : Type v₄} [AddCommGroup N'] [Module R N']
    (S : Submonoid R)
    (f : M →ₗ[R] M') [IsLocalizedModule S f]
    (g : N →ₗ[R] N') [IsLocalizedModule S g]
    (φ : M →ₗ[R] N) (ψ : M' →ₗ[R] N')
    (h : ψ.comp f = g.comp φ) :
    IsLocalizedModule S (kernelRestriction f g φ ψ h)

Module documentation

Localization of the actual kernel map in a commutative square

Declarations

mapsTo_ker_of_comp_eq

kernelRestriction

isLocalizedModule_restrict_of_localized₀_eq

localized₀_ker_eq_of_comp_eq

isLocalizedModule_kernelRestriction