Module

HomogeneousIdeal_exists_homogeneous_pos_mem_forall_notMem.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HomogeneousIdeal_exists_homogeneous_pos_mem_forall_notMem

4 declarations indexed from sourceView source ↗

Module documentation

Differentials, residues, and divisor correspondences

Homogeneous prime avoidance constructs a positive-degree homogeneous element outside finitely many prime homogeneous ideals.

Imports3

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Mathlib.Tactic.ByContra
Mathlib.Tactic.Choose

Imported by3

theorem

exists_homogeneous_mem_notMem

L48 ↗

Ideal.IsHomogeneous.exists_homogeneous_mem_notMem

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousIdeal_exists_homogeneous_pos_mem_forall_notMem
universe u v
open _root_.DirectSum
open _root_.SetLike
open _root_.DirectSum.SetLike
open _root_.DirectSum
open _root_.SetLike
open _root_.DirectSum.SetLike
namespace Ideal
open _root_.Ideal
namespace IsHomogeneous
open _root_.Ideal.IsHomogeneous
open _root_.Ideal.IsHomogeneous
open _root_.Ideal
variable {A σ : Type*} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜]

Lean source · statement

theorem _root_.Ideal.IsHomogeneous.exists_homogeneous_mem_notMem {I : Ideal A} (hI :
  I.IsHomogeneous 𝒜) {p : Ideal A}
    (h : ¬ I ≤ p) : ∃ (n : ℕ) (x : A), x ∈ 𝒜 n ∧ x ∈ I ∧ x ∉ p

theorem

exists_homogeneous_pos_mem_notMem

L60 ↗

Ideal.IsHomogeneous.exists_homogeneous_pos_mem_notMem

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousIdeal_exists_homogeneous_pos_mem_forall_notMem
universe u v
open _root_.DirectSum
open _root_.SetLike
open _root_.DirectSum.SetLike
open _root_.DirectSum
open _root_.SetLike
open _root_.DirectSum.SetLike
namespace Ideal
open _root_.Ideal
namespace IsHomogeneous
open _root_.Ideal.IsHomogeneous
open _root_.Ideal.IsHomogeneous
open _root_.Ideal
variable {A σ : Type*} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜]
open _root_.Ideal.IsHomogeneous

Lean source · statement

theorem _root_.Ideal.IsHomogeneous.exists_homogeneous_pos_mem_notMem {I : Ideal A} (hI :
  I.IsHomogeneous 𝒜)
    (hirr : I ≤ (HomogeneousIdeal.irrelevant 𝒜).toIdeal) {p : Ideal A} (h : ¬ I ≤ p) :
    ∃ (n : ℕ) (x : A), 0 < n ∧ x ∈ 𝒜 n ∧ x ∈ I ∧ x ∉ p

theorem

exists_homogeneous_pos_mem_forall_notMem

L77 ↗

Ideal.IsHomogeneous.exists_homogeneous_pos_mem_forall_notMem

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousIdeal_exists_homogeneous_pos_mem_forall_notMem
universe u v
open _root_.DirectSum
open _root_.SetLike
open _root_.DirectSum.SetLike
open _root_.DirectSum
open _root_.SetLike
open _root_.DirectSum.SetLike
namespace Ideal
open _root_.Ideal
namespace IsHomogeneous
open _root_.Ideal.IsHomogeneous
open _root_.Ideal.IsHomogeneous
open _root_.Ideal
variable {A σ : Type*} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜]
open _root_.Ideal.IsHomogeneous
open _root_.Ideal.IsHomogeneous

Lean source · statement

theorem _root_.Ideal.IsHomogeneous.exists_homogeneous_pos_mem_forall_notMem {I :
  Ideal A} (hI : I.IsHomogeneous 𝒜)
    (hirr : I ≤ (HomogeneousIdeal.irrelevant 𝒜).toIdeal) (t : Finset (Ideal A))
    (hprime : ∀ p ∈ t, p.IsPrime) (hhom : ∀ p ∈ t, p.IsHomogeneous 𝒜) (havoid : ∀ p ∈ t, ¬ I ≤ p) :
    ∃ (n : ℕ) (x : A), 0 < n ∧ x ∈ 𝒜 n ∧ x ∈ I ∧ ∀ p ∈ t, x ∉ p

theorem

exists_homogeneous_pos_mem_forall_notMem

L149 ↗

HomogeneousIdeal.exists_homogeneous_pos_mem_forall_notMem

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HomogeneousIdeal_exists_homogeneous_pos_mem_forall_notMem
universe u v
open _root_.DirectSum
open _root_.SetLike
open _root_.DirectSum.SetLike
open _root_.DirectSum
open _root_.SetLike
open _root_.DirectSum.SetLike

Lean source · statement

theorem _root_.HomogeneousIdeal.exists_homogeneous_pos_mem_forall_notMem
    {A : Type u} {σ : Type v} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ}
      [GradedRing 𝒜]
    (I : HomogeneousIdeal 𝒜) (hirr : I ≤ HomogeneousIdeal.irrelevant 𝒜)
    (t : Finset (HomogeneousIdeal 𝒜)) (hprime : ∀ p ∈ t, p.toIdeal.IsPrime) (havoid : ∀ p ∈ t,
      ¬ I ≤ p) :
    ∃ (n : ℕ) (x : A), 0 < n ∧ x ∈ 𝒜 n ∧ x ∈ I ∧ ∀ p ∈ t, x ∉ p

Module documentation

Differentials, residues, and divisor correspondences

Declarations

exists_homogeneous_mem_notMem

exists_homogeneous_pos_mem_notMem

exists_homogeneous_pos_mem_forall_notMem

exists_homogeneous_pos_mem_forall_notMem