NYLL
Module

Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent.lean

Nyll.AlgebraicCurves.Places.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
13 declarations indexed from sourceView source ↗

Module documentation

Place exists intermediate Field finite Dimensional forall smul eq of descent

Imports5
Imported by1

Declarations

theorem

hfg

L37 ↗
AlgebraicCurves.Places.Proofs.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent.AlgebraicCurve.C3Tors.Frame.hfg
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace C3Tors
namespace Frame
open _root_.AlgebraicCurve
Lean source · statement
theorem hfg (F : Type) [Field F] [Algebra ℚ F] [IsCurveOver ℚ F] [Algebra.EssFiniteType ℚ F] :
    ∃ s : Finset F, IntermediateField.adjoin ℚ (s : Set F) = ⊤
theorem

hgen

L41 ↗
AlgebraicCurves.Places.Proofs.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent.AlgebraicCurve.C3Tors.Frame.hgen
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace C3Tors
namespace Frame
open _root_.AlgebraicCurve
Lean source · statement
theorem hgen (F Fbar : Type) [Field F] [Field Fbar] [Algebra (AlgebraicClosure ℚ) Fbar] [Algebra F
  Fbar]
    (toBar : F →+* Fbar) (halg : ∀ x : F, algebraMap F Fbar x = toBar x)
    (closure_toBar : Subfield.closure
      (Set.range (algebraMap (AlgebraicClosure ℚ) Fbar) ∪ Set.range toBar) = ⊤) :
    IntermediateField.adjoin (AlgebraicClosure ℚ) (Set.range (algebraMap F Fbar)) = ⊤
theorem

hLD

L59 ↗
AlgebraicCurves.Places.Proofs.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent.AlgebraicCurve.C3Tors.Frame.hLD
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
open _root_.AlgebraicCurve
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace C3Tors
namespace Frame
open _root_.AlgebraicCurve
Lean source · full declaration
theorem hLD (F Fbar : Type) [Field F] [Algebra ℚ F] [Field Fbar] [Algebra (AlgebraicClosure ℚ)
  Fbar] [Algebra F Fbar]
    (toBar : F →+* Fbar) (halg : ∀ x : F, algebraMap F Fbar x = toBar x)
    (linearIndependent_toBar : ∀ s : Finset F,
      LinearIndependent ℚ (fun x : s => (x : F)) →
        LinearIndependent (AlgebraicClosure ℚ) (fun x : s => toBar (x : F))) :
    ∀ (n : ℕ) (f : Fin n → F) (c : Fin n → AlgebraicClosure ℚ), LinearIndependent ℚ f →
      ∑ i, algebraMap (AlgebraicClosure ℚ) Fbar (c i) * algebraMap F Fbar (f i) = 0 → ∀ i, c i = 0
        := by
  classical
  intro n f c hf hsum i
  let s : Finset F := Finset.univ.image f
  have hmem : ∀ j, f j ∈ s := fun j => Finset.mem_image_of_mem f (Finset.mem_univ j)
  have hst : Set.range f = (s : Set F) := by
    rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  have hs : LinearIndependent ℚ (fun x : ↥s => (x : F)) := LinearIndependent.linearIndepOn_id' hf
    hst
  have hsbar := linearIndependent_toBar s hs
  let ι : Fin n → ↥s := fun j => ⟨f j, hmem j⟩
  have hι : Function.Injective ι := fun j k h => hf.injective (congrArg Subtype.val h)
  have hli : LinearIndependent (AlgebraicClosure ℚ) (fun j : Fin n => toBar (f j)) := hsbar.comp ι
    hι
  have hsum' : ∑ j, c j • toBar (f j) = 0 := by
    simpa only [Algebra.smul_def, halg] using hsum
  exact linearIndependent_iff'.mp hli Finset.univ c hsum' i (Finset.mem_univ i)
theorem

smul_mem_nonunits_smul

L99 ↗
AlgebraicCurves.Places.Proofs.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent.AlgebraicCurve.C3Tors.Core.smul_mem_nonunits_smul
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
open _root_.AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace C3Tors
namespace Core
open _root_.AlgebraicCurve
section Generic
variable {K F : Type} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem smul_mem_nonunits_smul (g : SemilinearAut K F) (P : Place K F) {x : F}
    (hx : x ∈ P.toValuationSubring.nonunits) : g • x ∈ (g • P).toValuationSubring.nonunits
theorem

exists_sub_algebraMap_mem_nonunits

L109 ↗
AlgebraicCurves.Places.Proofs.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent.AlgebraicCurve.C3Tors.Core.exists_sub_algebraMap_mem_nonunits
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
open _root_.AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace C3Tors
namespace Core
open _root_.AlgebraicCurve
section Generic
variable {K F : Type} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_sub_algebraMap_mem_nonunits [IsAlgClosed K] (P : Place K F) [Module.Finite K
  P.ResidueField]
    (y : F) (hy : y ∈ P.toValuationSubring) :
    ∃ a : K, y - algebraMap K F a ∈ P.toValuationSubring.nonunits
