Module

Module_flat_of_maximalIdeal_rTensor_injective_of_isLocalHom.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_flat_of_maximalIdeal_rTensor_injective_of_isLocalHom

7 declarations indexed from sourceView source ↗

Module documentation

Module flat of maximal Ideal r Tensor injective of is Local Hom

Imports10

Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.Flat.Tensor
Mathlib.RingTheory.Filtration
Mathlib.LinearAlgebra.TensorProduct.RightExactness
Mathlib.LinearAlgebra.TensorProduct.Map
Mathlib.LinearAlgebra.Span.Basic
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Finiteness.Basic
Mathlib.Tactic.Abel

Imported by2

theorem

inj_subtype_of_le

L42 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_maximalIdeal_rTensor_injective_of_isLocalHom.LCF.inj_subtype_of_le

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_maximalIdeal_rTensor_injective_of_isLocalHom
open TensorProduct IsLocalRing
universe u
namespace LCF
variable {A : Type u} [CommRing A] [IsLocalRing A]
variable (M : Type u) [AddCommGroup M] [Module A M]

Lean source · statement

theorem inj_subtype_of_le (h𝔪 : Function.Injective (LinearMap.lTensor M (maximalIdeal A).subtype))
    (J : Ideal A) (hJ : maximalIdeal A ≤ J) : Function.Injective (LinearMap.lTensor M J.subtype)

theorem

inj_of_bijective

L54 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_maximalIdeal_rTensor_injective_of_isLocalHom.LCF.inj_of_bijective

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_maximalIdeal_rTensor_injective_of_isLocalHom
open TensorProduct IsLocalRing
universe u
namespace LCF
variable {A : Type u} [CommRing A] [IsLocalRing A]
variable (M : Type u) [AddCommGroup M] [Module A M]
omit [IsLocalRing A] in

Lean source · statement

theorem inj_of_bijective {P Q : Type u} [AddCommGroup P] [Module A P] [AddCommGroup Q] [Module A Q]
    (f : P →ₗ[A] Q) (hf : Function.Bijective f) : Function.Injective (LinearMap.lTensor M f)

theorem

alpha

L60 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_maximalIdeal_rTensor_injective_of_isLocalHom.LCF.alpha

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_maximalIdeal_rTensor_injective_of_isLocalHom
open TensorProduct IsLocalRing
universe u
namespace LCF
variable {A : Type u} [CommRing A] [IsLocalRing A]
variable (M : Type u) [AddCommGroup M] [Module A M]

Lean source · statement

theorem alpha (h𝔪 : Function.Injective (LinearMap.lTensor M (maximalIdeal A).subtype))
    {P : Type u} [AddCommGroup P] [Module A P] (Q Q'' : Submodule A P) (p : P) (hQ : Q ≤ Q'')
    (hQ'' : Q'' = Q ⊔ Submodule.span A {p}) (hp : ∀ a ∈ maximalIdeal A, a • p ∈ Q) :
    Function.Injective (LinearMap.lTensor M (Submodule.inclusion hQ))

theorem

beta

L123 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_maximalIdeal_rTensor_injective_of_isLocalHom.LCF.beta

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_maximalIdeal_rTensor_injective_of_isLocalHom
open TensorProduct IsLocalRing
universe u
namespace LCF
variable {A : Type u} [CommRing A] [IsLocalRing A]
variable (M : Type u) [AddCommGroup M] [Module A M]

Lean source · statement

theorem beta (h𝔪 : Function.Injective (LinearMap.lTensor M (maximalIdeal A).subtype))
    {P' P : Type u} [AddCommGroup P'] [Module A P'] [AddCommGroup P] [Module A P] [Module.Finite A
      P]
    (u : P' →ₗ[A] P) (hu : Function.Injective u)
    (h𝔪P : ∀ a ∈ maximalIdeal A, ∀ x : P, a • x ∈ LinearMap.range u) :
    Function.Injective (LinearMap.lTensor M u)

theorem

gamma

L169 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_maximalIdeal_rTensor_injective_of_isLocalHom.LCF.gamma

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_maximalIdeal_rTensor_injective_of_isLocalHom
open TensorProduct IsLocalRing
universe u
namespace LCF
variable {A : Type u} [CommRing A] [IsLocalRing A]
variable (M : Type u) [AddCommGroup M] [Module A M]

Lean source · statement

theorem gamma [IsNoetherianRing A] (h𝔪 : Function.Injective (LinearMap.lTensor M (maximalIdeal
  A).subtype)) (n : ℕ) :
    ∀ (N : Type u) [AddCommGroup N] [Module A N] [Module.Finite A N],
      (maximalIdeal A) ^ n • (⊤ : Submodule A N) = ⊥ →
      ∀ (N' : Type u) [AddCommGroup N'] [Module A N'] (u : N' →ₗ[A] N), Function.Injective u →
        Function.Injective (LinearMap.lTensor M u)

theorem

finite_tensor

L247 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_flat_of_maximalIdeal_rTensor_injective_of_isLocalHom.LCF.finite_tensor

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_maximalIdeal_rTensor_injective_of_isLocalHom
open TensorProduct IsLocalRing
universe u
namespace LCF

Lean source · statement

theorem finite_tensor {A B : Type u} [CommRing A] [CommRing B] [Algebra A B]
    (M : Type u) [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M] [Module.Finite B
      M]
    (I : Type u) [AddCommGroup I] [Module A I] [Module.Finite A I] :
    Module.Finite B (M ⊗[A] I)

theorem

flat_of_maximalIdeal_rTensor_injective_of_isLocalHom

L292 ↗

Module.flat_of_maximalIdeal_rTensor_injective_of_isLocalHom

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Module_flat_of_maximalIdeal_rTensor_injective_of_isLocalHom
open TensorProduct IsLocalRing
universe u
open LCF in

Lean source · statement

theorem _root_.Module.flat_of_maximalIdeal_rTensor_injective_of_isLocalHom
    {A B : Type u} [CommRing A] [CommRing B] [IsNoetherianRing A] [IsNoetherianRing B] [IsLocalRing
      A] [IsLocalRing B]
    [Algebra A B] [IsLocalHom (algebraMap A B)]
    (M : Type u) [AddCommGroup M] [Module A M] [Module B M] [IsScalarTower A B M] [Module.Finite B
      M]
    (h : Function.Injective (LinearMap.rTensor M (maximalIdeal A).subtype)) :
    Module.Flat A M

Module documentation

Module flat of maximal Ideal r Tensor injective of is Local Hom

Declarations

inj_subtype_of_le

inj_of_bijective

alpha

beta

gamma

finite_tensor

flat_of_maximalIdeal_rTensor_injective_of_isLocalHom