Module

PrimeAwayAlgebraGluing.lean

Nyll.SchemeTheory.RingTheory.Descent.PrimeAwayAlgebraGluing

2 declarations indexed from sourceView source ↗

Module documentation

Extending algebra maps across a pair of principal opens

Flat Hartogs extension preserves the multiplicative structure: the algebra identities can be checked after the two principal localizations. These are the maps used to extend the actual completion-overlap isomorphism.

Imports3

Nyll.SchemeTheory.RingTheory.Descent.PrimeAwayPairGluing
Mathlib.Algebra.Algebra.Equiv
Mathlib.RingTheory.TensorProduct.Basic

Imported by1

Nyll.SchemeTheory.RingTheory.Descent.All

theorem

existsUnique_algHom_tensor_primeAwayPair

L38 ↗

SchemeTheory.existsUnique_algHom_tensor_primeAwayPair

Documentation

Compatible local algebra maps to a flat algebra extend uniquely.

Source context 10 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct nonZeroDivisors
universe u v w w'
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_algHom_tensor_primeAwayPair
    (S : Type*) [CommRing S]
    (P : Type w') [CommRing P] [Algebra S P]
    (M : Type w) [CommRing M] [Algebra R M] [Module.Flat R M]
    [Algebra 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

theorem

exists_algEquiv_tensor_primeAwayPair

L80 ↗

SchemeTheory.exists_algEquiv_tensor_primeAwayPair