\import Algebra.Monoid
\import Algebra.Ring.Ideal
\import Data.Array
\import Data.Or
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta

\record HomogenIdeal \extends Ideal {
\override S : GradedCRing
| isHomogenIdeal {l : Array S} : isHomogenArray l -> contains (AddMonoid.BigSum l) -> ∀ (x : l) (contains x)
} \where {
\func hasHomogenGen {R : GradedCRing} (I : Ideal R)
=> \Sigma (U : R -> \Prop) (\Pi (x : R) -> U x -> ∃ (n : Nat) (isHomogen x n)) (\Pi (x : R) -> I x <-> Ideal.sclosure U x)

-- | A homogeneous ideal has a set of homogeneous generators
\func toGen (I : HomogenIdeal) : hasHomogenGen I
=> \let U x => ∃ (l : Array S) (isHomogenArray l) (i : Fin l.len) (l i = x) (I (BigSum l))
\in (U, \lam x => TruncP.map __ \lam (l,f,n,p,c) => (n, rewriteI p (f n)),
\lam x => (\lam Ix => TruncP.map (homogen-decomp x) \lam (l,f,p) => (mkArray \lam j => later (1, (l j, inP (l, f, j, idp, rewrite p Ix))), inv p *> pmap BigSum (exts \lam j => inv ide-left)),
Ideal.sclosure-univ $later \lam y (inP (l,f,i,p,c)) => transport I p (isHomogenIdeal f c i))) -- | If an ideal has a set of homogeneous generators, then it is homogeneous \func fromGen {R : GradedCRing} (I : Ideal R) (h : TruncP (hasHomogenGen I)) : HomogenIdeal \cowith | Ideal => I | isHomogenIdeal {l} lh s j => \have | (inP H) => h | (inP (l',p)) => (H.3 (BigSum l)).1 s | (inP (N,f,q)) => sum-decomp (map (\lam s => (s.1,s.2.1)) l') (\lam i => H.2 (l' i).2.1 (l' i).2.2) \in \case similar-eq (R.homogen-similar lh (\lam n => homogen-FinSum$ (f n).5) (p *> q)) j \with {
| inl r => transportInv I r.2 $finSum \lam k => later$ ideal-left $(H.3 _).2$ Ideal.sclosure-superset (l' _).2.2
| inr r => transportInv I r contains_zro
}
}

\func irrelevantIdeal (R : GradedCRing) : HomogenIdeal R
=> HomogenIdeal.fromGen (Ideal.sclosure (\lam x => ∃ (n : Nat) (isHomogen x (suc n)))) \$
inP (\lam x => ∃ (n : Nat) (isHomogen x (suc n)), \lam x => TruncP.map __ \lam (n,h) => (suc n, h), \lam x => (\lam c => c, \lam c => c))