FiniteFamilyModel.lean

def coefficientBaseChangeMap
    (k A B : Type u) [Field k] [Field A] [Field B] [Algebra k A] [Algebra k B]
    (U : Scheme.{u}) (f : U ⟶ Spec (CommRingCat.of k)) (v : A →ₐ[k] B) :
    Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k B))) f ⟶
      Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k A))) f

theorem coefficientBaseChangeMap_comp
    (k A B C : Type u) [Field k] [Field A] [Field B] [Field C]
    [Algebra k A] [Algebra k B] [Algebra k C]
    (U : Scheme.{u}) (f : U ⟶ Spec (CommRingCat.of k))
    (v : A →ₐ[k] B) (w : B →ₐ[k] C) :
    coefficientBaseChangeMap k B C U f w ≫ coefficientBaseChangeMap k A B U f v =
      coefficientBaseChangeMap k A C U f (w.comp v)

def finiteEtalePullbackCompObjIso {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (fg : X ⟶ Z)
    (hfg : f ≫ g = fg) (A : AlgebraicGeometry.FiniteEtale Z) :
    (AlgebraicGeometry.FiniteEtale.pullback f).obj
      ((AlgebraicGeometry.FiniteEtale.pullback g).obj A) ≅
        (AlgebraicGeometry.FiniteEtale.pullback fg).obj A

theorem exists_finiteIntermediateField_affine_scheme_model_family
    (k L : Type u) [Field k] [Field L] [Algebra k L] [Algebra.IsAlgebraic k L]
    {ι : Type u} [Finite ι] (U : ι → Scheme.{u}) [∀ i, IsAffine (U i)]
    (f : ∀ i, U i ⟶ Spec (CommRingCat.of k))
    (X : ∀ i, AlgebraicGeometry.FiniteEtale
      (Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) (f i))) :
    ∃ F : IntermediateField k L, FiniteDimensional k F ∧
      ∃ X₀ : ∀ i, AlgebraicGeometry.FiniteEtale
        (Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k F))) (f i)),
        ∀ i, Nonempty ((AlgebraicGeometry.FiniteEtale.pullback
          (Limits.pullback.map (Spec.map (CommRingCat.ofHom (algebraMap k L))) (f i)
            (Spec.map (CommRingCat.ofHom (algebraMap k F))) (f i)
            (Spec.map (CommRingCat.ofHom F.val.toRingHom)) (𝟙 (U i))
            (𝟙 (Spec (CommRingCat.of k)))
            (by rw [Category.comp_id, ← Spec.map_comp]; rfl)
            (by rw [Category.id_comp, Category.comp_id]))).obj (X₀ i) ≅ X i) := by
  classical
  choose Fᵢ hFᵢ Mᵢ eᵢ using fun i ↦
    exists_finiteIntermediateField_affine_scheme_model k L (U i) (f i) (X i)
  let : ∀ i, FiniteDimensional k (Fᵢ i) := hFᵢ
  let F : IntermediateField k L := ⨆ i, Fᵢ i
  let v (i : ι) : Fᵢ i →ₐ[k] F := IntermediateField.inclusion (le_iSup Fᵢ i)
  let a (i : ι) := coefficientBaseChangeMap k (Fᵢ i) F (U i) (f i) (v i)
  let b (i : ι) := coefficientBaseChangeMap k F L (U i) (f i) F.val
  let c (i : ι) := coefficientBaseChangeMap k (Fᵢ i) L (U i) (f i) (Fᵢ i).val
  have hcomp (i : ι) : b i ≫ a i = c i := by
    dsimp only [a, b, c]
    rw [coefficientBaseChangeMap_comp]
    rfl
  let M (i : ι) : AlgebraicGeometry.FiniteEtale
      (Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k F))) (f i)) :=
    (AlgebraicGeometry.FiniteEtale.pullback (a i)).obj (Mᵢ i)
  refine ⟨F, inferInstance, M, ?_⟩
  intro i
  change Nonempty ((AlgebraicGeometry.FiniteEtale.pullback (b i)).obj (M i) ≅ X i)
  exact ⟨finiteEtalePullbackCompObjIso (b i) (a i) (c i) (hcomp i) (Mᵢ i) ≪≫
    (eᵢ i).some⟩