NYLL
Module

LocalizationCriteria.lean

Nyll.SchemeTheory.Modules.LocalizationCriteria
2 declarations indexed from sourceView source ↗

Module documentation

Native module localization criteria

Constructs localization from the actual invertibility, fraction and kernel criteria.

Imports6
  • Mathlib.Algebra.Category.ModuleCat.Basic
  • Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
  • Mathlib.Algebra.Category.Ring.Basic
  • Mathlib.Algebra.Module.LocalizedModule.Away
  • Mathlib.Algebra.Module.Equiv.Basic
  • Mathlib.Algebra.Group.Action.Basic
Imported by1

Declarations

theorem

isLocalizedModuleAway_of_criteria

L30 ↗
ModuleCat.isLocalizedModuleAway_of_criteria
Documentation

The native module localization constructor with its three actual criteria. This keeps the endomorphism-ring unit conversion in its algebraic owner.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory
namespace ModuleCat
Lean source · full declaration
theorem isLocalizedModuleAway_of_criteria (R : CommRingCat.{u})
    (M N : ModuleCat.{v} R) (f : M ⟶ N) (r : R)
    (hunit : Function.Bijective (fun x : N => r • x))
    (hsurj : ∀ x : N, ∃ (n : ℕ) (y : M), f.hom y = r ^ n • x)
    (hker : ∀ y : M, f.hom y = 0 → ∃ n : ℕ, r ^ n • y = 0) :
    IsLocalizedModule.Away r f.hom := by
  apply IsLocalizedModule.Away.mk_of_addCommGroup
  · rw [Module.End.isUnit_iff]
    exact hunit
  · intro x
    obtain ⟨n, y, hy⟩ := hsurj x
    exact ⟨n, y, hy.symm⟩
  · exact hker
theorem

restrictScalars_smul_bijective_of_isUnit

L46 ↗
ModuleCat.restrictScalars_smul_bijective_of_isUnit
Documentation

A unit in the coefficient ring acts bijectively on the actual module obtained by native restriction of scalars. No new action is installed.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory
namespace ModuleCat
Lean source · full declaration
theorem restrictScalars_smul_bijective_of_isUnit (R A : CommRingCat.{u})
    (σ : R →+* A) (N : ModuleCat.{v} A) (r : R) (hr : IsUnit (σ r)) :
    Function.Bijective (fun x : (ModuleCat.restrictScalars σ).obj N => r • x) := by
  have hfun : (fun x : (ModuleCat.restrictScalars σ).obj N => r • x) =
      (fun x : (ModuleCat.restrictScalars σ).obj N =>
        (show A from σ r) • (show N from x)) := by
    funext x
    exact ModuleCat.restrictScalars.smul_def σ r x
  rw [hfun]
  exact hr.smul_bijective (β := N)

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