Module

GenericFlatness.lean

Nyll.SchemeTheory.RingTheory.Flat.GenericFlatness

39 declarations indexed from sourceView source ↗

Module documentation

Generic flatness of finite modules over finite-type algebras

A finite module over a finite-type algebra over a noetherian domain becomes flat after localizing at a suitable nonzero base element. The proof controls tensor kernels and passes to the localized module.

Imports15

Mathlib.Algebra.Module.LocalizedModule.Basic
Mathlib.Algebra.MvPolynomial.Equiv
Mathlib.LinearAlgebra.Basis.Basic
Mathlib.LinearAlgebra.Isomorphisms
Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Mathlib.LinearAlgebra.TensorProduct.RightExactness
Mathlib.RingTheory.FiniteType
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.Flat.Tensor
Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.Polynomial.Basic
Mathlib.Tactic.Choose
Mathlib.Tactic.Ring

Imported by3

def

KT

L51 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.KT

Documentation

Every element in the kernel of tensoring an ideal inclusion is annihilated by a power of a.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]

Lean source · statement

def KT (a : A) (M : Type*) [AddCommGroup M] [Module A M] : Prop

lemma

mul_right

L58 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.KT.mul_right

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Basic
variable {M N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]

Lean source · statement

lemma KT.mul_right {a : A} (c : A) (h : KT a M) : KT (a * c) M

lemma

mul_left

L62 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.KT.mul_left

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Basic
variable {M N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]

Lean source · statement

lemma KT.mul_left {a : A} (c : A) (h : KT a M) : KT (c * a) M

lemma

of_pow

L65 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.KT.of_pow

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Basic
variable {M N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]

Lean source · statement

lemma KT.of_pow {a : A} {m : ℕ} (h : KT (a ^ m) M) : KT a M

lemma

of_linearEquiv

L69 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.KT.of_linearEquiv

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Basic
variable {M N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]

Lean source · statement

lemma KT.of_linearEquiv {a : A} (e : M ≃ₗ[A] N) (h : KT a M) : KT a N

lemma

of_flat

L80 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.KT.of_flat

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Basic
variable {M N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]

Lean source · statement

lemma KT.of_flat (a : A) [Module.Flat A M] : KT a M

lemma

smul_tensor_eq_zero

L87 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.smul_tensor_eq_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Basic
variable {M N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]

Lean source · statement

lemma smul_tensor_eq_zero {a : A} (h : ∀ m : M, a • m = 0) {P : Type*} [AddCommGroup P]
    [Module A P] (k : M ⊗[A] P) : a • k = 0

lemma

of_smul_eq_zero

L93 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.KT.of_smul_eq_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Basic
variable {M N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]

Lean source · statement

lemma KT.of_smul_eq_zero {a : A} (h : ∀ m : M, a • m = 0) : KT a M

lemma

rid_rTensor

L103 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.rid_rTensor

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Extension
variable {M₁ M₂ M₃ : Type*} [AddCommGroup M₁] [Module A M₁] [AddCommGroup M₂] [Module A M₂]
  [AddCommGroup M₃] [Module A M₃]

Lean source · statement

lemma rid_rTensor (ι : M₁ →ₗ[A] M₂) (z : M₁ ⊗[A] A) :
    TensorProduct.rid A M₂ (LinearMap.rTensor A ι z) = ι (TensorProduct.rid A M₁ z)

lemma

rTensor_injective_of_injective

L109 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.rTensor_injective_of_injective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Extension
variable {M₁ M₂ M₃ : Type*} [AddCommGroup M₁] [Module A M₁] [AddCommGroup M₂] [Module A M₂]
  [AddCommGroup M₃] [Module A M₃]

Lean source · statement

lemma rTensor_injective_of_injective (ι : M₁ →ₗ[A] M₂) (hι : Function.Injective ι) :
    Function.Injective (LinearMap.rTensor A ι)

theorem

extension

L116 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.KT.extension

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Extension
variable {M₁ M₂ M₃ : Type*} [AddCommGroup M₁] [Module A M₁] [AddCommGroup M₂] [Module A M₂]
  [AddCommGroup M₃] [Module A M₃]

Lean source · statement

