IntegralCover.lean

theorem mapRingHom_isIntegral
    {A B M : Type*} [CommRing A] [CommRing B] [AddCommMonoid M]
    (f : A →+* B) (hf : f.IsIntegral) :
    (AddMonoidAlgebra.mapRingHom M f).IsIntegral

theorem nestedDiagonalRadicalBase_isIntegral
    {R : Type u} [CommRing R] :
    ∀ {r : ℕ} (n : Fin r → ℕ), (∀ i, 0 < n i) →
      (nestedDiagonalRadicalBase R r n).IsIntegral
  | 0, _, _ => fun x ↦ (RingHom.id R).isIntegralElem_map
  | r + 1, n, hn => by
      let nInit : Fin r → ℕ := Fin.init n
      let nLast : ℕ := n (Fin.last r)
      let T₀ := nestedDiagonalRadical R r nInit
      let A := AddMonoidAlgebra T₀ ℤ
      let uA : A := AddMonoidAlgebra.single (1 : ℤ) (1 : T₀)
      let pA : A[X] := X ^ nLast - C uA
      have hInit :
          (nestedDiagonalRadicalBase R r nInit).IsIntegral :=
        nestedDiagonalRadicalBase_isIntegral nInit
          (fun i ↦ hn i.castSucc)
      have hMap :
          (AddMonoidAlgebra.mapRingHom ℤ
            (nestedDiagonalRadicalBase R r nInit)).IsIntegral :=
        mapRingHom_isIntegral _ hInit
      have hpA : pA.Monic :=
        Polynomial.monic_X_pow_sub_C uA (hn (Fin.last r)).ne'
      let : Module.Finite A (AdjoinRoot pA) := hpA.finite_adjoinRoot
      have hRoot : (AdjoinRoot.of pA).IsIntegral :=
        (RingHom.finite_algebraMap.mpr inferInstance).to_isIntegral
      exact hMap.trans _ _ hRoot

theorem finDiagonalRadicalBase_isIntegral
    {R : Type u} [CommRing R] {r : ℕ} (n : Fin r → ℕ)
    (hn : ∀ i, 0 < n i) :
    (finDiagonalRadicalBase R n).IsIntegral

theorem latticeMonoidAlgebraMap_isIntegral
    {R L : Type u} [CommRing R] [AddCommGroup L]
    [Module.Free ℤ L] [Module.Finite ℤ L]
    (H : Submodule ℤ L) [Finite (L ⧸ H)] :
    (AddMonoidAlgebra.mapDomainRingHom R
      H.subtype.toAddMonoidHom).IsIntegral