ArithmeticAlgebraicClosure.lean

theorem pi1_transport_injective
    {X : Scheme.{u}} {Ω : Type u} [Field Ω]
    {xi eta : Spec (.of Ω) ⟶ X} (h : xi = eta) :
    Function.Injective (fun a : π₁ᵉᵗ(xi) ↦ h ▸ a) := by
  cases h
  exact Function.injective_id

theorem pi1_transport_symm_cancel
    {X : Scheme.{u}} {Ω : Type u} [Field Ω]
    {xi eta : Spec (.of Ω) ⟶ X} (h : xi = eta) (a : π₁ᵉᵗ(eta)) :
    h ▸ (h.symm ▸ a) = a

theorem fundamentalGroupHom_eq_one_transport
    {X Y : Scheme.{u}} (f : X ⟶ Y) {Ω : Type u} [Field Ω]
    {xi eta : Spec (.of Ω) ⟶ X} (h : xi = eta) (a : π₁ᵉᵗ(xi)) :
    fundamentalGroupHom f eta (h ▸ a) = 1 ↔
      fundamentalGroupHom f xi a = 1

theorem separableClosureProjection_pullback_isEquivalence
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsAlgClosure k L]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) :
    (pullback (separableClosureProjection k L X f)).IsEquivalence

theorem separableClosureProjection_fundamentalGroupHom_bijective
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsAlgClosure k L]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    [ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    Function.Bijective (fundamentalGroupHom (separableClosureProjection k L X f) xi)

theorem separableClosureProjection_fundamentalGroupHom_comparison
    (k L : Type u) [Field k] [Field L] [Algebra k L]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k))
    {Ω : Type u} [Field Ω]
    (xi : Spec (.of Ω) ⟶ Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    let r := separableClosureProjection k L X f
    let pK := pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k (separableClosure k L)))) f
    let pL := pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f
    ∃ hpoint : (xi ≫ r) ≫ pK = xi ≫ pL,
      ∃ c : π₁ᵉᵗ(xi ≫ pL), ∀ a : π₁ᵉᵗ(xi),
        hpoint ▸ fundamentalGroupHom pK (xi ≫ r) (fundamentalGroupHom r xi a) =
          MulAut.conj c (fundamentalGroupHom pL xi a) := by
  let r := separableClosureProjection k L X f
  let pK := pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k (separableClosure k L)))) f
  let pL := pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap k L))) f
  have hp : pL = r ≫ pK := (separableClosureProjection_comp_snd k L X f).symm
  have hpoint : (xi ≫ r) ≫ pK = xi ≫ pL := by
    rw [Category.assoc, ← hp]
  let t : pullback pL ⋙ fiber xi ≅ fiber (xi ≫ pL) :=
    pullbackCompositeFiberIsoOfEq r pK pL hp xi (xi ≫ pL) hpoint
  refine ⟨hpoint, (pullbackFiberIso pL xi).symm ≪≫ t, ?_⟩
  intro a
  rw [fundamentalGroupHom_comp_transport_eq_autHomOfCompIso r pK pL hp xi (xi ≫ pL) hpoint]
  exact fundamentalGroupHom_eq_conj_of_comparison pL xi t a

theorem fundamentalGroupHom_injective_of_isAlgClosure
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsAlgClosure k L]
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (f : X ⟶ Spec (.of k))
    [ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    Function.Injective (fundamentalGroupHom (Limits.pullback.snd _ f) xi)

theorem fundamentalGroupHom_constantField_ker_eq_range_of_isAlgClosure
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsAlgClosure k L]
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (f : X ⟶ Spec (.of k))
    [ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    (fundamentalGroupHom f (xi ≫ Limits.pullback.snd _ f)).toMonoidHom.ker =
      (fundamentalGroupHom (Limits.pullback.snd _ f) xi).toMonoidHom.range

theorem arithmetic_exactSequence_of_isAlgClosure
    (k L : Type u) [Field k] [Field L] [Algebra k L] [IsAlgClosure k L]
    (X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X]
    (f : X ⟶ Spec (.of k))
    [ConnectedSpace ↑(Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f)]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (xi : Spec (.of Ω) ⟶ Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap k L))) f) :
    let geometric := fundamentalGroupHom (Limits.pullback.snd _ f) xi
    let arithmetic := arithmeticFundamentalGroupHom k (SeparableClosure k) f
      (xi ≫ Limits.pullback.snd _ f)
    Function.Injective geometric ∧ Function.Surjective arithmetic ∧
      arithmetic.toMonoidHom.ker = geometric.toMonoidHom.range := by
  let : IsAlgClosed L := IsAlgClosure.isAlgClosed k
  refine ⟨fundamentalGroupHom_injective_of_isAlgClosure k L X f xi,
    arithmeticFundamentalGroupHom_surjective_of_connected_constantField
      k (SeparableClosure k) L f (xi ≫ Limits.pullback.snd _ f), ?_⟩
  exact (arithmeticFundamentalGroupHom_ker k (SeparableClosure k) f
    (xi ≫ Limits.pullback.snd _ f)).trans
      (fundamentalGroupHom_constantField_ker_eq_range_of_isAlgClosure k L X f xi)