theorem

algebraMap_eq_of_sub_mem_nonunits

L128 ↗
AlgebraicCurves.Places.Proofs.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent.AlgebraicCurve.C3Tors.Core.algebraMap_eq_of_sub_mem_nonunits
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
open _root_.AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace C3Tors
namespace Core
open _root_.AlgebraicCurve
section Generic
variable {K F : Type} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem algebraMap_eq_of_sub_mem_nonunits (P : Place K F) {y : F} (_hy : y ∈ P.toValuationSubring)
  {a a' : K}
    (ha : y - algebraMap K F a ∈ P.toValuationSubring.nonunits)
    (ha' : y - algebraMap K F a' ∈ P.toValuationSubring.nonunits) : a = a'
theorem

isIntegral_of_closure

L158 ↗
AlgebraicCurves.Places.Proofs.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent.AlgebraicCurve.C3Tors.Core.isIntegral_of_closure
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
open _root_.AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace C3Tors
namespace Core
open _root_.AlgebraicCurve
section Frame
variable (F : Type) [Field F] [Algebra ℚ F] [IsCurveOver ℚ F] [Algebra.EssFiniteType ℚ F]
  (Fbar : Type) [Field Fbar] [Algebra (AlgebraicClosure ℚ) Fbar]
  [IsCurveOver (AlgebraicClosure ℚ) Fbar] [Algebra.EssFiniteType (AlgebraicClosure ℚ) Fbar]
  [Algebra F Fbar] [Algebra ℚ Fbar] [IsScalarTower ℚ F Fbar] [IsScalarTower ℚ (AlgebraicClosure ℚ)
    Fbar]
omit [IsCurveOver ℚ F] [Algebra.EssFiniteType ℚ F]
  [IsCurveOver (AlgebraicClosure ℚ) Fbar]
  [Algebra.EssFiniteType (AlgebraicClosure ℚ) Fbar] in
Lean source · statement
theorem isIntegral_of_closure (toBar : F →+* Fbar) (halg : ∀ x, algebraMap F Fbar x = toBar x)
    (closure_toBar : Subfield.closure
      (Set.range (algebraMap (AlgebraicClosure ℚ) Fbar) ∪ Set.range toBar) = ⊤) :
    Algebra.IsIntegral F Fbar
def

overQ

L189 ↗
AlgebraicCurves.Places.Proofs.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent.AlgebraicCurve.C3Tors.Core.overQ
Documentation

A place over the algebraic closure of the rationals, viewed as a place over the rationals.

Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
open _root_.AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace C3Tors
namespace Core
open _root_.AlgebraicCurve
section Frame
variable (F : Type) [Field F] [Algebra ℚ F] [IsCurveOver ℚ F] [Algebra.EssFiniteType ℚ F]
  (Fbar : Type) [Field Fbar] [Algebra (AlgebraicClosure ℚ) Fbar]
  [IsCurveOver (AlgebraicClosure ℚ) Fbar] [Algebra.EssFiniteType (AlgebraicClosure ℚ) Fbar]
  [Algebra F Fbar] [Algebra ℚ Fbar] [IsScalarTower ℚ F Fbar] [IsScalarTower ℚ (AlgebraicClosure ℚ)
    Fbar]
variable [Algebra.IsIntegral F Fbar]
Lean source · full declaration
def overQ (P : Place (AlgebraicClosure ℚ) Fbar) : Place ℚ Fbar where
  toValuationSubring := P.toValuationSubring
  algebraMap_mem' a := by
    rw [IsScalarTower.algebraMap_apply ℚ (AlgebraicClosure ℚ) Fbar]
    exact P.algebraMap_mem' _
  ne_top' := P.ne_top'
  isPrincipalIdealRing' := P.isPrincipalIdealRing'
theorem

overQ_toValuationSubring

L197 ↗
AlgebraicCurves.Places.Proofs.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent.AlgebraicCurve.C3Tors.Core.overQ_toValuationSubring
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
open _root_.AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace C3Tors
namespace Core
open _root_.AlgebraicCurve
section Frame
variable (F : Type) [Field F] [Algebra ℚ F] [IsCurveOver ℚ F] [Algebra.EssFiniteType ℚ F]
  (Fbar : Type) [Field Fbar] [Algebra (AlgebraicClosure ℚ) Fbar]
  [IsCurveOver (AlgebraicClosure ℚ) Fbar] [Algebra.EssFiniteType (AlgebraicClosure ℚ) Fbar]
  [Algebra F Fbar] [Algebra ℚ Fbar] [IsScalarTower ℚ F Fbar] [IsScalarTower ℚ (AlgebraicClosure ℚ)
    Fbar]
variable [Algebra.IsIntegral F Fbar]
omit [IsCurveOver (AlgebraicClosure ℚ) Fbar] [Algebra.EssFiniteType (AlgebraicClosure ℚ) Fbar] in
Lean source · statement
theorem overQ_toValuationSubring (P : Place (AlgebraicClosure ℚ) Fbar) :
    (overQ Fbar P).toValuationSubring = P.toValuationSubring
theorem

restrict_smul_eq

L202 ↗
AlgebraicCurves.Places.Proofs.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent.AlgebraicCurve.C3Tors.Core.restrict_smul_eq
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
open _root_.AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace C3Tors
namespace Core
open _root_.AlgebraicCurve
section Frame
variable (F : Type) [Field F] [Algebra ℚ F] [IsCurveOver ℚ F] [Algebra.EssFiniteType ℚ F]
  (Fbar : Type) [Field Fbar] [Algebra (AlgebraicClosure ℚ) Fbar]
  [IsCurveOver (AlgebraicClosure ℚ) Fbar] [Algebra.EssFiniteType (AlgebraicClosure ℚ) Fbar]
  [Algebra F Fbar] [Algebra ℚ Fbar] [IsScalarTower ℚ F Fbar] [IsScalarTower ℚ (AlgebraicClosure ℚ)
    Fbar]
variable [Algebra.IsIntegral F Fbar]
omit [IsCurveOver ℚ F] [Algebra.EssFiniteType ℚ F]
  [IsCurveOver (AlgebraicClosure ℚ) Fbar]
  [Algebra.EssFiniteType (AlgebraicClosure ℚ) Fbar] in
Lean source · statement
theorem restrict_smul_eq (g : SemilinearAut (AlgebraicClosure ℚ) Fbar) (hg : ∀ x : F, g •
  algebraMap F Fbar x = algebraMap F Fbar x)
    (P : Place (AlgebraicClosure ℚ) Fbar) :
    (g • P).toValuationSubring.comap (algebraMap F Fbar) = ((overQ Fbar P).restrict
      F).toValuationSubring
theorem

exists_intermediateField_forall_exists_mem

L215 ↗
AlgebraicCurves.Places.Proofs.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent.AlgebraicCurve.C3Tors.Core.exists_intermediateField_forall_exists_mem
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
open _root_.AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace C3Tors
namespace Core
open _root_.AlgebraicCurve
section Frame
variable (F : Type) [Field F] [Algebra ℚ F] [IsCurveOver ℚ F] [Algebra.EssFiniteType ℚ F]
  (Fbar : Type) [Field Fbar] [Algebra (AlgebraicClosure ℚ) Fbar]
  [IsCurveOver (AlgebraicClosure ℚ) Fbar] [Algebra.EssFiniteType (AlgebraicClosure ℚ) Fbar]
  [Algebra F Fbar] [Algebra ℚ Fbar] [IsScalarTower ℚ F Fbar] [IsScalarTower ℚ (AlgebraicClosure ℚ)
    Fbar]
variable [Algebra.IsIntegral F Fbar]
omit [Algebra.EssFiniteType ℚ F] [Algebra.EssFiniteType (AlgebraicClosure ℚ) Fbar] in
Lean source · statement
theorem exists_intermediateField_forall_exists_mem (P : Place (AlgebraicClosure ℚ) Fbar) :
    ∃ L : IntermediateField ℚ (AlgebraicClosure ℚ), FiniteDimensional ℚ L ∧
      ∀ f : F, f ∈ ((overQ Fbar P).restrict F).toValuationSubring →
        ∃ a : AlgebraicClosure ℚ, a ∈ L ∧
          algebraMap F Fbar f - algebraMap (AlgebraicClosure ℚ) Fbar a ∈
            P.toValuationSubring.nonunits
theorem

main

L292 ↗
AlgebraicCurves.Places.Proofs.Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent.AlgebraicCurve.C3Tors.Core.main
Source context 15 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
open _root_.AlgebraicCurve
open scoped Pointwise
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace C3Tors
namespace Core
open _root_.AlgebraicCurve
section Frame
variable (F : Type) [Field F] [Algebra ℚ F] [IsCurveOver ℚ F] [Algebra.EssFiniteType ℚ F]
  (Fbar : Type) [Field Fbar] [Algebra (AlgebraicClosure ℚ) Fbar]
  [IsCurveOver (AlgebraicClosure ℚ) Fbar] [Algebra.EssFiniteType (AlgebraicClosure ℚ) Fbar]
  [Algebra F Fbar] [Algebra ℚ Fbar] [IsScalarTower ℚ F Fbar] [IsScalarTower ℚ (AlgebraicClosure ℚ)
    Fbar]
variable [Algebra.IsIntegral F Fbar]
omit [Algebra.EssFiniteType ℚ F]
  [Algebra.EssFiniteType (AlgebraicClosure ℚ) Fbar] in
Lean source · statement
theorem main
    (toBar : F →+* Fbar) (halg : ∀ x, algebraMap F Fbar x = toBar x)
    (gal : (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) →* SemilinearAut (AlgebraicClosure ℚ) Fbar)
    (baseAut_gal : ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ,
      SemilinearAut.baseAut (gal σ) = (σ : AlgebraicClosure ℚ ≃+* AlgebraicClosure ℚ))
    (gal_smul_toBar : ∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : F), gal σ • toBar x
      = toBar x)
    (hfg : ∃ s : Finset F, IntermediateField.adjoin ℚ (s : Set F) = ⊤)
    (hgen : IntermediateField.adjoin (AlgebraicClosure ℚ) (Set.range (algebraMap F Fbar)) = ⊤)
    (hLD : ∀ (n : ℕ) (f : Fin n → F) (c : Fin n → AlgebraicClosure ℚ), LinearIndependent ℚ f →
      ∑ i, algebraMap (AlgebraicClosure ℚ) Fbar (c i) * algebraMap F Fbar (f i) = 0 → ∀ i, c i = 0)
    (P : Place (AlgebraicClosure ℚ) Fbar) :
    ∃ L : IntermediateField ℚ (AlgebraicClosure ℚ), FiniteDimensional ℚ L ∧
      ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, (∀ y ∈ L, σ y = y) → gal σ • P = P
