Module

Module_rankAtStalk_eq_of_forall_localizedModule_equiv.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_rankAtStalk_eq_of_forall_localizedModule_equiv

5 declarations indexed from sourceView source ↗

Module documentation

Stalk ranks preserved by local equivalences

Compares ranks at stalks using module equivalences after localization.

Imports6

Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Mathlib.RingTheory.Spectrum.Prime.Noetherian
Mathlib.RingTheory.IsTensorProduct
Mathlib.RingTheory.Localization.BaseChange
Mathlib.LinearAlgebra.TensorProduct.Pi
Mathlib.RingTheory.Artinian.Module

Imported by3

theorem

isLocalizedModule_id_of_forall_isUnit

L42 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_rankAtStalk_eq_of_forall_localizedModule_equiv.RankAtStalkLocallyIso.isLocalizedModule_id_of_forall_isUnit

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_rankAtStalk_eq_of_forall_localizedModule_equiv
open TensorProduct
universe u
namespace RankAtStalkLocallyIso
section UnitsBaseChange
variable {A : Type*} [CommRing A] (S : Submonoid A) (T : Type*) [CommRing T] [Algebra A T]
  (X : Type*) [AddCommGroup X] [Module A X]

Lean source · full declaration

theorem isLocalizedModule_id_of_forall_isUnit (hT : ∀ s : S, IsUnit (algebraMap A T s)) :
    IsLocalizedModule S (LinearMap.id : T ⊗[A] X →ₗ[A] T ⊗[A] X) where
  map_units s := by
    rw [Module.End.isUnit_iff]
    have : ⇑(algebraMap A (Module.End A (T ⊗[A] X)) s) = fun y => algebraMap A T s • y := by
      funext y
      simp [Module.algebraMap_end_apply]
    rw [this]
    exact (hT s).smul_bijective
  surj y := ⟨(y, 1), one_smul _ _⟩
  exists_of_eq h := ⟨1, by simpa using h⟩

def

tensorLocalizedModuleEquiv

L55 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_rankAtStalk_eq_of_forall_localizedModule_equiv.RankAtStalkLocallyIso.tensorLocalizedModuleEquiv

Documentation

The tensor equivalence induced by localization when every denominator acts as a unit.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_rankAtStalk_eq_of_forall_localizedModule_equiv
open TensorProduct
universe u
namespace RankAtStalkLocallyIso
section UnitsBaseChange
variable {A : Type*} [CommRing A] (S : Submonoid A) (T : Type*) [CommRing T] [Algebra A T]
  (X : Type*) [AddCommGroup X] [Module A X]

Lean source · statement

def tensorLocalizedModuleEquiv (hT : ∀ s : S, IsUnit (algebraMap A T s)) :
    T ⊗[A] X ≃ₗ[T] T ⊗[A] LocalizedModule S X

theorem

finrank_eq_sum_finrank_localization

L81 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_rankAtStalk_eq_of_forall_localizedModule_equiv.RankAtStalkLocallyIso.finrank_eq_sum_finrank_localization

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_rankAtStalk_eq_of_forall_localizedModule_equiv
open TensorProduct
universe u
namespace RankAtStalkLocallyIso
section Artinian
variable (k : Type*) [Field k] (B : Type*) [CommRing B] [Algebra k B] [IsArtinianRing B]
  (V : Type*) [AddCommGroup V] [Module B V] [Module k V] [IsScalarTower k B V] [Module.Finite k V]

Lean source · statement

theorem finrank_eq_sum_finrank_localization [Fintype (PrimeSpectrum B)] :
    Module.finrank k V =
      ∑ q : PrimeSpectrum B, Module.finrank k (Localization.AtPrime q.asIdeal ⊗[B] V)

theorem

finrank_eq_of_forall_localization_equiv

L96 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_rankAtStalk_eq_of_forall_localizedModule_equiv.RankAtStalkLocallyIso.finrank_eq_of_forall_localization_equiv

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_rankAtStalk_eq_of_forall_localizedModule_equiv
open TensorProduct
universe u
namespace RankAtStalkLocallyIso
section Artinian
variable (k : Type*) [Field k] (B : Type*) [CommRing B] [Algebra k B] [IsArtinianRing B]
  (V : Type*) [AddCommGroup V] [Module B V] [Module k V] [IsScalarTower k B V] [Module.Finite k V]

Lean source · statement

theorem finrank_eq_of_forall_localization_equiv (W : Type*) [AddCommGroup W] [Module B W]
    [Module k W] [IsScalarTower k B W] [Module.Finite k W]
    (H : ∀ q : PrimeSpectrum B, Nonempty
      (Localization.AtPrime q.asIdeal ⊗[B] V ≃ₗ[k] Localization.AtPrime q.asIdeal ⊗[B] W)) :
    Module.finrank k V = Module.finrank k W

theorem

rankAtStalk_eq_of_forall_localizedModule_equiv

L111 ↗

Module.rankAtStalk_eq_of_forall_localizedModule_equiv

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_rankAtStalk_eq_of_forall_localizedModule_equiv
open TensorProduct
universe u
open RankAtStalkLocallyIso in

Lean source · statement

theorem _root_.Module.rankAtStalk_eq_of_forall_localizedModule_equiv
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] [Module.Finite R A]
    (M N : Type u) [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M]
    [Module.Finite R M] [Module.Flat R M]
    [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N]
    [Module.Finite R N] [Module.Flat R N] (s : Set A) (hs : Ideal.span s = ⊤)
    (H : ∀ h ∈ s, Nonempty
      (LocalizedModule (Submonoid.powers h) M ≃ₗ[A] LocalizedModule (Submonoid.powers h) N)) :
    Module.rankAtStalk (R := R) M = Module.rankAtStalk N

Module documentation

Stalk ranks preserved by local equivalences

Declarations

isLocalizedModule_id_of_forall_isUnit

tensorLocalizedModuleEquiv

finrank_eq_sum_finrank_localization

finrank_eq_of_forall_localization_equiv

rankAtStalk_eq_of_forall_localizedModule_equiv