LinearIndependent_algebraMap_of_constantsAreBase_of_isAlgebraic.lean

theorem mem_range_of_isAlgebraic {K F : Type*} [Field K] [Field F] [Algebra K F] (hC :
  AlgebraicCurve.ConstantsAreBase K F)
    (y : F) (hy : IsAlgebraic K y) : y ∈ (algebraMap K F).range

theorem _root_.AlgebraicCurve.linearIndependent_algebraMap_of_constantsAreBase_of_isAlgebraic
    (K F K' F' : Type*)
    [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
    [PerfectField K] [Algebra.IsAlgebraic K K']
    (hC : AlgebraicCurve.ConstantsAreBase K F)
    {ι : Type*} {b : ι → F} (hb : LinearIndependent K b) :
    LinearIndependent K' (fun i => algebraMap F F' (b i)) := by
  classical
  have hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range := mem_range_of_isAlgebraic hC
  have : Algebra.IsSeparable K K' := Algebra.IsAlgebraic.isSeparable_of_perfectField
  have hfield : IsField (F ⊗[K] K') :=
    Algebra.TensorProduct.isField_of_isSeparable_of_forall_isAlgebraic_mem_range K F K' hconst
  have hfield' : IsField (K' ⊗[K] F) := MulEquiv.isField hfield (Algebra.TensorProduct.comm K K'
    F).toMulEquiv
  let : Field (K' ⊗[K] F) := hfield'.toField
  let ψ : K' ⊗[K] F →ₐ[K'] F' := Algebra.TensorProduct.lift (Algebra.ofId K' F')
    (IsScalarTower.toAlgHom K F F') (fun _ _ => Commute.all _ _)
  have hψ : ∀ f : F, ψ ((1 : K') ⊗ₜ[K] f) = algebraMap F F' f := by
    intro f
    change Algebra.TensorProduct.lift _ _ _ ((1 : K') ⊗ₜ[K] f) = _
    rw [Algebra.TensorProduct.lift_tmul]
    simp [Algebra.ofId_apply]
  have hψinj : Function.Injective ψ := RingHom.injective ψ.toRingHom
  have hψker : LinearMap.ker ψ.toLinearMap = ⊥ := LinearMap.ker_eq_bot.mpr hψinj
  let M : Submodule K F := Submodule.span K (Set.range b)
  let bM : Module.Basis ι K M := Module.Basis.span hb
  let B := Algebra.TensorProduct.basis K' bM
  have hincl : Function.Injective (M.subtype.baseChange K') := by
    show Function.Injective ((M.subtype.baseChange K' : K' ⊗[K] M →ₗ[K'] K' ⊗[K] F) : K' ⊗[K] M →
      K' ⊗[K] F)
    rw [LinearMap.baseChange_eq_ltensor]
    exact Module.Flat.lTensor_preserves_injective_linearMap M.subtype (Submodule.injective_subtype
      M)
  have hli1 : LinearIndependent K' ((M.subtype.baseChange K') ∘ B) := B.linearIndependent.map' _
    (LinearMap.ker_eq_bot.mpr hincl)
  have hli2 : LinearIndependent K' (ψ.toLinearMap ∘ ((M.subtype.baseChange K') ∘ B)) := hli1.map' _
    hψker
  convert hli2 using 1
  funext i
  simp only [Function.comp_apply]
  rw [show B i = (1 : K') ⊗ₜ[K] (bM i) from Algebra.TensorProduct.basis_apply bM i,
    LinearMap.baseChange_tmul, Submodule.subtype_apply,
    show ((bM i : M) : F) = b i from congrArg Subtype.val (Module.Basis.span_apply hb i)]
  exact (hψ (b i)).symm