NYLL
Module

IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring
6 declarations indexed from sourceView source ↗

Module documentation

Is Local Ring is Reduced quotient map of flat of locally Principal Overring

Imports13
  • Mathlib.RingTheory.Filtration
  • Mathlib.RingTheory.Flat.Tensor
  • Mathlib.RingTheory.Ideal.GoingUp
  • Mathlib.RingTheory.LocalProperties.Reduced
  • Mathlib.RingTheory.Localization.Submodule
  • Mathlib.RingTheory.Localization.AtPrime.Basic
  • Mathlib.RingTheory.TensorProduct.Finite
  • Mathlib.RingTheory.TensorProduct.Quotient
  • Mathlib.RingTheory.Noetherian.Basic
  • Mathlib.RingTheory.FiniteType
  • Mathlib.Tactic.Push
  • Mathlib.Tactic.Ring
  • Mathlib.Tactic.Abel
Imported by1

Declarations

theorem

isReduced_of_maximalIdeal_eq_span

L40 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring.R1AF8H1.isReduced_of_maximalIdeal_eq_span
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring
open IsLocalRing TensorProduct
namespace R1AF8H1
Lean source · statement
theorem isReduced_of_maximalIdeal_eq_span {L : Type*} [CommRing L] [IsLocalRing L]
  [IsNoetherianRing L]
    (τ : L) (hτ : maximalIdeal L = Ideal.span {τ}) (hreg : τ = 0 ∨ τ ∈ nonZeroDivisors L) :
    IsReduced L
theorem

tmul_one_mem_nonZeroDivisors

L95 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring.R1AF8H1.tmul_one_mem_nonZeroDivisors
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring
open IsLocalRing TensorProduct
namespace R1AF8H1
section Main
variable {A B D₁ : Type*} [CommRing A] [IsLocalRing A] [CommRing B] [IsLocalRing B]
  [IsNoetherianRing B]
  [Algebra A B] [Module.Flat A B]
  [CommRing D₁] [IsDomain D₁] [Algebra A D₁] [Module.Finite A D₁]
omit [IsLocalRing A] [IsLocalRing B] [IsNoetherianRing B] [Module.Finite A D₁] in
Lean source · statement
theorem tmul_one_mem_nonZeroDivisors (t : D₁) (ht : t ≠ 0) :
    ((1 : B) ⊗ₜ[A] t) ∈ nonZeroDivisors (B ⊗[A] D₁)
theorem

exists_sub_tmul_mem

L117 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring.R1AF8H1.exists_sub_tmul_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring
open IsLocalRing TensorProduct
namespace R1AF8H1
section Main
variable {A B D₁ : Type*} [CommRing A] [IsLocalRing A] [CommRing B] [IsLocalRing B]
  [IsNoetherianRing B]
  [Algebra A B] [Module.Flat A B]
  [CommRing D₁] [IsDomain D₁] [Algebra A D₁] [Module.Finite A D₁]
variable (hmax : (maximalIdeal A).map (algebraMap A B) = maximalIdeal B)
  (hres : ∀ b : B, ∃ a : A, b - algebraMap A B a ∈ maximalIdeal B)
omit [IsLocalRing A] [IsNoetherianRing B] [Module.Flat A B] [IsDomain D₁] [Module.Finite A D₁] in
include hres in
Lean source · statement
theorem exists_sub_tmul_mem (J : Ideal (B ⊗[A] D₁))
    (hJ : ∀ m ∈ maximalIdeal B, ∀ d : D₁, m ⊗ₜ[A] d ∈ J) (x : B ⊗[A] D₁) :
    ∃ d : D₁, x - (1 : B) ⊗ₜ[A] d ∈ J
theorem

isReduced_localization_tensor

L137 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring.R1AF8H1.isReduced_localization_tensor
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring
open IsLocalRing TensorProduct
namespace R1AF8H1
section Main
variable {A B D₁ : Type*} [CommRing A] [IsLocalRing A] [CommRing B] [IsLocalRing B]
  [IsNoetherianRing B]
  [Algebra A B] [Module.Flat A B]
  [CommRing D₁] [IsDomain D₁] [Algebra A D₁] [Module.Finite A D₁]
variable (hmax : (maximalIdeal A).map (algebraMap A B) = maximalIdeal B)
  (hres : ∀ b : B, ∃ a : A, b - algebraMap A B a ∈ maximalIdeal B)
include hmax hres in
Lean source · statement
theorem isReduced_localization_tensor
    (hloc : ∀ 𝔫 : Ideal D₁, 𝔫.IsMaximal → ∃ t ∈ 𝔫, ∀ x ∈ 𝔫, ∃ s ∉ 𝔫, ∃ y : D₁, s * x = t * y)
    (𝔑 : Ideal (B ⊗[A] D₁)) [h𝔑 : 𝔑.IsMaximal] :
    IsReduced (Localization.AtPrime 𝔑)
theorem

isReduced_quotient_map

L269 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring.R1AF8H1.isReduced_quotient_map
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring
open IsLocalRing TensorProduct
namespace R1AF8H1
section Main
variable {A B D₁ : Type*} [CommRing A] [IsLocalRing A] [CommRing B] [IsLocalRing B]
  [IsNoetherianRing B]
  [Algebra A B] [Module.Flat A B]
  [CommRing D₁] [IsDomain D₁] [Algebra A D₁] [Module.Finite A D₁]
variable (hmax : (maximalIdeal A).map (algebraMap A B) = maximalIdeal B)
  (hres : ∀ b : B, ∃ a : A, b - algebraMap A B a ∈ maximalIdeal B)
include hmax hres in
Lean source · statement
theorem isReduced_quotient_map
    (hloc : ∀ 𝔫 : Ideal D₁, 𝔫.IsMaximal → ∃ t ∈ 𝔫, ∀ x ∈ 𝔫, ∃ s ∉ 𝔫, ∃ y : D₁, s * x = t * y)
    (𝔭 : Ideal A) (hker : RingHom.ker (algebraMap A D₁) = 𝔭) :
    IsReduced (B ⧸ 𝔭.map (algebraMap A B))
theorem

isReduced_quotient_map_of_flat_of_locallyPrincipalOverring

L316 ↗
IsLocalRing.isReduced_quotient_map_of_flat_of_locallyPrincipalOverring
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_isReduced_quotient_map_of_flat_of_locallyPrincipalOverring
open IsLocalRing TensorProduct
open IsLocalRing in
Lean source · statement
theorem _root_.IsLocalRing.isReduced_quotient_map_of_flat_of_locallyPrincipalOverring
    {A B D₁ : Type*} [CommRing A] [IsLocalRing A] [CommRing B] [IsLocalRing B] [IsNoetherianRing B]
    [Algebra A B] [Module.Flat A B]
    (hmax : (IsLocalRing.maximalIdeal A).map (algebraMap A B) = IsLocalRing.maximalIdeal B)
    (hres : ∀ b : B, ∃ a : A, b - algebraMap A B a ∈ IsLocalRing.maximalIdeal B)
    [CommRing D₁] [IsDomain D₁] [Algebra A D₁] [Module.Finite A D₁]
    (hloc : ∀ 𝔫 : Ideal D₁, 𝔫.IsMaximal → ∃ t ∈ 𝔫, ∀ x ∈ 𝔫, ∃ s ∉ 𝔫, ∃ y : D₁, s * x = t * y)
    (𝔭 : Ideal A) (hker : RingHom.ker (algebraMap A D₁) = 𝔭) :
    IsReduced (B ⧸ 𝔭.map (algebraMap A B))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.