Module

PrimeAwayTensorDetection.lean

Nyll.SchemeTheory.RingTheory.Descent.PrimeAwayTensorDetection

3 declarations indexed from sourceView source ↗

Module documentation

Detecting an isomorphism on two principal opens

A map from a flat module is an isomorphism if it becomes an isomorphism at two prime-away localizations and the first parameter acts injectively on the target. The source's flat Hartogs equalizer constructs preimages.

Imports7

Nyll.SchemeTheory.RingTheory.Descent.PrimeAwayPairGluing
Mathlib.Algebra.Module.LocalizedModule.Basic
Mathlib.Algebra.Module.Torsion.Free
Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.Flat.Localization
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.RingTheory.Localization.Away.Basic

Imported by2

theorem

tmul_one_injective_of_isTorsionFree

L34 ↗

SchemeTheory.tmul_one_injective_of_isTorsionFree

Documentation

Localization of a torsion-free module embeds the module into its tensor extension, with the localization factor written on the right.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct nonZeroDivisors
universe u v w w'

Lean source · full declaration

theorem tmul_one_injective_of_isTorsionFree
    {R : Type u} [CommRing R] [IsDomain R]
    (A : Type v) [CommRing A] [Algebra R A]
    (T : Submonoid R) [IsLocalization T A] (hT : T ≤ nonZeroDivisors R)
    (M : Type w) [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] :
    Function.Injective (fun m : M => m ⊗ₜ[R] (1 : A)) := by
  have hleft : Function.Injective (TensorProduct.mk R A M 1) := by
    apply (IsLocalizedModule.injective_iff_isRegular T _).mpr
    intro t
    exact IsSMulRegular.of_ne_zero (mem_nonZeroDivisors_iff_ne_zero.mp (hT t.2))
  intro m n hmn
  apply hleft
  change (1 : A) ⊗ₜ[R] m = (1 : A) ⊗ₜ[R] n
  have h := congrArg (TensorProduct.comm R M A) hmn
  simpa only [TensorProduct.comm_tmul] using h

theorem

rTensor_surjective_of_pow_smul_mem_range

L52 ↗

SchemeTheory.rTensor_surjective_of_pow_smul_mem_range

Documentation

If powers of the inverted element bring every vector into the image, the localized linear map is surjective.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct nonZeroDivisors
universe u v w w'

Lean source · statement

theorem rTensor_surjective_of_pow_smul_mem_range
    {R : Type u} [CommRing R] (A : Type v) [CommRing A] [Algebra R A]
    (x : R) [IsLocalization.Away x A]
    {M : Type w} [AddCommGroup M] [Module R M]
    {N : Type w'} [AddCommGroup N] [Module R N]
    (f : M →ₗ[R] N) (h : ∀ n : N, ∃ (m : M) (k : ℕ), f m = x ^ k • n) :
    Function.Surjective (f.rTensor A)

theorem

linearMap_bijective_of_tensor_primeAwayPair

L86 ↗

SchemeTheory.linearMap_bijective_of_tensor_primeAwayPair

Documentation

Two principal-localization isomorphisms detect an isomorphism from a flat source when the first parameter acts regularly on the target.

Source context 11 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct nonZeroDivisors
universe u v w w'
section Pair
variable {R : Type u} [CommRing R] [IsDomain R]
variable (F : Type v) [Field F] [Algebra R F] [IsFractionRing R F]
variable {x y : R} (hx : Prime x) (hy : y ≠ 0) (hxy : ¬ x ∣ y)
local notation "Aₓ" => Localization.subalgebra.ofField F (Submonoid.powers x)
  (Submonoid.powers_le.mpr (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero))
local notation "Aᵧ" => Localization.subalgebra.ofField F (Submonoid.powers y)
  (Submonoid.powers_le.mpr (mem_nonZeroDivisors_iff_ne_zero.mpr hy))
include hxy in

Lean source · statement

theorem linearMap_bijective_of_tensor_primeAwayPair
    {M : Type w} [AddCommGroup M] [Module R M] [Module.Flat R M]
    {N : Type w'} [AddCommGroup N] [Module R N] (hxN : IsSMulRegular N x)
    (f : M →ₗ[R] N)
    (hfx : Function.Bijective (f.rTensor Aₓ))
    (hfy : Function.Bijective (f.rTensor Aᵧ)) : Function.Bijective f

Module documentation

Detecting an isomorphism on two principal opens

Declarations

tmul_one_injective_of_isTorsionFree

rTensor_surjective_of_pow_smul_mem_range

linearMap_bijective_of_tensor_primeAwayPair