theorem KT.extension {a₁ a₃ : A} (ι : M₁ →ₗ[A] M₂) (π : M₂ →ₗ[A] M₃)
    (hι : Function.Injective ι) (hex : Function.Exact ι π) (hπ : Function.Surjective π)
    (h₁ : KT a₁ M₁) (h₃ : KT a₃ M₃) : KT (a₁ * a₃) M₂

theorem

of_directed_cover

L143 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.KT.of_directed_cover

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Union
variable {M : Type*} [AddCommGroup M] [Module A M]

Lean source · statement

theorem KT.of_directed_cover {ι' : Type*} [Nonempty ι'] (N : ι' → Submodule A M)
    (hdir : Directed (· ≤ ·) N) (hcov : ∀ m : M, ∃ i, m ∈ N i) {a : A}
    (h : ∀ i, KT a (N i)) : KT a M

theorem

base_case

L178 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.base_case

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Base
variable [IsDomain A] {M : Type*} [AddCommGroup M] [Module A M] [Module.Finite A M]

Lean source · statement

theorem base_case : ∃ a : A, a ≠ 0 ∧ KT a M

def

filt

L224 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.filt

Documentation

The increasing filtration generated by the images of M' under powers of f up to the given index.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · full declaration

def filt : ℕ → Submodule R M
  | 0 => M'
  | i + 1 => filt i ⊔ M'.map (f ^ (i + 1))

lemma

filt_zero

L228 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.filt_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

lemma filt_zero : filt f M' 0 = M'

lemma

filt_succ

L230 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.filt_succ

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

lemma filt_succ (i : ℕ) : filt f M' (i + 1) = filt f M' i ⊔ M'.map (f ^ (i + 1))

lemma

filt_le_succ

L232 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.filt_le_succ

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

lemma filt_le_succ (i : ℕ) : filt f M' i ≤ filt f M' (i + 1)

lemma

filt_mono

L235 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.filt_mono

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

lemma filt_mono : Monotone (filt f M')

lemma

map_filt_le

L237 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.map_filt_le

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

lemma map_filt_le (i : ℕ) : (filt f M' i).map f ≤ filt f M' (i + 1)

lemma

pow_apply_mem_filt

L250 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.pow_apply_mem_filt

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

lemma pow_apply_mem_filt {i : ℕ} {x : M} (hx : x ∈ filt f M' i) (j : ℕ) :
    (f ^ j) x ∈ filt f M' (i + j)

lemma

pow_apply_mem_filt'

L258 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.pow_apply_mem_filt'

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

lemma pow_apply_mem_filt' (m : M') (j : ℕ) : (f ^ j) (m : M) ∈ filt f M' j

def

K

L263 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.K

Documentation

The submodule of M' whose image under the next power of f lies in the preceding filtration level.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

def K (i : ℕ) : Submodule R M'

lemma

mem_K

L265 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.mem_K

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

lemma mem_K (i : ℕ) (m : M') : m ∈ K f M' i ↔ (f ^ (i + 1)) (m : M) ∈ filt f M' i

lemma

K_mono

L267 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.K_mono

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

lemma K_mono : Monotone (K f M')

abbrev

Gr

L274 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.Gr

Documentation

The quotient of consecutive levels of the filtration generated by f and M'.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

abbrev Gr (i : ℕ)

def

toGr

L277 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.toGr

Documentation

The map from M' to the corresponding filtration quotient induced by the next power of f.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

def toGr (i : ℕ) : M' →ₗ[R] Gr f M' i

lemma

toGr_apply

L282 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.toGr_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

lemma toGr_apply (i : ℕ) (m : M') :
    toGr f M' i m = Submodule.Quotient.mk
      ⟨(f ^ (i + 1)) (m : M), pow_apply_mem_filt' f M' m (i + 1)⟩

lemma

ker_toGr

L287 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.ker_toGr

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

lemma ker_toGr (i : ℕ) : LinearMap.ker (toGr f M' i) = K f M' i

lemma

toGr_surjective

L292 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.toGr_surjective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

lemma toGr_surjective (i : ℕ) : Function.Surjective (toGr f M' i)

def

grEquiv

L303 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.grEquiv

Documentation

The linear equivalence between the quotient by K and the corresponding filtration quotient.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)

Lean source · statement

def grEquiv (i : ℕ) : (M' ⧸ K f M' i) ≃ₗ[R] Gr f M' i

theorem

KT_filt_succ

L311 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.KT_filt_succ

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Filt
variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]
  (f : M →ₗ[R] M) (M' : Submodule R M)
section WithBase
variable [Algebra A R] [Module A M] [IsScalarTower A R M]

Lean source · statement

theorem KT_filt_succ {a : A} (i : ℕ) (ih : KT a (filt f M' i)) (hGr : KT a (Gr f M' i)) :
    KT a (filt f M' (i + 1))

theorem

poly_step

L346 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.poly_step

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Step
universe uM
variable {B' : Type*} [CommRing B'] [Algebra A B'] [IsNoetherianRing B'] [IsDomain A]
open Polynomial in

Lean source · statement

theorem poly_step
    (IH : ∀ (N : Type uM) [AddCommGroup N] [Module A N] [Module B' N] [IsScalarTower A B' N]
      [Module.Finite B' N], ∃ a : A, a ≠ 0 ∧ KT a N)
    (M : Type uM) [AddCommGroup M] [Module A M] [Module B' M] [Module B'[X] M]
    [IsScalarTower A B' M] [IsScalarTower B' B'[X] M] [Module.Finite B'[X] M] :
    ∃ a : A, a ≠ 0 ∧ KT a M

lemma

finite_of_surjective_ringHom

L435 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.finite_of_surjective_ringHom

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Induction
universe uM
variable [IsDomain A] [IsNoetherianRing A]

Lean source · statement

lemma finite_of_surjective_ringHom {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S)
    (hφ : Function.Surjective φ) (M : Type*) [AddCommGroup M] [Module S M] [Module R M]
    (hsmul : ∀ (r : R) (m : M), r • m = φ r • m) [Module.Finite S M] : Module.Finite R M

theorem

mvPolynomial_case

L452 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.mvPolynomial_case

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Induction
universe uM
variable [IsDomain A] [IsNoetherianRing A]

Lean source · statement

theorem mvPolynomial_case (n : ℕ) :
    ∀ (M : Type uM) [AddCommGroup M] [Module A M] [Module (MvPolynomial (Fin n) A) M]
      [IsScalarTower A (MvPolynomial (Fin n) A) M] [Module.Finite (MvPolynomial (Fin n) A) M],
      ∃ a : A, a ≠ 0 ∧ KT a M

theorem

finiteType_case

L481 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.finiteType_case

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Induction
universe uM
variable [IsDomain A] [IsNoetherianRing A]

Lean source · statement

theorem finiteType_case {B : Type*} [CommRing B] [Algebra A B] [Algebra.FiniteType A B]
    (M : Type uM) [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M]
    [Module.Finite B M] : ∃ a : A, a ≠ 0 ∧ KT a M

theorem

flat_of_isLocalizedModule

L500 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.flat_of_isLocalizedModule

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Convert
variable {M M' : Type*} [AddCommGroup M] [Module A M] [AddCommGroup M'] [Module A M']

Lean source · statement

theorem flat_of_isLocalizedModule (S : Submonoid A) (g : M →ₗ[A] M') [IsLocalizedModule S g]
    (h : ∀ (I : Ideal A) (k : M ⊗[A] I), LinearMap.lTensor M I.subtype k = 0 → ∃ s ∈ S, s • k = 0) :
    Module.Flat A M'

theorem

isLocalizedModule_powers

L532 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_Flat_exists_ne_zero_flat_localization_tensorProduct.GenericFlatness.isLocalizedModule_powers

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_Flat_exists_ne_zero_flat_localization_tensorProduct
open TensorProduct
noncomputable section
namespace GenericFlatness
variable {A : Type*} [CommRing A]
section Convert
variable {M M' : Type*} [AddCommGroup M] [Module A M] [AddCommGroup M'] [Module A M']
variable {B : Type*} [CommRing B] [Algebra A B] [Module B M] [IsScalarTower A B M]

Lean source · statement

theorem isLocalizedModule_powers (a : A) :
    IsLocalizedModule (Submonoid.powers a)
      ((TensorProduct.mk B
        (Localization (Submonoid.powers (algebraMap A B a))) M 1).restrictScalars A)

theorem