Module

LocalCriterion.lean

Nyll.SchemeTheory.RingTheory.Flat.LocalCriterion

23 declarations indexed from sourceView source ↗

Module documentation

Local flatness criteria.

Imports17

Mathlib.Algebra.Module.LocalizedModule.Basic
Mathlib.Algebra.Module.Torsion.Basic
Mathlib.LinearAlgebra.DirectSum.Finsupp
Mathlib.LinearAlgebra.Finsupp.LinearCombination
Mathlib.LinearAlgebra.Isomorphisms
Mathlib.LinearAlgebra.Prod
Mathlib.LinearAlgebra.TensorProduct.RightExactness
Mathlib.LinearAlgebra.TensorProduct.Tower
Mathlib.RingTheory.Filtration
Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.Flat.Tensor
Mathlib.RingTheory.Flat.Localization
Mathlib.RingTheory.LocalRing.ResidueField.Defs
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.SimpleModule.Basic
Mathlib.Tactic.LinearCombination

Imported by4

def

FreeCover

L49 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.FreeCover

Documentation

The free R-module on the elements of X, implemented as finitely supported functions.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v

Lean source · statement

def FreeCover (R : Type u) [CommRing R] (X : Type*) : Type _

instance

(anonymous instance)

L55 ↗

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
namespace FreeCover
variable (R : Type u) [CommRing R] (X : Type*)

Lean source · statement

instance : AddCommGroup (FreeCover R X)

instance

(anonymous instance)

L56 ↗

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
namespace FreeCover
variable (R : Type u) [CommRing R] (X : Type*)

Lean source · statement

instance : Module R (FreeCover R X)

def

equiv

L59 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.FreeCover.equiv

Documentation

The linear equivalence identifying the free cover with its finitely supported functions.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
namespace FreeCover
variable (R : Type u) [CommRing R] (X : Type*)

Lean source · statement

def equiv : FreeCover R X ≃ₗ[R] (X →₀ R)

theorem

lTensor_injective_of_cover

