Module

Module_projective_of_isReduced_of_finrank_fiber_const.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_projective_of_isReduced_of_finrank_fiber_const

10 declarations indexed from sourceView source ↗

Module documentation

Module projective of is Reduced of finrank fiber const

Imports23

Mathlib.Algebra.Module.FinitePresentation
Mathlib.Algebra.Module.Projective
Mathlib.LinearAlgebra.Dimension.Finrank
Mathlib.RingTheory.Nilpotent.Defs
Mathlib.RingTheory.Spectrum.Prime.Defs
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.LinearAlgebra.Dimension.Constructions
Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Mathlib.LinearAlgebra.TensorProduct.Pi
Mathlib.LinearAlgebra.TensorProduct.RightExactness
Mathlib.RingTheory.TensorProduct.Finite
Mathlib.RingTheory.TensorProduct.Free
Mathlib.RingTheory.Support
Mathlib.RingTheory.LocalRing.Module
Mathlib.RingTheory.LocalProperties.Projective
Mathlib.RingTheory.LocalProperties.Reduced
Mathlib.RingTheory.Localization.Integer
Mathlib.RingTheory.Localization.Ideal
Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.Nilpotent.Lemmas
Mathlib.RingTheory.Noetherian.Basic

Imported by1

Nyll.AlgebraicCurves.Foundations.Algebra.All

abbrev

κ

L59 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_projective_of_isReduced_of_finrank_fiber_const.CBCSol.κ

Documentation

The residue field at a prime of the base ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_projective_of_isReduced_of_finrank_fiber_const
noncomputable section
universe u v
open scoped TensorProduct
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

abbrev κ (𝔭 : PrimeSpectrum R) : Type u

theorem

span_one_tmul_eq_top

L61 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_projective_of_isReduced_of_finrank_fiber_const.CBCSol.span_one_tmul_eq_top

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_projective_of_isReduced_of_finrank_fiber_const
noncomputable section
universe u v
open scoped TensorProduct
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · full declaration

theorem span_one_tmul_eq_top (𝔭 : PrimeSpectrum R) :
    Submodule.span (κ 𝔭) (Set.range fun x : M => (1 : κ 𝔭) ⊗ₜ[R] x) = ⊤ := by
  rw [eq_top_iff]
  rintro t -
  induction t using TensorProduct.inductionOn with
  | tmul a x =>
    have : a ⊗ₜ[R] x = a • ((1 : κ 𝔭) ⊗ₜ[R] x) := by
      rw [TensorProduct.smul_tmul', smul_eq_mul, mul_one]
    rw [this]
    exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨x, rfl⟩)
  | add s t hs ht => exact Submodule.add_mem _ hs ht

theorem

exists_basis_one_tmul

L73 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_projective_of_isReduced_of_finrank_fiber_const.CBCSol.exists_basis_one_tmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_projective_of_isReduced_of_finrank_fiber_const
noncomputable section
universe u v
open scoped TensorProduct
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem exists_basis_one_tmul [Module.Finite R M] (𝔭 : PrimeSpectrum R) :
    ∃ (ι : Type v) (_ : Fintype ι) (m : ι → M) (b : Module.Basis ι (κ 𝔭) (κ 𝔭 ⊗[R] M)),
      ∀ i, b i = (1 : κ 𝔭) ⊗ₜ[R] m i

theorem

subsingleton_residue_tensor_coker

L84 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_projective_of_isReduced_of_finrank_fiber_const.CBCSol.subsingleton_residue_tensor_coker

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_projective_of_isReduced_of_finrank_fiber_const
noncomputable section
universe u v
open scoped TensorProduct
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem subsingleton_residue_tensor_coker (𝔭 : PrimeSpectrum R) {ι : Type v} [Fintype ι]
    (m : ι → M) (b : Module.Basis ι (κ 𝔭) (κ 𝔭 ⊗[R] M)) (hb : ∀ i, b i = (1 : κ 𝔭) ⊗ₜ[R] m i) :
    Subsingleton (κ 𝔭 ⊗[R] (M ⧸ LinearMap.range (Fintype.linearCombination R m)))

theorem

baseChange_injective_of_le

L111 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_projective_of_isReduced_of_finrank_fiber_const.CBCSol.baseChange_injective_of_le

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_projective_of_isReduced_of_finrank_fiber_const
noncomputable section
universe u v
open scoped TensorProduct
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem baseChange_injective_of_le [Module.Finite R M] {e : ℕ}
    (hconst : ∀ 𝔮 : PrimeSpectrum R, Module.finrank (κ 𝔮) (κ 𝔮 ⊗[R] M) = e)
    (𝔭 : PrimeSpectrum R) {ι : Type v}
    [Fintype ι] (m : ι → M) (b : Module.Basis ι (κ 𝔭) (κ 𝔭 ⊗[R] M))
    (hb : ∀ i, b i = (1 : κ 𝔭) ⊗ₜ[R] m i) {𝔮 : PrimeSpectrum R} (hle : 𝔮 ≤ 𝔭) :
    Function.Injective ((Fintype.linearCombination R m).baseChange (κ 𝔮))

