{-# OPTIONS --safe --lossy-unification #-}

module Cubical.ZCohomology.CohomologyRings.RP2wedgeS1 where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels

open import Cubical.Relation.Nullary

open import Cubical.Data.Empty as 
open import Cubical.Data.Unit
open import Cubical.Data.Bool
open import Cubical.Data.Nat using ( ; zero ; suc ; discreteℕ ; suc-predℕ ; +-comm)
open import Cubical.Data.Int
open import Cubical.Data.Int.IsEven
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Vec
open import Cubical.Data.FinData

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Group.Instances.Unit
open import Cubical.Algebra.Group.Instances.Bool
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.Ring

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.Quotient
open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤCommRing to ℤCR)
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-Quotient
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-notationZ

open import Cubical.HITs.Truncation
open import Cubical.HITs.SetTruncation as ST
open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.SetQuotients as SQ renaming (_/_ to _/sq_)
open import Cubical.HITs.Sn
open import Cubical.HITs.RPn.Base

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.RingLaws
open import Cubical.ZCohomology.RingStructure.CohomologyRing
open import Cubical.ZCohomology.Groups.RP2wedgeS1
open import Cubical.ZCohomology.CohomologyRings.CupProductProperties

open Iso


{- Convention over ℤ[X,Y]
   X : (1,0)
   Y : (0,1)
-}

module Equiv-RP²⋁S¹-Properties
  (e₁ : GroupIso ℤGroup (coHomGr 1 RP²⋁S¹))
  (e₂ : GroupIso BoolGroup (coHomGr 2 RP²⋁S¹))
  where


