Module

Ideal_height_eq_height_under_of_isIntegrallyClosed_of_isIntegral.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_height_eq_height_under_of_isIntegrallyClosed_of_isIntegral

3 declarations indexed from sourceView source ↗

Module documentation

Ideal height eq height under of is Integrally Closed of is Integral

Imports2

Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Mathlib.RingTheory.IntegralClosure.GoingDown

Imported by2

theorem

eq_of_le_of_under_eq

L29 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_height_eq_height_under_of_isIntegrallyClosed_of_isIntegral.HeightAux.eq_of_le_of_under_eq

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_height_eq_height_under_of_isIntegrallyClosed_of_isIntegral
universe u
namespace HeightAux

Lean source · statement

theorem eq_of_le_of_under_eq {P B : Type*} [CommRing P] [CommRing B] [Algebra P B]
    [Algebra.IsIntegral P B] {Q q : Ideal B} [Q.IsPrime] [q.IsPrime] (hle : Q ≤ q)
    (hu : q.under P ≤ Q.under P) : Q = q

theorem

height_eq_height_under

L39 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_height_eq_height_under_of_isIntegrallyClosed_of_isIntegral.HeightAux.height_eq_height_under

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_height_eq_height_under_of_isIntegrallyClosed_of_isIntegral
universe u
namespace HeightAux

Lean source · statement

theorem height_eq_height_under (P B : Type*) [CommRing P] [IsDomain P] [IsNoetherianRing P]
    [IsIntegrallyClosed P] [CommRing B] [IsDomain B] [IsNoetherianRing B] [Algebra P B]
    [FaithfulSMul P B] [Algebra.IsIntegral P B] (q : Ideal B) [q.IsPrime] :
    q.height = (q.under P).height

theorem

height_eq_height_under_of_isIntegrallyClosed_of_isIntegral

L73 ↗

Ideal.height_eq_height_under_of_isIntegrallyClosed_of_isIntegral

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_height_eq_height_under_of_isIntegrallyClosed_of_isIntegral
universe u

Lean source · statement

theorem _root_.Ideal.height_eq_height_under_of_isIntegrallyClosed_of_isIntegral
    (P B : Type u) [CommRing P] [IsDomain P] [IsNoetherianRing P] [IsIntegrallyClosed P]
    [CommRing B] [IsDomain B] [IsNoetherianRing B] [Algebra P B] [FaithfulSMul P B]
    [Algebra.IsIntegral P B] (q : Ideal B) [q.IsPrime] :
    q.height = (q.under P).height

Module documentation

Ideal height eq height under of is Integrally Closed of is Integral

Declarations

eq_of_le_of_under_eq

height_eq_height_under

height_eq_height_under_of_isIntegrallyClosed_of_isIntegral