Module

FiniteFreeHom.lean

Nyll.EtaleFundamentalGroups.Purity.HeightOne.FiniteFreeHom

2 declarations indexed from sourceView source ↗

Module documentation

Descent of finite-free morphisms from height-one localizations

Over a unique factorization domain, a matrix over the fraction field whose entries belong to every prime-element localization has a unique matrix over the original ring. Via the standard bases, this gives existence and uniqueness of a descended morphism between finite free modules.

This is a coordinate codimension-one full-faithfulness input. It does not assert extension of finite étale covers across a punctured spectrum.

Imports3

Mathlib.LinearAlgebra.Matrix.ToLin
Nyll.EtaleFundamentalGroups.Purity.HeightOne.UFDIntersection
Mathlib.Data.Fintype.EquivFin

Imported by2

theorem

existsUnique_matrix_over_base_of_mem_localization_primeElement

L33 ↗

EtaleFundamentalGroups.existsUnique_matrix_over_base_of_mem_localization_primeElement

Documentation

A finite matrix over the fraction field descends uniquely when every entry belongs to each prime-element localization.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open nonZeroDivisors
universe u v

Lean source · full declaration

theorem existsUnique_matrix_over_base_of_mem_localization_primeElement
    {A : Type u} {K : Type v}
    [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    {m n : Type*} (M : Matrix m n K)
    (hM : ∀ i j (p : A) (hp : Prime p),
      letI : (Ideal.span {p}).IsPrime :=
        Ideal.isPrime_span_singleton_of_prime hp
      M i j ∈ Localization.subalgebra.ofField K
        (Ideal.span {p}).primeCompl
        (Ideal.primeCompl_le_nonZeroDivisors (Ideal.span {p}))) :
    ∃! M₀ : Matrix m n A,
      ∀ i j, algebraMap A K (M₀ i j) = M i j := by
  classical
  have hentry (i : m) (j : n) : M i j ∈ (⊥ : Subalgebra A K) :=
    mem_bot_of_mem_localization_primeElement (M i j) (hM i j)
  let M₀ : Matrix m n A := fun i j ↦
    Classical.choose (Algebra.mem_bot.mp (hentry i j))
  have hM₀ (i : m) (j : n) : algebraMap A K (M₀ i j) = M i j :=
    Classical.choose_spec (Algebra.mem_bot.mp (hentry i j))
  refine ⟨M₀, hM₀, ?_⟩
  intro N hN
  ext i j
  exact IsFractionRing.injective A K <| (hN i j).trans (hM₀ i j).symm

theorem

existsUnique_linearMap_pi_over_base_of_mem_localization_primeElement

L61 ↗

EtaleFundamentalGroups.existsUnique_linearMap_pi_over_base_of_mem_localization_primeElement