-----------------------------------------------------------------------------
-- Definitions, Import with notations, Partition

  -- Definition
  private
    ℤAG = Ring→AbGroup (CommRing→Ring ℤCR)

  <2Y,Y²,XY,X²> : FinVec ℤ[x,y] 4
  <2Y,Y²,XY,X²> zero  = base (0  1  []) 2
  <2Y,Y²,XY,X²> one   = base (0  2  []) 1
  <2Y,Y²,XY,X²> two   = base (1  1  []) 1
  <2Y,Y²,XY,X²> three = base (2  0  []) 1

  ℤ[X,Y]/<2Y,Y²,XY,X²> : CommRing ℓ-zero
  ℤ[X,Y]/<2Y,Y²,XY,X²> = PolyCommRing-Quotient ℤCR <2Y,Y²,XY,X²>

  ℤ[x,y]/<2y,y²,xy,x²> : Type ℓ-zero
  ℤ[x,y]/<2y,y²,xy,x²> = fst ℤ[X,Y]/<2Y,Y²,XY,X²>

  -- Import with notation
  open IsGroupHom
  open gradedRingProperties

  open GroupStr (snd BoolGroup) using ()
    renaming
    ( 1g        to 0gBool
    ; _·_       to _+Bool_
    ; inv       to -Bool_
    ; ·Assoc    to +BoolAssoc
    ; ·IdL      to +BoolIdL
    ; ·IdR      to +BoolIdR
    ; is-set    to isSetBool   )

  open CommRingStr (snd ℤCR) using ()
    renaming
    ( 0r        to 0ℤ
    ; 1r        to 1ℤ
    ; _+_       to _+ℤ_
    ; -_        to -ℤ_
    ; _·_       to _·ℤ_
    ; +Assoc    to +ℤAssoc
    ; +IdL      to +ℤIdL
    ; +IdR      to +ℤIdR
    ; +Comm     to +ℤComm
    ; ·Assoc    to ·ℤAssoc
    ; ·IdL      to ·ℤIdL
    ; ·IdR      to ·ℤIdR
    ; ·DistR+   to ·ℤDistR+
    ; ·Comm     to ·ℤComm
    ; is-set    to isSetℤ     )

  open RingStr (snd (H*R RP²⋁S¹)) using ()
    renaming
    ( 0r        to 0H*
    ; 1r        to 1H*
    ; _+_       to _+H*_
    ; -_        to -H*_
    ; _·_       to _cup_
    ; +Assoc    to +H*Assoc
    ; +IdL      to +H*IdL
    ; +IdR      to +H*IdR
    ; +Comm     to +H*Comm
    ; ·Assoc    to ·H*Assoc
    ; ·IdL      to ·H*IdL
    ; ·IdR      to ·H*IdR
    ; ·DistR+   to ·H*DistR+
    ; is-set    to isSetH*     )

  open CommRingStr (snd ℤ[X,Y]) using ()
    renaming
    ( 0r        to 0Pℤ
    ; 1r        to 1Pℤ
    ; _+_       to _+Pℤ_
    ; -_        to -Pℤ_
    ; _·_       to _·Pℤ_
    ; +Assoc    to +PℤAssoc
    ; +IdL      to +PℤIdL
    ; +IdR      to +PℤIdR
    ; +Comm     to +PℤComm
    ; ·Assoc    to ·PℤAssoc
    ; ·IdL      to ·PℤIdL
    ; ·IdR      to ·PℤIdR
    ; ·Comm     to ·PℤComm
    ; ·DistR+   to ·PℤDistR+
    ; is-set    to isSetPℤ     )

  open CommRingStr (snd ℤ[X,Y]/<2Y,Y²,XY,X²>) using ()
    renaming
    ( 0r        to 0PℤI
    ; 1r        to 1PℤI
    ; _+_       to _+PℤI_
    ; -_        to -PℤI_
    ; _·_       to _·PℤI_
    ; +Assoc    to +PℤIAssoc
    ; +IdL      to +PℤIIdL
    ; +IdR      to +PℤIIdR
    ; +Comm     to +PℤIComm
    ; ·Assoc    to ·PℤIAssoc
    ; ·IdL      to ·PℤIIdL
    ; ·IdR      to ·PℤIIdR
    ; ·DistR+   to ·PℤIDistR+
    ; is-set    to isSetPℤI     )


  e₀ = invGroupIso H⁰-RP²⋁S¹≅ℤ
  ϕ₀ = fun (fst e₀)
  ϕ₀str = snd e₀
  ϕ₀⁻¹ = inv (fst e₀)
  ϕ₀⁻¹str = snd (invGroupIso e₀)
  ϕ₀-sect = rightInv (fst e₀)
  ϕ₀-retr = leftInv (fst e₀)

  ϕ₁ = fun (fst e₁)
  ϕ₁str = snd e₁
  ϕ₁⁻¹ = inv (fst e₁)
  ϕ₁⁻¹str = snd (invGroupIso e₁)
  ϕ₁-sect = rightInv (fst e₁)
  ϕ₁-retr = leftInv (fst e₁)

  ϕ₂ = fun (fst e₂)
  ϕ₂str = snd e₂
  ϕ₂⁻¹ = inv (fst e₂)
  ϕ₂⁻¹str = snd (invGroupIso e₂)
  ϕ₂-sect = rightInv (fst e₂)
  ϕ₂-retr = leftInv (fst e₂)

  module PblComp
    (null-H¹  : (a b : )  (ϕ₁ a)   (ϕ₁ b)  0ₕ 2)
    where

  -----------------------------------------------------------------------------
  -- Direct Sens on ℤ[x,y]

    ψ₂ :   Bool
    ψ₂ = isEven

    ϕ₂∘ψ₂str : IsGroupHom (snd ℤGroup) (ϕ₂  ψ₂) (snd (coHomGr 2 RP²⋁S¹))
    ϕ₂∘ψ₂str = isGroupHomComp (ψ₂ , isEven-GroupMorphism) (ϕ₂ , ϕ₂str)

    ℤ[x,y]→H*-RP²⋁S¹ : ℤ[x,y]  H* RP²⋁S¹
    ℤ[x,y]→H*-RP²⋁S¹ = DS-Rec-Set.f _ _ _ _ isSetH*
                        0H*
                        ϕ
                        _+H*_
                        +H*Assoc
                        +H*IdR
                        +H*Comm
                        base-neutral-eq
                        base-add-eq
     where
     ϕ : _
     ϕ (zero         zero         []) a = base 0 (ϕ₀ a)
     ϕ (zero         one          []) a = base 2 ((ϕ₂  ψ₂) a)
     ϕ (zero         suc (suc m)  []) a = 0H*
     ϕ (one          zero         []) a = base 1 (ϕ₁ a)
     ϕ (one          suc m        []) a = 0H*
     ϕ (suc (suc n)  m            []) a = 0H*

     base-neutral-eq : _
     base-neutral-eq (zero         zero         []) = cong (base 0) (pres1 ϕ₀str)  base-neutral _
     base-neutral-eq (zero         one          []) = cong (base 2) (pres1 ϕ₂∘ψ₂str)  base-neutral _
     base-neutral-eq (zero         suc (suc m)  []) = refl
     base-neutral-eq (one          zero         []) = cong (base 1) (pres1 ϕ₁str)  base-neutral _
     base-neutral-eq (one          suc m        []) = refl
     base-neutral-eq (suc (suc n)  m            []) = refl

     base-add-eq : _
     base-add-eq (zero         zero         []) a b = base-add _ _ _  cong (base 0) (sym (pres· ϕ₀str _ _))
     base-add-eq (zero         one          []) a b = base-add _ _ _  cong (base 2) (sym (pres· ϕ₂∘ψ₂str _ _))
     base-add-eq (zero         suc (suc m)  []) a b = +H*IdR _
     base-add-eq (one          zero         []) a b = base-add _ _ _  cong (base 1) (sym (pres· ϕ₁str _ _))
     base-add-eq (one          suc m        []) a b = +H*IdR _
     base-add-eq (suc (suc n)  m            []) a b = +H*IdR _

  -----------------------------------------------------------------------------
  -- Morphism on ℤ[x]

    ℤ[x,y]→H*-RP²⋁S¹-pres1 : ℤ[x,y]→H*-RP²⋁S¹ (1Pℤ)  1H*
    ℤ[x,y]→H*-RP²⋁S¹-pres1 = refl

    ℤ[x,y]→H*-RP²⋁S¹-pres+ : (x y : ℤ[x,y])  ℤ[x,y]→H*-RP²⋁S¹ (x +Pℤ y)  ℤ[x,y]→H*-RP²⋁S¹ x +H* ℤ[x,y]→H*-RP²⋁S¹ y
    ℤ[x,y]→H*-RP²⋁S¹-pres+ x y = refl

    --           Explanation of the product proof
    --
    --           -------------------------------------------------------
    --           | (0,0) | (0,1) | (0,m+2) | (1,0) | (1,m+1) | (n+2,m) |
    -- -----------------------------------------------------------------
    -- | (0,0)   |   H⁰  |   H⁰  |    0    |   H⁰  |    0    |    0    |
    -- -----------------------------------------------------------------
    -- | (0,1)   |  Sym  |   0₄  |    0    |   0₃  |    0    |    0    |
    -- -----------------------------------------------------------------
    -- | (0,m+2) | ==========================================> triv    |
    -- -----------------------------------------------------------------
    -- | (1,0)   |  Sym  |  Sym  |    0    |   ★  |    0    |    0    |
    -- -----------------------------------------------------------------
    -- | (1,m+1) | ==========================================> triv    |
    -- -----------------------------------------------------------------
    -- | (n+2,m) | ==========================================> triv    |
    -- -----------------------------------------------------------------

    -- ★ : prove that ϕ₁(1) ⌣ ϕ₁(1) ≡ 0

    open pres⌣


    ϕ₀-gen : (n : )  (f : coHom n RP²⋁S¹)  ϕ₀ (pos 1)  f  f
    ϕ₀-gen n = ST.elim  _  isProp→isSet (GroupStr.is-set (snd (coHomGr n RP²⋁S¹)) _ _))
                        f  cong ∣_∣₂ (funExt  x  rUnitₖ n (f x))))

    -- note that the proof might be simpliale by adding a second partition on T
    -- side, though it might complicated a bunch of things
    pres·-int : (n m : )  (a : )  (k l : )  (b : ) 
                   ℤ[x,y]→H*-RP²⋁S¹ (base (n  m  []) a ·Pℤ base (k  l  []) b)
                 ℤ[x,y]→H*-RP²⋁S¹ (base (n  m  []) a) cup ℤ[x,y]→H*-RP²⋁S¹ (base (k  l  []) b)

      -- non trivial case (0,0)
    pres·-int zero zero a zero zero          b = cong (base 0) (ϕₙ⌣ϕₘ _ ϕ₀str _ ϕ₀str _ ϕ₀str (ϕ₀-gen _ _) _ _)
    pres·-int zero zero a zero one           b = cong (base 2) (ϕₙ⌣ϕₘ _ ϕ₀str _ ϕ₂∘ψ₂str _ ϕ₂∘ψ₂str (ϕ₀-gen _ _) _ _)
    pres·-int zero zero a zero (suc (suc l)) b = refl
    pres·-int zero zero a one zero           b = cong (base 1) (ϕₙ⌣ϕₘ _ ϕ₀str _ ϕ₁str _ ϕ₁str (ϕ₀-gen _ _) _ _)
    pres·-int zero zero a one (suc l)        b = refl
    pres·-int zero zero a (suc (suc k)) l    b = refl
      -- non trivial case (0,1)
    pres·-int zero one a zero  zero         b = cong ℤ[x,y]→H*-RP²⋁S¹ (·PℤComm (base (0  1  []) a) (base (0  0  []) b))
                                                 pres·-int 0 0 b 0 1 a
                                                 gradCommRing RP²⋁S¹ _ _ _ _
    pres·-int zero one a zero  one          b = sym (base-neutral 4)
                                                 cong (base 4) (unitGroupEq (Hⁿ-RP²⋁S¹≅0 1) _ _)
    pres·-int zero one a zero (suc (suc l)) b = refl
    pres·-int zero one a one zero           b = sym (base-neutral 3)
                                                 cong (base 3) (unitGroupEq (Hⁿ-RP²⋁S¹≅0 0) _ _)
    pres·-int zero one a one (suc l)        b = refl
    pres·-int zero one a (suc (suc k)) l    b = refl
      -- trivial case (0, m+2)
    pres·-int zero (suc (suc m)) a  zero         l b = refl
    pres·-int zero (suc (suc m)) a  one          l b = refl
    pres·-int zero (suc (suc m)) a (suc (suc k)) l b = refl
      -- non trivial case (1,0)
    pres·-int one zero a zero zero          b = cong ℤ[x,y]→H*-RP²⋁S¹ (·PℤComm (base (1  0  []) a) (base (0  0  []) b))
                                                 pres·-int 0 0 b 1 0 a
                                                 gradCommRing RP²⋁S¹ _ _ _ _
    pres·-int one zero a zero one           b = cong ℤ[x,y]→H*-RP²⋁S¹ (·PℤComm (base (1  0  []) a) (base (0  1  []) b))
                                                 pres·-int 0 1 b 1 0 a
                                                 gradCommRing RP²⋁S¹ _ _ _ _
    pres·-int one zero a zero (suc (suc l)) b = refl
    pres·-int one zero a one zero           b = sym (base-neutral 2)
                                                 cong (base 2) (sym (null-H¹ _ _))
    pres·-int one zero a one (suc l)        b = refl
    pres·-int one zero a (suc (suc k)) l    b = refl
      -- trivial case (1,m+1)
    pres·-int one (suc m) a  zero   l b = refl
    pres·-int one (suc m) a (suc k) l b = refl
      -- trivial case (n+2,m)
    pres·-int (suc (suc n)) m a k l b = refl



    pres·-base-case-vec : (v : Vec  2)  (a : )  (v' : Vec  2)  (b : ) 
                             ℤ[x,y]→H*-RP²⋁S¹ (base v a ·Pℤ base v' b)
                           ℤ[x,y]→H*-RP²⋁S¹ (base v a) cup ℤ[x,y]→H*-RP²⋁S¹ (base v' b)
    pres·-base-case-vec (n  m  []) a (k  l  []) b = pres·-int n m a k l b

    -- proof of the morphism
    ℤ[x,y]→H*-RP²⋁S¹-pres· : (x y : ℤ[x,y])  ℤ[x,y]→H*-RP²⋁S¹ (x ·Pℤ y)  ℤ[x,y]→H*-RP²⋁S¹ x cup ℤ[x,y]→H*-RP²⋁S¹ y
    ℤ[x,y]→H*-RP²⋁S¹-pres· = DS-Ind-Prop.f _ _ _ _
                            x p q i y j  isSetH* _ _ (p y) (q y) i j)
                            y  refl)
                           base-case
                           λ {U V} ind-U ind-V y  cong₂ _+H*_ (ind-U y) (ind-V y)
      where
      base-case : _
      base-case v a = DS-Ind-Prop.f _ _ _ _  _  isSetH* _ _)
                             (sym (RingTheory.0RightAnnihilates (H*R RP²⋁S¹) _))
                              v' b  pres·-base-case-vec v a v' b )
                             λ {U V} ind-U ind-V  (cong₂ _+H*_ ind-U ind-V)  sym (·H*DistR+ _ _ _)


  -----------------------------------------------------------------------------
  -- Function on ℤ[x]/x + morphism

    -- not a trivial cancel ?
    ℤ[x,y]→H*-RP²⋁S¹-cancel : (x : Fin 4)  ℤ[x,y]→H*-RP²⋁S¹ (<2Y,Y²,XY,X²> x)  0H*
    ℤ[x,y]→H*-RP²⋁S¹-cancel zero = cong (base 2) (pres1 ϕ₂str)  base-neutral _
    ℤ[x,y]→H*-RP²⋁S¹-cancel one = refl
    ℤ[x,y]→H*-RP²⋁S¹-cancel two = refl
    ℤ[x,y]→H*-RP²⋁S¹-cancel three = refl


    ℤ[X,Y]→H*-RP²⋁S¹ : RingHom (CommRing→Ring ℤ[X,Y]) (H*R RP²⋁S¹)
    fst ℤ[X,Y]→H*-RP²⋁S¹ = ℤ[x,y]→H*-RP²⋁S¹
    snd ℤ[X,Y]→H*-RP²⋁S¹ = makeIsRingHom ℤ[x,y]→H*-RP²⋁S¹-pres1
                                       ℤ[x,y]→H*-RP²⋁S¹-pres+
                                       ℤ[x,y]→H*-RP²⋁S¹-pres·

    -- hence not a trivial pres+, yet pres0 still is
    ℤ[X,Y]/<2Y,Y²,XY,X²>→H*R-RP²⋁S¹ : RingHom (CommRing→Ring ℤ[X,Y]/<2Y,Y²,XY,X²>) (H*R RP²⋁S¹)
    ℤ[X,Y]/<2Y,Y²,XY,X²>→H*R-RP²⋁S¹ = Quotient-FGideal-CommRing-Ring.inducedHom
                                    ℤ[X,Y] (H*R RP²⋁S¹) ℤ[X,Y]→H*-RP²⋁S¹
                                    <2Y,Y²,XY,X²> ℤ[x,y]→H*-RP²⋁S¹-cancel

    ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹ : ℤ[x,y]/<2y,y²,xy,x²>  H* RP²⋁S¹
    ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹ = fst ℤ[X,Y]/<2Y,Y²,XY,X²>→H*R-RP²⋁S¹

    ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹-pres0 : ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹ 0PℤI  0H*
    ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹-pres0 = refl

    ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹-pres+ : (x y : ℤ[x,y]/<2y,y²,xy,x²>) 
                                             ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹ ( x +PℤI y)
                                           ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹ x +H* ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹ y
    ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹-pres+ x y = IsRingHom.pres+ (snd ℤ[X,Y]/<2Y,Y²,XY,X²>→H*R-RP²⋁S¹) x y


  -----------------------------------------------------------------------------
  -- Converse Sens on H* → ℤ[X,Y]

    ψ₂⁻¹ : Bool  
    ψ₂⁻¹ false = 1
    ψ₂⁻¹ true = 0

    private
    -- Those lemma are requiered because ψ₂⁻¹
    -- is a morphism only under the quotient
      Λ : (x : Bool)  ℤ[x,y]/<2y,y²,xy,x²>
      Λ x = [ (base (0  1  []) (ψ₂⁻¹ x)) ]

      Λ-pres+ : (x y : Bool)  Λ x +PℤI Λ y  Λ (x +Bool y)
      Λ-pres+ false false = cong [_] (base-add _ _ _)
                             eq/ (base (0  1  []) 2)
                                  (base (0  1  []) 0)
                                   ((λ {zero  base (0  0  []) 1 ; one  0Pℤ ; two  0Pℤ ; three  0Pℤ}) , helper) ∣₁
              where
              helper : _
              helper = base-add  _ _ _
                        sym (cong₂ _+Pℤ_ refl (+PℤIdL _  +PℤIdL _  +PℤIdL _)  +PℤIdR _)
      Λ-pres+ false true = cong [_] (base-add _ _ _)
      Λ-pres+ true false = cong [_] (base-add _ _ _)
      Λ-pres+ true true = cong [_] (base-add _ _ _)

    ϕ⁻¹ : (k : )  (a : coHom k RP²⋁S¹)  ℤ[x,y]/<2y,y²,xy,x²>
    ϕ⁻¹ zero a = [ base (0  0  []) (ϕ₀⁻¹ a) ]
    ϕ⁻¹ one a = [ base (1  0  []) (ϕ₁⁻¹ a) ]
    ϕ⁻¹ two a = [ base (0  1  []) ((ψ₂⁻¹  ϕ₂⁻¹) a) ]
    ϕ⁻¹ (suc (suc (suc k))) a = 0PℤI

    H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²> : H* RP²⋁S¹  ℤ[x,y]/<2y,y²,xy,x²>
    H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²> = DS-Rec-Set.f _ _ _ _ isSetPℤI
         0PℤI
         ϕ⁻¹
         _+PℤI_
         +PℤIAssoc
         +PℤIIdR
         +PℤIComm
         base-neutral-eq
         base-add-eq
      where

      base-neutral-eq : _
      base-neutral-eq zero = cong [_] (cong (base {AGP = λ _  snd ℤAG} (0  0  [])) (pres1 ϕ₀⁻¹str)
                                        (base-neutral _))
      base-neutral-eq one = cong [_] (cong (base {AGP = λ _  snd ℤAG} (1  0  [])) (pres1 ϕ₁⁻¹str)
                                        (base-neutral _))
      base-neutral-eq two = cong [_] (cong (base (0  1  [])) (cong ψ₂⁻¹ (pres1 ϕ₂⁻¹str))
                                      base-neutral _)
      base-neutral-eq (suc (suc (suc k))) = refl

      base-add-eq : _
      base-add-eq zero a b = cong [_] (base-add _ _ _  cong (base (0  0  [])) (sym (pres· ϕ₀⁻¹str _ _)))
      base-add-eq one a b = cong [_] (base-add _ _ _  cong (base (1  0  [])) (sym (pres· ϕ₁⁻¹str _ _)))
      base-add-eq two a b = Λ-pres+ (ϕ₂⁻¹ a) (ϕ₂⁻¹ b)
                             cong [_] (cong (base (0  1  [])) (cong ψ₂⁻¹ (sym (pres· ϕ₂⁻¹str _ _))))
      base-add-eq (suc (suc (suc k))) a b = +PℤIIdR _

    H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²>-pres0 : H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²> 0H*  0PℤI
    H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²>-pres0 = refl

    H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²>-pres+ : (x y : H* RP²⋁S¹) 
                                               H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²> (x +H* y)
                                            (H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²> x) +PℤI (H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²> y)
    H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²>-pres+ x y = refl



  -----------------------------------------------------------------------------
  -- Section

    ψ₂-sect : (x : Bool)  ψ₂ (ψ₂⁻¹ x)  x
    ψ₂-sect false = refl
    ψ₂-sect true = refl


    e-sect-base : (k : )  (a : coHom k RP²⋁S¹) 
                  ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹ (ϕ⁻¹ k a)  base k a
    e-sect-base zero a = cong (base 0) (ϕ₀-sect a)
    e-sect-base one a = cong (base 1) (ϕ₁-sect a)
    e-sect-base two a = cong (base 2) (cong ϕ₂ (ψ₂-sect _)  ϕ₂-sect a)
    e-sect-base (suc (suc (suc k))) a = sym (base-neutral (suc (suc (suc k))))
                                         cong (base (suc (suc (suc k)))) (unitGroupEq (Hⁿ-RP²⋁S¹≅0 k) _ _)

    e-sect : (x : H* RP²⋁S¹)  ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹ (H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²> x)  x
    e-sect = DS-Ind-Prop.f _ _ _ _  _  isSetH* _ _)
             refl
             e-sect-base
             λ {U V} ind-U ind-V  ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹-pres+ _ _  cong₂ _+H*_ ind-U ind-V



  -----------------------------------------------------------------------------
  -- Retraction

    e-retr-ψ₂-false : (a : )  (isEven a  false)  Λ (ψ₂ a)  [ base (0  1  []) a ]
    e-retr-ψ₂-false a x = cong [_] (cong (base (0  1  [])) (cong ψ₂⁻¹ x))
                     eq/ (base (0  1  []) 1) (base (0  1  []) a)
                       ((λ {zero  base (0  0  []) (-ℤ m) ; one  0Pℤ ; two  0Pℤ ; three  0Pℤ}) , helper) ∣₁
              where
              m = fst (isEvenFalse a x)

              helper : _
              helper = base-add _ _ _
                        cong (base (0  1  [])) (cong  X  1 +ℤ (-ℤ X)) (snd (isEvenFalse a x))
                                                cong  X  1 +ℤ X) (-Dist+ _ _)
                                                +ℤAssoc _ _ _
                                                +ℤIdL _)
                        sym (cong₂ _+Pℤ_ (cong (base (0  1  [])) (sym (-DistL· _ _)  cong -ℤ_ (·ℤComm _ _)))
                                          (+PℤIdL _  +PℤIdL _  +PℤIdL _)
                              +PℤIdR _)

    e-retr-ψ₂-true : (a : )  (isEven a  true)  Λ (ψ₂ a)  [ base (0  1  []) a ]
    e-retr-ψ₂-true a x = cong [_] (cong (base (0  1  [])) (cong ψ₂⁻¹ x))
                     eq/ (base (0  1  []) 0) (base (0  1  []) a)
                       ((λ {zero  base (0  0  []) (-ℤ m) ; one  0Pℤ ; two  0Pℤ ; three  0Pℤ}) , helper) ∣₁
              where
              m = fst (isEvenTrue a x)

              helper : _
              helper = base-add _ _ _
                        cong (base (0  1  [])) (+ℤIdL _  cong -ℤ_ (snd (isEvenTrue a x)))
                        sym (cong₂ _+Pℤ_ (cong (base (0  1  [])) (sym (-DistL· _ _)  cong -ℤ_ (·ℤComm _ _)))
                                          (+PℤIdL _  +PℤIdL _  +PℤIdL _)
                              +PℤIdR _)


    e-retr-ψ₂ : (a : )  ((isEven a  false)  (isEven a  true))  Λ (ψ₂ a)  [ base (0  1  []) a ]
    e-retr-ψ₂ a (inl x) = e-retr-ψ₂-false a x
    e-retr-ψ₂ a (inr x) = e-retr-ψ₂-true a x



    e-retr-base : (v : Vec  2)  (a : ) 
                  H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²> (ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹ [ base v a ])  [ base v a ]
    e-retr-base (zero         zero         []) a = cong [_] (cong (base (0  0  [])) (ϕ₀-retr a))
    e-retr-base (zero         one          []) a = cong [_] (cong (base (0  1  [])) (cong ψ₂⁻¹ (ϕ₂-retr (ψ₂ a))))
                                                       e-retr-ψ₂ a (dichotomyBoolSym (isEven a))
    e-retr-base (zero         suc (suc m)  []) a = eq/ _ _  (v , helper) ∣₁
           where
           v = λ { zero  0Pℤ ; one  base (0  m  []) (-ℤ a) ; two  0Pℤ ; three  0Pℤ }
           helper : _
           helper = +PℤIdL _  sym (+PℤIdL _
                     cong₂ _+Pℤ_ (cong₂ base (cong  X  0  X  []) (+-comm _ _)) (·ℤIdR _))
                                  (+PℤIdL _  +PℤIdL _)  +PℤIdR _)
    e-retr-base (one          zero         []) a = cong [_] (cong (base (1  0  [])) (ϕ₁-retr a))
    e-retr-base (one          suc m        []) a = eq/ _ _  (v , helper) ∣₁
           where
           v = λ { zero  0Pℤ ; one  0Pℤ ; two  base (0  m  []) (-ℤ a) ; three  0Pℤ }
           helper : _
           helper = +PℤIdL _  sym (+PℤIdL _  +PℤIdL _
                     cong₂ _+Pℤ_ (cong₂ base (cong  X  1  X  []) (+-comm _ _)) (·ℤIdR _)) (+PℤIdL _)  +PℤIdR _)
    e-retr-base (suc (suc n)  m            []) a = eq/ _ _  (v , helper) ∣₁
           where
           v = λ {zero  0Pℤ ; one  0Pℤ ; two  0Pℤ ; three  base (n  m  []) (-ℤ a) }
           helper : _
           helper = +PℤIdL _  sym (+PℤIdL _  +PℤIdL _  +PℤIdL _  +PℤIdR _
                     cong₂ base (cong₂  X  λ Y  X  Y  []) (+-comm _ _) (+-comm _ _)) (·ℤIdR _))

    e-retr : (x : ℤ[x,y]/<2y,y²,xy,x²>)  H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²> (ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹ x)  x
    e-retr = SQ.elimProp  _  isSetPℤI _ _)
             (DS-Ind-Prop.f _ _ _ _  _  isSetPℤI _ _)
             refl
             e-retr-base
             λ {U V} ind-U ind-V  cong₂ _+PℤI_ ind-U ind-V)



