ProperGroupScheme.lean

theorem multiplication_data (G : RelativeGroupLaw K f) :
    let e := (G.one (𝟙 (Spec (.of K)))).1
    let z := pullback.lift e e (rfl : e ≫ f = e ≫ f)
    let P := pointedFundamentalGroupHom (pullback.fst f f) z e
      (pullback.lift_fst _ _ _)
    let Q := pointedFundamentalGroupHom (pullback.snd f f) z e
      (pullback.lift_snd _ _ _)
    let M := pointedFundamentalGroupHom (G.mulRight f idPoint) z e
      G.unitPoint_comp_mulRight_idPoint
    (∀ a, M a = P a * Q a) ∧ (∀ a b : π₁ᵉᵗ(e), a * b = b * a) := by
  intro e z P Q M
  have he : e ≫ f = 𝟙 _ := (G.one (𝟙 (Spec (.of K)))).2
  have hA : ConnectedSpace A := GeometricallyConnected.connectedSpace f f.isOpenMap
  have hN : IsLocallyNoetherian A := LocallyOfFiniteType.isLocallyNoetherian f
  have hz₁ : z ≫ pullback.fst f f = e := pullback.lift_fst _ _ _
  have hz₂ : z ≫ pullback.snd f f = e := pullback.lift_snd _ _ _
  let i : A ⟶ pullback f f := pullback.lift (𝟙 A) (f ≫ e)
    (by rw [Category.assoc, he, Category.comp_id, Category.id_comp])
  let j : A ⟶ pullback f f := pullback.lift (f ≫ e) (𝟙 A)
    (by rw [Category.assoc, he, Category.comp_id, Category.id_comp])
  have hi₁ : i ≫ pullback.fst f f = 𝟙 A := pullback.lift_fst _ _ _
  have hi₂ : i ≫ pullback.snd f f = f ≫ e := pullback.lift_snd _ _ _
  have hj₁ : j ≫ pullback.fst f f = f ≫ e := pullback.lift_fst _ _ _
  have hj₂ : j ≫ pullback.snd f f = 𝟙 A := pullback.lift_snd _ _ _
  have hei : e ≫ i = z := by
    apply pullback.hom_ext
    · rw [Category.assoc, hi₁, Category.comp_id, hz₁]
    · rw [Category.assoc, hi₂, ← Category.assoc, he, Category.id_comp, hz₂]
  have hej : e ≫ j = z := by
    apply pullback.hom_ext
    · rw [Category.assoc, hj₁, ← Category.assoc, he, Category.id_comp, hz₁]
    · rw [Category.assoc, hj₂, Category.comp_id, hz₂]
  let I := pointedFundamentalGroupHom i e z hei
  let J := pointedFundamentalGroupHom j e z hej
  have hPI : P.comp I = ContinuousMonoidHom.id π₁ᵉᵗ(e) := by
    dsimp only [P, I]
    rw [pointedFundamentalGroupHom_comp]
    simpa only [hi₁] using pointedFundamentalGroupHom_id e
  have hQI : Q.comp I = 1 := by
    dsimp only [Q, I]
    rw [pointedFundamentalGroupHom_comp]
    simpa only [hi₂] using
      pointedFundamentalGroupHom_constant f e e e
        (by rw [← Category.assoc, he, Category.id_comp])
  have hPJ : P.comp J = 1 := by
    dsimp only [P, J]
    rw [pointedFundamentalGroupHom_comp]
    simpa only [hj₁] using
      pointedFundamentalGroupHom_constant f e e e
        (by rw [← Category.assoc, he, Category.id_comp])
  have hQJ : Q.comp J = ContinuousMonoidHom.id π₁ᵉᵗ(e) := by
    dsimp only [Q, J]
    rw [pointedFundamentalGroupHom_comp]
    simpa only [hj₂] using pointedFundamentalGroupHom_id e
  have hMI : M.comp I = ContinuousMonoidHom.id π₁ᵉᵗ(e) := by
    have hm : i ≫ G.mulRight f idPoint = 𝟙 A := G.rightUnit_comp_mulRight_idPoint
    dsimp only [M, I]
    rw [pointedFundamentalGroupHom_comp]
    simpa only [hm] using pointedFundamentalGroupHom_id e
  have hMJ : M.comp J = ContinuousMonoidHom.id π₁ᵉᵗ(e) := by
    have hm : j ≫ G.mulRight f idPoint = 𝟙 A := G.leftUnit_comp_mulRight_idPoint
    dsimp only [M, J]
    rw [pointedFundamentalGroupHom_comp]
    simpa only [hm] using pointedFundamentalGroupHom_id e
  have hpair : Function.Injective (P.prod Q) := by
    have hn := (fundamentalGroupHom_proper_product_bijective f f z
      (by rw [hz₂, he])).1
    intro a b hab
    apply hn
    apply Prod.ext
    · change fundamentalGroupHom (pullback.fst f f) z a =
        fundamentalGroupHom (pullback.fst f f) z b
      apply (eq_rec_on_bijective
        (C := fun eta : Spec (.of K) ⟶ A => π₁ᵉᵗ(eta)) hz₁).injective
      have h : P a = P b := congrArg Prod.fst hab
      simpa only [P, pointedFundamentalGroupHom_apply] using h
    · change fundamentalGroupHom (pullback.snd f f) z a =
        fundamentalGroupHom (pullback.snd f f) z b
      apply (eq_rec_on_bijective
        (C := fun eta : Spec (.of K) ⟶ A => π₁ᵉᵗ(eta)) hz₂).injective
      have h : Q a = Q b := congrArg Prod.snd hab
      simpa only [Q, pointedFundamentalGroupHom_apply] using h
  have hpi (a) : P (I a) = a := DFunLike.congr_fun hPI a
  have hqi (a) : Q (I a) = 1 := DFunLike.congr_fun hQI a
  have hpj (a) : P (J a) = 1 := DFunLike.congr_fun hPJ a
  have hqj (a) : Q (J a) = a := DFunLike.congr_fun hQJ a
  have hmi (a) : M (I a) = a := DFunLike.congr_fun hMI a
  have hmj (a) : M (J a) = a := DFunLike.congr_fun hMJ a
  have hdecomp (a : π₁ᵉᵗ(z)) : I (P a) * J (Q a) = a := by
    apply hpair
    apply Prod.ext
    · change P (I (P a) * J (Q a)) = P a
      rw [map_mul, hpi, hpj, _root_.mul_one]
    · change Q (I (P a) * J (Q a)) = Q a
      rw [map_mul, hqi, hqj, _root_.one_mul]
  constructor
  · intro a
    calc
      M a = M (I (P a) * J (Q a)) := congrArg M (hdecomp a).symm
      _ = P a * Q a := by rw [map_mul, hmi, hmj]
  · intro a b
    have hab : I a * J b = J b * I a := by
      apply hpair
      apply Prod.ext
      · change P (I a * J b) = P (J b * I a)
        rw [map_mul, map_mul, hpi, hpj, _root_.mul_one, _root_.one_mul]
      · change Q (I a * J b) = Q (J b * I a)
        rw [map_mul, map_mul, hqi, hqj, _root_.mul_one, _root_.one_mul]
    calc
      a * b = M (I a * J b) := by rw [map_mul, hmi, hmj]
      _ = M (J b * I a) := congrArg M hab
      _ = b * a := by rw [map_mul, hmj, hmi]

theorem fundamentalGroup_mul_comm (G : RelativeGroupLaw K f)
    (a b : π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1)) : a * b = b * a

theorem pointedFundamentalGroupHom_schemeNsmul (G : RelativeGroupLaw K f) (n : ℕ)
    (a : π₁ᵉᵗ((G.one (𝟙 (Spec (.of K)))).1)) :
    pointedFundamentalGroupHom (G.schemeNsmul n)
      (G.one (𝟙 (Spec (.of K)))).1 (G.one (𝟙 (Spec (.of K)))).1
      (G.unit_comp_schemeNsmul n) a = a ^ n