Commit 2022-02-23 14:40 0d5bed0e

View on Github →

feat(ring_theory/graded_algebra): definitions and basic operations of homogeneous ideal (#10784) This defines homogeneous ideals (homogeneous_ideal) of a graded algebra.

Estimated changes

Modified src/algebra/graded_monoid.lean

added theorem set_like.is_homogeneous_coe

Created src/ring_theory/graded_algebra/homogeneous_ideal.lean

added theorem homogeneous_ideal.coe_Inf

added theorem homogeneous_ideal.coe_Sup

added theorem homogeneous_ideal.coe_add

added theorem homogeneous_ideal.coe_bot

added theorem homogeneous_ideal.coe_inf

added theorem homogeneous_ideal.coe_infi

added theorem homogeneous_ideal.coe_mul

added theorem homogeneous_ideal.coe_sup

added theorem homogeneous_ideal.coe_supr

added theorem homogeneous_ideal.coe_top

added theorem homogeneous_ideal.eq_bot_iff

added theorem homogeneous_ideal.eq_top_iff

added theorem homogeneous_ideal.homogeneous_core_coe_eq_self

added theorem homogeneous_ideal.homogeneous_hull_coe_eq_self

added def homogeneous_ideal

added theorem ideal.coe_homogeneous_core_le

added theorem ideal.coe_homogeneous_hull_eq_supr

added def ideal.homogeneous_core'

added theorem ideal.homogeneous_core'_eq_Sup

added theorem ideal.homogeneous_core'_le

added theorem ideal.homogeneous_core'_mono

added theorem ideal.homogeneous_core.gc

added def ideal.homogeneous_core.gi

added def ideal.homogeneous_core

added theorem ideal.homogeneous_core_eq_Sup

added theorem ideal.homogeneous_core_mono

added theorem ideal.homogeneous_hull.gc

added def ideal.homogeneous_hull.gi

added def ideal.homogeneous_hull

added theorem ideal.homogeneous_hull_eq_Inf

added theorem ideal.homogeneous_hull_eq_supr

added theorem ideal.homogeneous_hull_mono

added theorem ideal.is_homogeneous.Inf

added theorem ideal.is_homogeneous.Sup

added theorem ideal.is_homogeneous.bot

added theorem ideal.is_homogeneous.coe_homogeneous_core_eq_self

added theorem ideal.is_homogeneous.homogeneous_hull_eq_self

added theorem ideal.is_homogeneous.iff_eq

added theorem ideal.is_homogeneous.iff_exists

added theorem ideal.is_homogeneous.inf

added theorem ideal.is_homogeneous.mul

added theorem ideal.is_homogeneous.sup

added theorem ideal.is_homogeneous.top

added def ideal.is_homogeneous

added theorem ideal.is_homogeneous_iff_forall_subset

added theorem ideal.is_homogeneous_iff_subset_Inter

added theorem ideal.is_homogeneous_span

added theorem ideal.le_coe_homogeneous_hull

added theorem ideal.mul_homogeneous_element_mem_of_mem

Modified src/ring_theory/ideal/basic.lean

added theorem ideal.mem_span

added theorem ideal.span_Union

added theorem ideal.span_empty

added theorem ideal.span_union

added theorem ideal.span_univ

added theorem ideal.sum_mem