-- Computation of the Cohomology Ring

module _ where

  open Equiv-RP²⋁S¹-Properties (invGroupIso H¹-RP²⋁S¹≅ℤ) (invGroupIso H²-RP²⋁S¹≅Bool)
  open pres⌣trivial
  open PblComp  a b  sym (ϕₙ⌣ϕₘ-0 ϕ₁ ϕ₁str ϕ₁ ϕ₁str trivial-cup a b))

  RP²⋁S¹-CohomologyRing : RingEquiv (CommRing→Ring ℤ[X,Y]/<2Y,Y²,XY,X²>) (H*R RP²⋁S¹)
  fst RP²⋁S¹-CohomologyRing = isoToEquiv is
    where
    is : Iso ℤ[x,y]/<2y,y²,xy,x²> (H* RP²⋁S¹)
    fun is = ℤ[x,y]/<2y,y²,xy,x²>→H*-RP²⋁S¹
    inv is = H*-RP²⋁S¹→ℤ[x,y]/<2y,y²,xy,x²>
    rightInv is = e-sect
    leftInv is = e-retr
  snd RP²⋁S¹-CohomologyRing = snd ℤ[X,Y]/<2Y,Y²,XY,X²>→H*R-RP²⋁S¹

  CohomologyRing-RP²⋁S¹ : RingEquiv (H*R RP²⋁S¹) (CommRing→Ring ℤ[X,Y]/<2Y,Y²,XY,X²>)
  CohomologyRing-RP²⋁S¹ = RingEquivs.invRingEquiv RP²⋁S¹-CohomologyRing