Fix typechecking

JetBrains · May 7, 2024 · 2becf66 · 2becf66
1 parent f663a47
commit 2becf66
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 32 deletions.
diff --git a/src/Algebra/Field/Splitting.ard b/src/Algebra/Field/Splitting.ard
@@ -44,40 +44,40 @@
       | greater q => absurd $ K.zro/=ide $ pmap (polyCoef __ n) {pzero} (inv $ lq *> pmap (PolyRing.`*c _) (inv pc2 *> degree<=.toCoefs _ _ (degree<=_polyMap pd) q) *> PolyRing.zro_*c) *> pc1
     }) *> PolyRing.ide_*c)
 
-\private \record RootFieldData (P : DiscreteField -> \Set) (k : DiscreteField) (p : Poly k)
-  | RootField : DiscreteField
-  | RootFieldP : P RootField
-  | rootFieldHom : RingHom k RootField
-  | root : RootField
-  | isRoot : polyMapEval rootFieldHom p root = 0
-  | RootField-gen (x : RootField) : ∃ (q : Poly k) (polyMapEval rootFieldHom q root = x)
+\sfunc countableSplittingField {k : DiscreteField} (c : Countable k) {p : Poly k} : \Sigma (K : DiscreteField) (Countable K) (f : RingHom k K) (IsSplittingField p f)
+  => CountableSplittingFieldData.makeSplittingField c ()
+  \where \protected {
+    \record RootFieldData (P : DiscreteField -> \Set) (k : DiscreteField) (p : Poly k)
+      | RootField : DiscreteField
+      | RootFieldP : P RootField
+      | rootFieldHom : RingHom k RootField
+      | root : RootField
+      | isRoot : polyMapEval rootFieldHom p root = 0
+      | RootField-gen (x : RootField) : ∃ (q : Poly k) (polyMapEval rootFieldHom q root = x)
 
-\private \class SplittingFieldData \noclassifying
-  (P : DiscreteField -> \Set) (S : \Pi {K : DiscreteField} -> Poly K -> \Prop)
-  (S-hom : \Pi {K K' : DiscreteField} (f : RingHom K K') {p : Poly K} -> S p -> S (polyMap f p))
-  (S-factor : \Pi {K : DiscreteField} {p q : Poly K} -> S (p * q) -> S p)
-  (nextField : \Pi {K : DiscreteField} {p : Poly K} -> P K -> p /= 0 -> Not (Inv p) -> RootFieldData P K p) {
+    \class SplittingFieldData \noclassifying
+      (P : DiscreteField -> \Set) (S : \Pi {K : DiscreteField} -> Poly K -> \Prop)
+      (S-hom : \Pi {K K' : DiscreteField} (f : RingHom K K') {p : Poly K} -> S p -> S (polyMap f p))
+      (S-factor : \Pi {K : DiscreteField} {p q : Poly K} -> S (p * q) -> S p)
+      (nextField : \Pi {K : DiscreteField} {p : Poly K} -> P K -> p /= 0 -> Not (Inv p) -> RootFieldData P K p) {
 
-  \func makeSplittingField {k : DiscreteField} (Pk : P k) {p : Poly k} (Sp : S p) : \Sigma (K : DiscreteField) (P K) (f : RingHom k K) (IsSplittingField p f)
-    => aux Pk idp Sp
-    \where
-      \func aux {k : DiscreteField} (Pk : P k) {p : Poly k} {n : Nat} (d : degree p = n) (Sp : S p) : \Sigma (K : DiscreteField) (P K) (f : RingHom k K) (IsSplittingField p f) \elim n
-        | 0 => (k, Pk, RingCat.id k, inP (nil, polyCoef p 0, \lam x => inP (mConst x, simplify), rewrite {1} (degree=0-lem d) $ pmap (padd pzero) $ leadCoef_polyCoef *> pmap (polyCoef p) d *> inv ide-right))
-        | suc n => \let | p/=0 : p /= 0 => \case rewrite __ in d
-                        | rfd : RootFieldData P k p => nextField Pk p/=0 \lam pi => \case polyInv pi \with {
-                                                         | inP (r,q,_) => \case rewrite q in d
-                                                       }
-                        | (K,PK,f,Ks) => aux rfd.RootFieldP {_} {n} (pmap pred (inv (rewrite (decideEq/=_reduce $ /=-sym zro/=ide) in inv (degree_polyMap RingHom.field-isInj) *> degree_*_= (\lam q => p/=0 $ polyMap-inj RingHom.field-isInj q) (rootDiv_* rfd.isRoot)) *> d)) $ S-factor $ transport S (rootDiv_* rfd.isRoot) (S-hom rfd.rootFieldHom Sp)
-                   \in (K, PK, f RingCat.∘ rfd.rootFieldHom, TruncP.map Ks \lam (l,c,fl,q) => later
-                        (f rfd.root :: l, c, RingHom.isAlgebraGenerated-comp rfd.RootField-gen fl,
-                         inv (polyMap-comp rfd.rootFieldHom f) *> pmap (polyMap f) (rootDiv_* rfd.isRoot) *> func-* {polyMapRingHom f} *> pmap (`* _) q *> inv PolyRing.*c-comm-left *>
-                         pmap (c PolyRing.*c) (pmap (_ *) (pmap2 (\lam x y => padd (padd pzero x) y) func-ide AddGroupHom.func-negative) *> *-comm {_} {_} {padd 1 (negative (f root))})))
-}
+      \func makeSplittingField {k : DiscreteField} (Pk : P k) {p : Poly k} (Sp : S p) : \Sigma (K : DiscreteField) (P K) (f : RingHom k K) (IsSplittingField p f)
+        => aux Pk idp Sp
+        \where
+          \func aux {k : DiscreteField} (Pk : P k) {p : Poly k} {n : Nat} (d : degree p = n) (Sp : S p) : \Sigma (K : DiscreteField) (P K) (f : RingHom k K) (IsSplittingField p f) \elim n
+            | 0 => (k, Pk, RingCat.id k, inP (nil, polyCoef p 0, \lam x => inP (mConst x, simplify), rewrite {1} (degree=0-lem d) $ pmap (padd pzero) $ leadCoef_polyCoef *> pmap (polyCoef p) d *> inv ide-right))
+            | suc n => \let | p/=0 : p /= 0 => \case rewrite __ in d
+                            | rfd : RootFieldData P k p => nextField Pk p/=0 \lam pi => \case polyInv pi \with {
+                                                             | inP (r,q,_) => \case rewrite q in d
+                                                           }
+                            | (K,PK,f,Ks) => aux rfd.RootFieldP {_} {n} (pmap pred (inv (rewrite (decideEq/=_reduce $ /=-sym zro/=ide) in inv (degree_polyMap RingHom.field-isInj) *> degree_*_= (\lam q => p/=0 $ polyMap-inj RingHom.field-isInj q) (rootDiv_* rfd.isRoot)) *> d)) $ S-factor $ transport S (rootDiv_* rfd.isRoot) (S-hom rfd.rootFieldHom Sp)
+                       \in (K, PK, f RingCat.∘ rfd.rootFieldHom, TruncP.map Ks \lam (l,c,fl,q) => later
+                            (f rfd.root :: l, c, RingHom.isAlgebraGenerated-comp rfd.RootField-gen fl,
+                             inv (polyMap-comp rfd.rootFieldHom f) *> pmap (polyMap f) (rootDiv_* rfd.isRoot) *> func-* {polyMapRingHom f} *> pmap (`* _) q *> inv PolyRing.*c-comm-left *>
+                             pmap (c PolyRing.*c) (pmap (_ *) (pmap2 (\lam x y => padd (padd pzero x) y) func-ide AddGroupHom.func-negative) *> *-comm {_} {_} {padd 1 (negative (f root))})))
+    }
 
-\sfunc countableSplittingField {k : DiscreteField} (c : Countable k) {p : Poly k} : \Sigma (K : DiscreteField) (Countable K) (f : RingHom k K) (IsSplittingField p f)
-  => CountableSplittingFieldData.makeSplittingField c ()
-  \where {
-    \private \func CountableSplittingFieldData : SplittingFieldData \cowith
+    \func CountableSplittingFieldData : SplittingFieldData \cowith
       | P K => Countable K
       | S _ => \Sigma
       | S-hom _ _ => ()

diff --git a/src/Algebra/Ring/MPoly.ard b/src/Algebra/Ring/MPoly.ard
@@ -173,7 +173,7 @@
 
     \func retHom : RingHom (PolyRing (MPoly (Fin n) R)) (MPoly (Fin (suc n)) R) ret \cowith
       | func-zro => idp
-      | func-+ {p q : Poly (MPoly (Fin n) R)} : ret (p + q) = ret p + ret q \with {
+      | func-+ {p q : Poly (MPoly (Fin n) R)} : ret (p + q) = ret p + ret q \elim p, q {
         | pzero, q => inv zro-left
         | padd p a, pzero => inv zro-right
         | padd p a, padd q b => rewrite func-+ $ rewrite (AddMonoidHom.func-+ {monoidSet-hom (permSet-map fsuc) (id R)}) (equation {Ring})