FiniteCover.lean

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

theorem nestedDiagonalRadicalBase_isFinite
    {R : Type u} [CommRing R] :
    ∀ {r : ℕ} (n : Fin r → ℕ), (∀ i, 0 < n i) →
      (nestedDiagonalRadicalBase R r n).Finite
  | 0, _, _ => RingHom.Finite.id R
  | 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).Finite :=
        nestedDiagonalRadicalBase_isFinite nInit
          (fun i => hn i.castSucc)
      have hMap :
          (AddMonoidAlgebra.mapRingHom ℤ
            (nestedDiagonalRadicalBase R r nInit)).Finite :=
        mapRingHom_isFinite _ 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).Finite :=
        RingHom.finite_algebraMap.mpr inferInstance
      exact RingHom.Finite.comp hRoot hMap

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

theorem latticeMonoidAlgebraMap_isFinite
    {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).Finite