NYLL
Module

PrimeAwayPairGluing.lean

Nyll.SchemeTheory.RingTheory.Descent.PrimeAwayPairGluing
4 declarations indexed from sourceView source ↗

Module documentation

Gluing across two principal opens after flat base change

Two relatively prime principal localizations of a domain intersect in the base ring when one parameter is prime. Flat tensor products preserve this equalizer. This supplies the scalar extension step on completion overlaps; neither normality nor Noetherianity of the tensor product is required.

Imports3
Imported by3

Declarations

theorem

existsUnique_tensor_pair_of_inf_eq_bot

L29 ↗
SchemeTheory.existsUnique_tensor_pair_of_inf_eq_bot
Source context 4 commands

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

noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u v w w'
Lean source · statement
theorem existsUnique_tensor_pair_of_inf_eq_bot
    {R : Type u} [CommRing R] {F : Type v} [CommRing F] [Algebra R F]
    [FaithfulSMul R F] (A B : Subalgebra R F) (hAB : A ⊓ B = ⊥)
    (M : Type w) [AddCommGroup M] [Module R M] [Module.Flat R M]
    (a : M ⊗[R] A) (b : M ⊗[R] B)
    (hab : (A.val.toLinearMap.lTensor M) a = (B.val.toLinearMap.lTensor M) b) :
    ∃! m : M, m ⊗ₜ[R] (1 : A) = a ∧ m ⊗ₜ[R] (1 : B) = b
theorem

existsUnique_tensor_primeAwayPair

L97 ↗
SchemeTheory.existsUnique_tensor_primeAwayPair
Documentation

Compatible sections over two prime-away localizations glue uniquely after tensoring with any flat module.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u v w w'
Lean source · statement
theorem existsUnique_tensor_primeAwayPair
    {R : Type u} [CommRing R] [IsDomain R]
    (F : Type v) [Field F] [Algebra R F] [IsFractionRing R F]
    {x y : R} (hx : Prime x) (hy : y ≠ 0) (hxy : ¬ x ∣ y)
    (M : Type w) [AddCommGroup M] [Module R M] [Module.Flat R M]
    (a : M ⊗[R] Localization.subalgebra.ofField F (Submonoid.powers x)
      (Submonoid.powers_le.mpr (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero)))
    (b : M ⊗[R] Localization.subalgebra.ofField F (Submonoid.powers y)
      (Submonoid.powers_le.mpr (mem_nonZeroDivisors_iff_ne_zero.mpr hy)))
    (hab :
      ((Localization.subalgebra.ofField F (Submonoid.powers x)
        (Submonoid.powers_le.mpr
          (mem_nonZeroDivisors_iff_ne_zero.mpr hx.ne_zero))).val.toLinearMap.lTensor M) a =
      ((Localization.subalgebra.ofField F (Submonoid.powers y)
        (Submonoid.powers_le.mpr
          (mem_nonZeroDivisors_iff_ne_zero.mpr hy))).val.toLinearMap.lTensor M) b) :
    ∃! m : M, m ⊗ₜ[R] 1 = a ∧ m ⊗ₜ[R] 1 = b
theorem

tensor_primeAwayPair_ext

L134 ↗
SchemeTheory.tensor_primeAwayPair_ext
Documentation

Equality can be tested on the two principal localizations.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u v w w'
section LinearMaps
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 tensor_primeAwayPair_ext
    (M : Type w) [AddCommGroup M] [Module R M] [Module.Flat R M]
    {m n : M} (ha : m ⊗ₜ[R] (1 : Aₓ) = n ⊗ₜ[R] (1 : Aₓ))
    (hb : m ⊗ₜ[R] (1 : Aᵧ) = n ⊗ₜ[R] (1 : Aᵧ)) : m = n
theorem

existsUnique_linearMap_tensor_primeAwayPair

L150 ↗
SchemeTheory.existsUnique_linearMap_tensor_primeAwayPair
Documentation

Compatible local linear maps to a flat module extend uniquely. A commuting action of another ring is preserved by the extension, so this also applies to linear maps over a completion or a tensor overlap.

Source context 11 commands

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

noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u v w w'
section LinearMaps
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 existsUnique_linearMap_tensor_primeAwayPair
    (S : Type*) [Semiring S]
    (P : Type w') [AddCommGroup P] [Module S P]
    (M : Type w) [AddCommGroup M] [Module R M] [Module.Flat R M]
    [Module S M] [SMulCommClass R S M]
    (fa : P →ₗ[S] M ⊗[R] Aₓ) (fb : P →ₗ[S] M ⊗[R] Aᵧ)
    (hab : ∀ p : P, ((Aₓ).val.toLinearMap.lTensor M) (fa p) =
      ((Aᵧ).val.toLinearMap.lTensor M) (fb p)) :
    ∃! f : P →ₗ[S] M, ∀ p : P,
      f p ⊗ₜ[R] 1 = fa p ∧ f p ⊗ₜ[R] 1 = fb p

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