L69 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.lTensor_injective_of_cover

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section KernelTransfer
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem lTensor_injective_of_cover
    {N₁ N₂ G L K : Type*} [AddCommGroup N₁] [AddCommGroup N₂] [Module R N₁] [Module R N₂]
    [AddCommGroup G] [AddCommGroup L] [Module R G] [Module R L] [AddCommGroup K] [Module R K]
    {f : N₁ →ₗ[R] N₂} {v : G →ₗ[R] N₂} {i : L →ₗ[R] G} {u : L →ₗ[R] N₁}
    {k : K →ₗ[R] G} {ι' : K →ₗ[R] L}
    (hv : Function.Surjective v) (hu : Function.Surjective u)
    (hcomm : v ∘ₗ i = f ∘ₗ u) (hk : Function.Exact k v)
    (h1 : i ∘ₗ ι' = k) (h2 : u ∘ₗ ι' = 0)
    (hi : Function.Injective (i.lTensor M)) :
    Function.Injective (f.lTensor M)

def

cover

L96 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.cover

Documentation

The canonical surjection from the free module on the elements of N2 to N2.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section KernelTransfer
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

def cover (N₂ : Type*) [AddCommGroup N₂] [Module R N₂] :
    FreeCover R N₂ →ₗ[R] N₂

theorem

cover_surjective

L100 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.cover_surjective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section KernelTransfer
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem cover_surjective (N₂ : Type*) [AddCommGroup N₂] [Module R N₂] :
    Function.Surjective (cover (R := R) N₂)

theorem

lTensor_injective_of_comap_cover

L104 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.lTensor_injective_of_comap_cover

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section KernelTransfer
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem lTensor_injective_of_comap_cover
    {N₁ N₂ : Type*} [AddCommGroup N₁] [AddCommGroup N₂] [Module R N₁] [Module R N₂]
    (f : N₁ →ₗ[R] N₂) (_hf : Function.Injective f)
    (_hL : Function.Injective
      (((LinearMap.range f).comap (cover (R := R) N₂)).subtype.lTensor M)) :
    Function.Injective (f.lTensor M)

theorem

lTensor_mapRange_injective

L155 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.lTensor_mapRange_injective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section KernelTransfer
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem lTensor_mapRange_injective (I : Ideal R)
    (hI : Function.Injective (I.subtype.lTensor M)) (ι : Type*) :
    Function.Injective
      ((Finsupp.mapRange.linearMap (α := ι) I.subtype).lTensor M)

def

TorVanish

L180 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.TorVanish

Documentation

Tensoring with M preserves injectivity at the start of every short exact sequence ending in N.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section KernelTransfer
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
variable (R M) in

Lean source · statement

def TorVanish (N : Type u) [AddCommGroup N] [Module R N] : Prop

theorem

torVanish_of_torsion

L186 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.torVanish_of_torsion

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section KernelTransfer
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
variable (R M) in

Lean source · statement

theorem torVanish_of_torsion (I : Ideal R)
    (hsplit : ∀ ⦃Q₁ Q₂ : Type u⦄ [AddCommGroup Q₁] [AddCommGroup Q₂] [Module R Q₁]
      [Module R Q₂] (g : Q₁ →ₗ[R] Q₂), Function.Injective g →
      Module.IsTorsionBySet R Q₁ I → Module.IsTorsionBySet R Q₂ I →
      Function.Injective (g.lTensor M))
    (hI : Function.Injective (I.subtype.lTensor M))
    {N : Type u} [AddCommGroup N] [Module R N] (hN : Module.IsTorsionBySet R N I) :
    TorVanish R M N

theorem

torVanish_of_extension

L283 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.torVanish_of_extension

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section KernelTransfer
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
variable (R M) in

Lean source · statement

theorem torVanish_of_extension {N' N N'' : Type u} [AddCommGroup N'] [AddCommGroup N]
    [AddCommGroup N''] [Module R N'] [Module R N] [Module R N'']
    (ι : N' →ₗ[R] N) (π : N →ₗ[R] N'') (hι : Function.Injective ι)
    (hπ : Function.Surjective π) (hιπ : Function.Exact ι π)
    (h' : TorVanish R M N') (h'' : TorVanish R M N'') : TorVanish R M N

theorem

torVanish_of_subsingleton

L356 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.torVanish_of_subsingleton

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section KernelTransfer
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
variable (R M) in

Lean source · statement

theorem torVanish_of_subsingleton {N : Type u} [AddCommGroup N] [Module R N]
    [Subsingleton N] : TorVanish R M N

theorem

torVanish_of_torsion_pow

L369 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.torVanish_of_torsion_pow

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section KernelTransfer
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
variable (R M) in

Lean source · statement

theorem torVanish_of_torsion_pow (I : Ideal R)
    (hsplit : ∀ ⦃Q₁ Q₂ : Type u⦄ [AddCommGroup Q₁] [AddCommGroup Q₂] [Module R Q₁]
      [Module R Q₂] (g : Q₁ →ₗ[R] Q₂), Function.Injective g →
      Module.IsTorsionBySet R Q₁ I → Module.IsTorsionBySet R Q₂ I →
      Function.Injective (g.lTensor M))
    (hI : Function.Injective (I.subtype.lTensor M)) (n : ℕ) :
    ∀ {N : Type u} [AddCommGroup N] [Module R N],
      Module.IsTorsionBySet R N (I ^ n : Ideal R) → TorVanish R M N

theorem

ker_le_range_of_torVanish

L418 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.ker_le_range_of_torVanish

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section Tail
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem ker_le_range_of_torVanish (𝔞 J : Ideal R)
    (h : TorVanish R M (R ⧸ (𝔞 ⊔ J))) (x : M ⊗[R] 𝔞) (hx : (𝔞.subtype.lTensor M) x = 0) :
    x ∈ LinearMap.range ((Submodule.inclusion (inf_le_left : 𝔞 ⊓ J ≤ 𝔞)).lTensor M)

theorem

range_lTensor_inclusion_le_smul

L471 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.range_lTensor_inclusion_le_smul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section Tail
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]

Lean source · statement

theorem range_lTensor_inclusion_le_smul (𝔞 J 𝔟 : Ideal R) (h𝔟 : 𝔟 ≤ J * 𝔞) (hle : 𝔟 ≤ 𝔞) :
    LinearMap.range ((Submodule.inclusion hle).lTensor M) ≤
      (J • ⊤ : Submodule R (M ⊗[R] 𝔞))

theorem

finite_lTensor_ideal

L504 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.finite_lTensor_ideal

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section Tail
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
variable {S : Type*} [CommRing S] [Algebra R S] [Module S M] [IsScalarTower R S M]

Lean source · statement

theorem finite_lTensor_ideal [IsNoetherianRing R] [Module.Finite S M] (𝔞 : Ideal R) :
    Module.Finite S (M ⊗[R] 𝔞)

theorem

flat_of_torVanish_pow

L537 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.flat_of_torVanish_pow

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section Tail
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
variable {S : Type*} [CommRing S] [Algebra R S] [Module S M] [IsScalarTower R S M]

Lean source · statement

theorem flat_of_torVanish_pow [IsNoetherianRing R] [IsNoetherianRing S] [Module.Finite S M]
    (I : Ideal R) (hIS : I.map (algebraMap R S) ≤ (⊥ : Ideal S).jacobson)
    (hTV : ∀ (n : ℕ) (N : Type u) [AddCommGroup N] [Module R N],
      Module.IsTorsionBySet R N (I ^ n : Ideal R) → TorVanish R M N) :
    Module.Flat R M

theorem

isLocalizedModule_id_of_units

L606 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.isLocalizedModule_id_of_units

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section Split
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
variable {S : Type*} [CommRing S] [Algebra R S] [Module S M] [IsScalarTower R S M]

Lean source · full declaration

theorem isLocalizedModule_id_of_units (T : Submonoid R)
    (hT : ∀ t : T, IsUnit (algebraMap R S t)) :
    IsLocalizedModule T (LinearMap.id : M →ₗ[R] M) where
  map_units t := by
    obtain ⟨w, hw⟩ := hT t
    rw [Module.End.isUnit_iff]
    have hsmul : ∀ m : M, (t : R) • m = (w : S) • m := fun m => by
      rw [hw, algebraMap_smul]
    constructor
    · intro a b hab
      have hab' : (t : R) • a = (t : R) • b := hab
      rw [hsmul, hsmul] at hab'
      have := congrArg (fun m => (↑w⁻¹ : S) • m) hab'
      simp only [smul_smul, Units.inv_mul, one_smul] at this
      exact this
    · intro b
      refine ⟨(↑w⁻¹ : S) • b, ?_⟩
      change (t : R) • ((↑w⁻¹ : S) • b) = b
      rw [hsmul, smul_smul, Units.mul_inv, one_smul]
  surj y := ⟨(y, 1), by simp⟩
  exists_of_eq h := ⟨1, by simpa using h⟩

theorem

isTorsionBySet_baseChange

L628 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.isTorsionBySet_baseChange

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section Split
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
variable {S : Type*} [CommRing S] [Algebra R S] [Module S M] [IsScalarTower R S M]

Lean source · statement

theorem isTorsionBySet_baseChange (p : Ideal R) [p.IsPrime] {Q : Type*} [AddCommGroup Q]
    [Module R Q] (hQ : Module.IsTorsionBySet R Q p) :
    Module.IsTorsionBySet (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] Q)
      (IsLocalRing.maximalIdeal (Localization.AtPrime p))

theorem

lTensor_injective_of_torsion

L648 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.lTensor_injective_of_torsion

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover
section Split
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
variable {S : Type*} [CommRing S] [Algebra R S] [Module S M] [IsScalarTower R S M]

Lean source · statement

theorem lTensor_injective_of_torsion (p : Ideal R) [p.IsPrime]
    (hunit : ∀ t : p.primeCompl, IsUnit (algebraMap R S t))
    {Q₁ Q₂ : Type*} [AddCommGroup Q₁] [AddCommGroup Q₂] [Module R Q₁] [Module R Q₂]
    (g : Q₁ →ₗ[R] Q₂) (hg : Function.Injective g)
    (h₂ : Module.IsTorsionBySet R Q₂ p) :
    Function.Injective (g.lTensor M)

theorem

flat_of_comap_maximalIdeal_lTensor_injective

L693 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_comap_maximalIdeal_rTensor_injective.LocalFlatnessCriterionAtPrime.flat_of_comap_maximalIdeal_lTensor_injective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap
noncomputable section
namespace LocalFlatnessCriterionAtPrime
universe u v
open scoped FreeCover

Lean source · statement

theorem flat_of_comap_maximalIdeal_lTensor_injective
    {R : Type u} {S : Type*} {M : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [IsNoetherianRing R] [IsNoetherianRing S] [IsLocalRing S]
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Module.Finite S M]
    (h : Function.Injective
      (((IsLocalRing.maximalIdeal S).comap (algebraMap R S)).subtype.lTensor M)) :
    Module.Flat R M

theorem

flat_of_comap_maximalIdeal_rTensor_injective

L720 ↗

Module.flat_of_comap_maximalIdeal_rTensor_injective

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_comap_maximalIdeal_rTensor_injective
open TensorProduct LinearMap

Lean source · statement

theorem _root_.Module.flat_of_comap_maximalIdeal_rTensor_injective
    {R S M : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [IsNoetherianRing R] [IsNoetherianRing S] [IsLocalRing S]
    [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Module.Finite S M]
    (p : Ideal R) (hp : (IsLocalRing.maximalIdeal S).comap (algebraMap R S) = p)
    (h : Function.Injective (p.subtype.rTensor M)) :
    Module.Flat R M

Module documentation

Declarations