Toric ideals

This file defines toric ideals.

def AddMonoidAlgebra.monoidIdeal {M : Type u_1} {G : Type u_2} {R : Type u_3} [AddCommMonoid M] [AddCommGroup G] (f : ⊤.LocalizationMap G) (s : AddSubmonoid G) [CommRing R] : Ideal (AddMonoidAlgebra R M)

The monoid ideal corresponding to a submonoid s of the Grothendieck group of a monoid is an ideal generated by binomials whose exponents differ by an element of s.

Equations

• One or more equations did not get rendered due to their size.

theorem AddMonoidAlgebra.monoidIdeal_comap {M : Type u_1} {G : Type u_2} {R : Type u_3} {H : Type u_5} [AddCommMonoid M] [AddCommGroup G] [AddCommGroup H] (f : ⊤.LocalizationMap G) (g : ⊤.LocalizationMap H) (s : AddSubmonoid G) [CommRing R] : monoidIdeal g (AddSubmonoid.comap (g.addEquivOfLocalizations f) s) = monoidIdeal f s

class AddMonoidAlgebra.IsToricIdeal {M : Type u_1} {R : Type u_3} [AddCommMonoid M] [CommRing R] (I : Ideal (AddMonoidAlgebra R M)) extends I.IsPrime : Prop

An ideal is toric if it's prime and a group ideal.

• ne_top' : I ≠ ⊤
• mem_or_mem' {x y : AddMonoidAlgebra R M} : x * y ∈ I → x ∈ I ∨ y ∈ I
• exists_monoidIdeal_eq' : ∃ (s : AddSubgroup (AddLocalization ⊤)), monoidIdeal (AddLocalization.addMonoidOf ⊤) s.toAddSubmonoid = I

  Use IsToricIdeal.exists_monoidIdeal_eq instead.

theorem AddMonoidAlgebra.isToricIdeal_iff_exists_monoidIdeal_eq' {M : Type u_1} {R : Type u_3} [AddCommMonoid M] [CommRing R] (I : Ideal (AddMonoidAlgebra R M)) : IsToricIdeal I ↔ I.IsPrime ∧ ∃ (s : AddSubgroup (AddLocalization ⊤)), monoidIdeal (AddLocalization.addMonoidOf ⊤) s.toAddSubmonoid = I

theorem AddMonoidAlgebra.isToricIdeal_iff_exists_monoidIdeal_eq {M : Type u_1} {G : Type u_2} {R : Type u_3} [AddCommMonoid M] [AddCommGroup G] (f : ⊤.LocalizationMap G) [CommRing R] {I : Ideal (AddMonoidAlgebra R M)} : IsToricIdeal I ↔ I.IsPrime ∧ ∃ (s : AddSubgroup G), monoidIdeal f s.toAddSubmonoid = I

theorem AddMonoidAlgebra.IsToricIdeal.of_exists_monoidIdeal_eq {M : Type u_1} {G : Type u_2} {R : Type u_3} [AddCommMonoid M] [AddCommGroup G] (f : ⊤.LocalizationMap G) [CommRing R] {I : Ideal (AddMonoidAlgebra R M)} : (I.IsPrime ∧ ∃ (s : AddSubgroup G), monoidIdeal f s.toAddSubmonoid = I) → IsToricIdeal I

Alias of the reverse direction of AddMonoidAlgebra.isToricIdeal_iff_exists_monoidIdeal_eq.

theorem AddMonoidAlgebra.IsToricIdeal.exists_monoidIdeal_eq {M : Type u_1} {G : Type u_2} {R : Type u_3} [AddCommMonoid M] [AddCommGroup G] (f : ⊤.LocalizationMap G) [CommRing R] {I : Ideal (AddMonoidAlgebra R M)} : IsToricIdeal I → I.IsPrime ∧ ∃ (s : AddSubgroup G), monoidIdeal f s.toAddSubmonoid = I

Alias of the forward direction of AddMonoidAlgebra.isToricIdeal_iff_exists_monoidIdeal_eq.

theorem AddMonoidAlgebra.isToricIdeal_iff_exists_span_single_sub_single {M : Type u_1} {k : Type u_4} [AddCommMonoid M] [Field k] [IsAlgClosed k] {I : Ideal (AddMonoidAlgebra k M)} : IsToricIdeal I ↔ I.IsPrime ∧ ∃ (s : Set (M × M)), Ideal.span ((fun (x : M × M) => match x with | (a, b) => single a 1 - single b 1) '' s) = I