FiniteFieldModel.lean

theorem tensor_field_range_mono
    {k L R : Type u} [Field k] [Field L] [CommRing R]
    [Algebra k L] [Algebra k R]
    {F E : IntermediateField k L} (h : F ≤ E) :
    (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) F.val).range ≤
      (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) E.val).range

theorem exists_finiteIntermediateField_range
    {k L R : Type u} [Field k] [Field L] [CommRing R]
    [Algebra k L] [Algebra k R] [Algebra.IsAlgebraic k L]
    (T : Subalgebra R (R ⊗[k] L)) (hT : T.FG) :
    ∃ F : IntermediateField k L, FiniteDimensional k F ∧
      T ≤ (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) F.val).range

theorem exists_model_over_range
    {R S B : Type u} [CommRing R] [CommRing S] [CommRing B]
    [Algebra R S] [Algebra R B]
    (m : B →ₐ[R] S) (hm : Function.Injective m)
    (T : Subalgebra R S) (hT : T ≤ m.range)
    (A₀ : CommAlgCat.FiniteEtale.{u} T) :
    letI : Algebra B S := m.toRingHom.toAlgebra
    ∃ A₁ : CommAlgCat.FiniteEtale.{u} B,
      Nonempty (S ⊗[T] A₀ ≃ₐ[S] S ⊗[B] A₁) := by
  let : Algebra B S := m.toRingHom.toAlgebra
  let em : B ≃ₐ[R] m.range := AlgEquiv.ofInjective m hm
  let f : T →ₐ[R] B :=
    em.symm.toAlgHom.comp (T.val.codRestrict m.range (fun x ↦ hT x.property))
  have hmf : m.comp f = T.val := by
    ext x
    exact congrArg Subtype.val (em.apply_symm_apply ⟨x.val, hT x.property⟩)
  let : Algebra T B := f.toRingHom.toAlgebra
  let : IsScalarTower T B S :=
    IsScalarTower.of_algebraMap_eq' (congrArg AlgHom.toRingHom hmf).symm
  let A₁ : Type u := B ⊗[T] A₀
  refine ⟨CommAlgCat.FiniteEtale.of B A₁, ?_⟩
  exact ⟨(Algebra.TensorProduct.cancelBaseChange T B S S A₀).symm⟩

theorem exists_finiteIntermediateField_model
    (k L R : Type u) [Field k] [Field L] [CommRing R]
    [Algebra k L] [Algebra k R] [Algebra.IsAlgebraic k L]
    (A : CommAlgCat.FiniteEtale.{u} (R ⊗[k] L)) :
    ∃ F : IntermediateField k L, FiniteDimensional k F ∧
      letI : Algebra (R ⊗[k] F) (R ⊗[k] L) :=
        (Algebra.TensorProduct.map (R := k) (S := R) (AlgHom.id R R) F.val).toRingHom.toAlgebra
      ∃ A₀ : CommAlgCat.FiniteEtale.{u} (R ⊗[k] F),
        Nonempty (A ≃ₐ[R ⊗[k] L] (R ⊗[k] L) ⊗[R ⊗[k] F] A₀) := by
  obtain ⟨T, A₀, hring, halgebra, hTfinite, hfinite, hetale, ⟨eA⟩⟩ :=
    exists_finite_subalgebra_model R (R ⊗[k] L) A
  let : CommRing A₀ := hring
  let : Algebra T A₀ := halgebra
  let : Module.Finite T A₀ := hfinite
  let : Algebra.Etale T A₀ := hetale
  let : Module.Finite R T := hTfinite
  have hT : T.FG := (Subalgebra.fg_iff_finiteType T).mpr inferInstance
  obtain ⟨F, hF, hTF⟩ := exists_finiteIntermediateField_range T hT
  refine ⟨F, hF, ?_⟩
  let m : (R ⊗[k] F) →ₐ[R] (R ⊗[k] L) :=
    Algebra.TensorProduct.map (AlgHom.id R R) F.val
  let : Algebra (R ⊗[k] F) (R ⊗[k] L) := m.toRingHom.toAlgebra
  have hm : Function.Injective m :=
    TensorProduct.map_injective_of_flat_flat
      (AlgHom.id k R).toLinearMap F.val.toLinearMap
      (Function.injective_id) Subtype.val_injective
  obtain ⟨A₁, ⟨e₁⟩⟩ := by
    with_reducible_and_instances
      exact exists_model_over_range (R := R) (S := R ⊗[k] L) (B := R ⊗[k] F)
        m hm T hTF (CommAlgCat.FiniteEtale.of T A₀)
  exact ⟨A₁, ⟨eA.trans e₁⟩⟩