NYLL
Module

Local.lean

Nyll.SchemeTheory.Affine.WeilRestriction.Local
2 declarations indexed from sourceView source ↗

Module documentation

Local finite étale internal Homs

A finite projective module becomes free after localizing at a suitable element outside any prescribed prime. We express this freeness using tensor products, so that the finite free Weil restriction construction applies.

For finite étale R-algebras A and B, this gives an actual finite étale internal Hom over a principal neighborhood of every point of Spec R. No global freeness assumption on A is needed.

Imports12
  • Nyll.SchemeTheory.Affine.WeilRestriction.GlobalFiniteEtale
  • Mathlib.Algebra.Module.FinitePresentation
  • Mathlib.RingTheory.Etale.Basic
  • Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
  • Mathlib.RingTheory.Flat.EquationalCriterion
  • Mathlib.RingTheory.LocalProperties.Projective
  • Mathlib.RingTheory.LocalRing.Module
  • Mathlib.RingTheory.Localization.BaseChange
  • Mathlib.RingTheory.Localization.Free
  • Mathlib.RingTheory.Smooth.Flat
  • Mathlib.RingTheory.Spectrum.Prime.Basic
  • Mathlib.RingTheory.TensorProduct.Finite
Imported by2

Declarations

lemma

exists_free_tensor_away_of_projective

L48 ↗
SchemeTheory.Affine.exists_free_tensor_away_of_projective
Documentation

A finite projective module is free on a principal neighborhood of any prime, expressed as a tensor product with the localized base ring.

Source context 6 commands

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

@[expose] public section
open CategoryTheory AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u
namespace SchemeTheory.Affine
Lean source · statement
lemma exists_free_tensor_away_of_projective
    {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M]
    [Module.Finite R M] [Module.Projective R M] (p : PrimeSpectrum R) :
    ∃ r : R, r ∉ p.asIdeal ∧
      Module.Free (Localization.Away r) (Localization.Away r ⊗[R] M)
theorem

exists_finiteEtaleInternalHomRepresentable_away

L71 ↗
SchemeTheory.Affine.exists_finiteEtaleInternalHomRepresentable_away
Documentation

Around every prime of R, the relative internal Hom of finite étale R-algebras is represented by a finite étale scheme over a principal localization of R. The representing equivalence holds for every test scheme over that localization.

Source context 6 commands

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

@[expose] public section
open CategoryTheory AlgebraicGeometry
open scoped TensorProduct
noncomputable section
universe u
namespace SchemeTheory.Affine
Lean source · statement
theorem exists_finiteEtaleInternalHomRepresentable_away
    {R A B : Type u} [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B]
    [Module.Finite R A] [Algebra.Etale R A]
    [Module.Finite R B] [Algebra.Etale R B] (p : PrimeSpectrum R) :
    ∃ r : R, r ∉ p.asIdeal ∧
      ∃ W : FiniteEtale (Spec (CommRingCat.of (Localization.Away r))),
        Nonempty ((globalInternalHomFunctor
          (R := Localization.Away r)
          (A := Localization.Away r ⊗[R] A)
          (B := Localization.Away r ⊗[R] B)).RepresentableBy
            ((FiniteEtale.forget (Spec (CommRingCat.of (Localization.Away r)))).obj W))

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