Module

Module_exists_forall_isUnit_rankAtStalk_baseChange_eq_finrank_residueField_tensor.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_exists_forall_isUnit_rankAtStalk_baseChange_eq_finrank_residueField_tensor

1 declaration indexed from sourceView source ↗

Module documentation

Module exists forall is Unit rank At Stalk base Change eq finrank residue Field tensor

Imports15

Mathlib.Algebra.Module.FinitePresentation
Mathlib.Algebra.Module.Projective
Mathlib.LinearAlgebra.Basis.VectorSpace
Mathlib.LinearAlgebra.Dimension.Finrank
Mathlib.LinearAlgebra.TensorProduct.Tower
Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.Localization.Ideal
Mathlib.RingTheory.Localization.Submodule
Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.RingTheory.TensorProduct.Finite
Mathlib.Topology.LocallyConstant.Basic

Imported by2

theorem

exists_forall_isUnit_rankAtStalk_baseChange_eq_finrank_residueField_tensor

L42 ↗

Module.exists_forall_isUnit_rankAtStalk_baseChange_eq_finrank_residueField_tensor

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_exists_forall_isUnit_rankAtStalk_baseChange_eq_finrank_residueField_tensor
universe u
open TensorProduct

Lean source · statement

theorem _root_.Module.exists_forall_isUnit_rankAtStalk_baseChange_eq_finrank_residueField_tensor
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    (M : Type u) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (𝔭 : PrimeSpectrum R) (g : R) (hg : g ∉ 𝔭.asIdeal)
    (hproj : ∀ (A : Type u) [CommRing A] [Algebra R A], IsUnit (algebraMap R A g) →
      Module.Projective A (A ⊗[R] M)) :
    ∃ g' : R, g' ∉ 𝔭.asIdeal ∧
      (∀ (A : Type u) [CommRing A] [Algebra R A], IsUnit (algebraMap R A g') → IsUnit (algebraMap R
        A g)) ∧
      ∀ (A : Type u) [CommRing A] [Algebra R A], IsUnit (algebraMap R A g') →
        ∀ 𝔮 : PrimeSpectrum A,
          Module.rankAtStalk (A ⊗[R] M) 𝔮 =
            Module.finrank 𝔭.asIdeal.ResidueField (𝔭.asIdeal.ResidueField ⊗[R] M)

Module documentation

Module exists forall is Unit rank At Stalk base Change eq finrank residue Field tensor

Declarations

exists_forall_isUnit_rankAtStalk_baseChange_eq_finrank_residueField_tensor