theorem

coeff_mem_of_rel

L149 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_projective_of_isReduced_of_finrank_fiber_const.CBCSol.coeff_mem_of_rel

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_projective_of_isReduced_of_finrank_fiber_const
noncomputable section
universe u v
open scoped TensorProduct
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem coeff_mem_of_rel [Module.Finite R M] {e : ℕ}
    (hconst : ∀ 𝔮 : PrimeSpectrum R, Module.finrank (κ 𝔮) (κ 𝔮 ⊗[R] M) = e)
    (𝔭 : PrimeSpectrum R) {ι : Type v} [Fintype ι]
    (m : ι → M) (b : Module.Basis ι (κ 𝔭) (κ 𝔭 ⊗[R] M))
    (hb : ∀ i, b i = (1 : κ 𝔭) ⊗ₜ[R] m i) {𝔮 : PrimeSpectrum R} (hle : 𝔮 ≤ 𝔭)
    (x : ι → R) (hx : Fintype.linearCombination R m x = 0) (i : ι) : x i ∈ 𝔮.asIdeal

theorem

algebraMap_coeff_eq_zero

L167 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_projective_of_isReduced_of_finrank_fiber_const.CBCSol.algebraMap_coeff_eq_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_projective_of_isReduced_of_finrank_fiber_const
noncomputable section
universe u v
open scoped TensorProduct
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem algebraMap_coeff_eq_zero [IsReduced R] [Module.Finite R M] {e : ℕ}
    (hconst : ∀ 𝔮 : PrimeSpectrum R, Module.finrank (κ 𝔮) (κ 𝔮 ⊗[R] M) = e)
    (𝔭 : PrimeSpectrum R)
    {ι : Type v} [Fintype ι] (m : ι → M) (b : Module.Basis ι (κ 𝔭) (κ 𝔭 ⊗[R] M))
    (hb : ∀ i, b i = (1 : κ 𝔭) ⊗ₜ[R] m i)
    (x : ι → R) (hx : Fintype.linearCombination R m x = 0) (i : ι) :
    algebraMap R (Localization.AtPrime 𝔭.asIdeal) (x i) = 0

theorem

free_localizedModule_of_isReduced

L187 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_projective_of_isReduced_of_finrank_fiber_const.CBCSol.free_localizedModule_of_isReduced

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_projective_of_isReduced_of_finrank_fiber_const
noncomputable section
universe u v
open scoped TensorProduct
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem free_localizedModule_of_isReduced [IsReduced R] [Module.Finite R M] {e : ℕ}
    (hconst : ∀ 𝔮 : PrimeSpectrum R, Module.finrank (κ 𝔮) (κ 𝔮 ⊗[R] M) = e)
    (𝔭 : PrimeSpectrum R) :
    Module.Free (Localization.AtPrime 𝔭.asIdeal)
      (LocalizedModule 𝔭.asIdeal.primeCompl M)

theorem

projective_of_isReduced_of_finrank_const

L240 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_projective_of_isReduced_of_finrank_fiber_const.CBCSol.projective_of_isReduced_of_finrank_const

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_projective_of_isReduced_of_finrank_fiber_const
noncomputable section
universe u v
open scoped TensorProduct
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem projective_of_isReduced_of_finrank_const [IsReduced R] [Module.FinitePresentation R M]
    {e : ℕ} (hconst : ∀ 𝔮 : PrimeSpectrum R, Module.finrank (κ 𝔮) (κ 𝔮 ⊗[R] M) = e) :
    Module.Projective R M

theorem

projective_of_isReduced_of_finrank_fiber_const

L251 ↗

Module.projective_of_isReduced_of_finrank_fiber_const

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_projective_of_isReduced_of_finrank_fiber_const
noncomputable section
universe u v
open scoped TensorProduct

Lean source · statement

theorem _root_.Module.projective_of_isReduced_of_finrank_fiber_const {R : Type u} [CommRing R]
    [IsReduced R] {M : Type v} [AddCommGroup M] [Module R M] [Module.FinitePresentation R M]
    {e : ℕ} (h : ∀ 𝔭 : PrimeSpectrum R,
      Module.finrank 𝔭.asIdeal.ResidueField (𝔭.asIdeal.ResidueField ⊗[R] M) = e) :
    Module.Projective R M

Module documentation

Module projective of is Reduced of finrank fiber const

Declarations