theorem

exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent

L332 ↗
AlgebraicCurve.Place.exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
open _root_.AlgebraicCurve
open scoped Pointwise
Lean source · full declaration
theorem
  _root_.AlgebraicCurve.Place.exists_intermediateField_finiteDimensional_forall_smul_eq_of_descent
    (F : Type) [Field F] [Algebra ℚ F] [IsCurveOver ℚ F] [Algebra.EssFiniteType ℚ F]
    (Fbar : Type) [Field Fbar] [Algebra (AlgebraicClosure ℚ) Fbar]
    [IsCurveOver (AlgebraicClosure ℚ) Fbar] [Algebra.EssFiniteType (AlgebraicClosure ℚ) Fbar]
    (toBar : F →+* Fbar)
    (toBar_algebraMap : ∀ r : ℚ,
      toBar (algebraMap ℚ F r) = algebraMap (AlgebraicClosure ℚ) Fbar (algebraMap ℚ
        (AlgebraicClosure ℚ) r))
    (closure_toBar : Subfield.closure
      (Set.range (algebraMap (AlgebraicClosure ℚ) Fbar) ∪ Set.range toBar) = ⊤)
    (linearIndependent_toBar : ∀ s : Finset F,
      LinearIndependent ℚ (fun x : s => (x : F)) →
        LinearIndependent (AlgebraicClosure ℚ) (fun x : s => toBar (x : F)))
    (gal : (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) →* SemilinearAut (AlgebraicClosure ℚ) Fbar)
    (baseAut_gal : ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ,
      SemilinearAut.baseAut (gal σ) = (σ : AlgebraicClosure ℚ ≃+* AlgebraicClosure ℚ))
    (gal_smul_toBar : ∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : F), gal σ • toBar x
      = toBar x)
    (P : Place (AlgebraicClosure ℚ) Fbar) :
    ∃ L : IntermediateField ℚ (AlgebraicClosure ℚ), FiniteDimensional ℚ L ∧
      ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, (∀ y ∈ L, σ y = y) → gal σ • P = P := by
  let algF : Algebra F Fbar := toBar.toAlgebra
  let algQ : Algebra ℚ Fbar := ((algebraMap (AlgebraicClosure ℚ) Fbar).comp (algebraMap ℚ
    (AlgebraicClosure ℚ))).toAlgebra
  have : IsScalarTower ℚ (AlgebraicClosure ℚ) Fbar := IsScalarTower.of_algebraMap_eq (fun _ => rfl)
  have halg : ∀ x : F, algebraMap F Fbar x = toBar x := fun _ => rfl
  have : IsScalarTower ℚ F Fbar := IsScalarTower.of_algebraMap_eq (fun r => by
    rw [halg, toBar_algebraMap]; rfl)
  have : Algebra.IsIntegral F Fbar := AlgebraicCurve.C3Tors.Core.isIntegral_of_closure F Fbar toBar
    halg closure_toBar
  exact AlgebraicCurve.C3Tors.Core.main F Fbar toBar halg gal baseAut_gal gal_smul_toBar
    (AlgebraicCurve.C3Tors.Frame.hfg F) (AlgebraicCurve.C3Tors.Frame.hgen F Fbar toBar halg
      closure_toBar)
    (AlgebraicCurve.C3Tors.Frame.hLD F Fbar toBar halg linearIndependent_toBar) P

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.