From ba5648fb874a3bcb972764e368003bd7fb3094ca Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Mon, 10 Sep 2018 18:02:07 +0200
Subject: [PATCH] start on construction of cup product of EM-spaces

---
 algebra/ring.hlean    | 54 +++++++++++++++++++++++++++++++++++++++++++
 homotopy/EMRing.hlean | 53 ++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 107 insertions(+)
 create mode 100644 algebra/ring.hlean
 create mode 100644 homotopy/EMRing.hlean

diff --git a/algebra/ring.hlean b/algebra/ring.hlean
new file mode 100644
index 0000000..be89caf
--- /dev/null
+++ b/algebra/ring.hlean
@@ -0,0 +1,54 @@
+-- Authors: Floris van Doorn
+
+import algebra.ring .direct_sum ..heq ..move_to_lib
+
+open algebra group eq is_trunc sigma
+
+namespace algebra
+definition AbGroup_of_Ring [constructor] (R : Ring) : AbGroup :=
+AbGroup.mk R (add_ab_group_of_ring R)
+
+definition ring_AbGroup_of_Ring [instance] (R : Ring) : ring (AbGroup_of_Ring R) :=
+Ring.struct R
+
+definition ring_right_action [constructor] {R : Ring} (r : R) :
+  AbGroup_of_Ring R →g AbGroup_of_Ring R :=
+homomorphism.mk (λs, s * r) (λs s', !right_distrib)
+
+definition ring_of_ab_group [constructor] (G : Type) [ab_group G] (m : G → G → G) (o : G)
+  (lm : Πg, m o g = g) (rm : Πg, m g o = g) (am : Πg₁ g₂ g₃, m (m g₁ g₂) g₃ = m g₁ (m g₂ g₃))
+  (ld : Πg₁ g₂ g₃, m g₁ (g₂ * g₃) = m g₁ g₂ * m g₁ g₃)
+  (rd : Πg₁ g₂ g₃, m (g₁ * g₂) g₃ = m g₁ g₃ * m g₂ g₃) : ring G :=
+ring.mk _ mul mul.assoc 1 one_mul mul_one inv mul.left_inv mul.comm m am o lm rm ld rd
+
+definition Ring_of_AbGroup [constructor] (G : AbGroup) (m : G → G → G) (o : G)
+  (lm : Πg, m o g = g) (rm : Πg, m g o = g) (am : Πg₁ g₂ g₃, m (m g₁ g₂) g₃ = m g₁ (m g₂ g₃))
+  (ld : Πg₁ g₂ g₃, m g₁ (g₂ * g₃) = m g₁ g₂ * m g₁ g₃)
+  (rd : Πg₁ g₂ g₃, m (g₁ * g₂) g₃ = m g₁ g₃ * m g₂ g₃) : Ring :=
+Ring.mk G (ring_of_ab_group G m o lm rm am ld rd)
+
+/- graded ring -/
+
+structure graded_ring (M : Monoid) :=
+  (R : M → AddAbGroup)
+  (mul : Π⦃m m'⦄, R m → R m' → R (m * m'))
+  (one : R 1)
+  (mul_one : Π⦃m⦄ (r : R m), mul r one ==[R] r)
+  (one_mul : Π⦃m⦄ (r : R m), mul one r ==[R] r)
+  (mul_assoc : Π⦃m₁ m₂ m₃⦄ (r₁ : R m₁) (r₂ : R m₂) (r₃ : R m₃),
+    mul (mul r₁ r₂) r₃ ==[R] mul r₁ (mul r₂ r₃))
+  (mul_left_distrib : Π⦃m₁ m₂⦄ (r₁ : R m₁) (r₂ r₂' : R m₂),
+    mul r₁ (r₂ + r₂') = mul r₁ r₂ + mul r₁ r₂')
+  (mul_right_distrib : Π⦃m₁ m₂⦄ (r₁ r₁' : R m₁) (r₂ : R m₂),
+    mul (r₁ + r₁') r₂ = mul r₁ r₂ + mul r₁' r₂)
+
+
+attribute graded_ring.R [coercion]
+infixl ` ** `:71 := graded_ring.mul
+
+-- definition ring_direct_sum {M : Monoid} (R : graded_ring M) : Ring :=
+-- Ring_of_AbGroup (dirsum R) _ (dirsum_incl R 1 (graded_ring.one R)) _ _ _ _ _
+
+
+
+end algebra
diff --git a/homotopy/EMRing.hlean b/homotopy/EMRing.hlean
new file mode 100644
index 0000000..4b932fb
--- /dev/null
+++ b/homotopy/EMRing.hlean
@@ -0,0 +1,53 @@
+-- Authors: Floris van Doorn
+
+import .EM .smash_adjoint ..algebra.ring
+
+open algebra eq EM is_equiv equiv is_trunc is_conn pointed trunc susp smash group nat
+namespace EM
+
+definition EM1product_adj {R : Ring} :
+  EM1 (AbGroup_of_Ring R) →* ppmap (EM1 (AbGroup_of_Ring R)) (EMadd1 (AbGroup_of_Ring R) 1) :=
+begin
+  have is_trunc 1 (ppmap (EM1 (AbGroup_of_Ring R)) (EMadd1 (AbGroup_of_Ring R) 1)),
+    from is_trunc_pmap_of_is_conn _ _ _ _ _ _ (le.refl 2) !is_trunc_EMadd1,
+  fapply EM1_pmap,
+  { intro r, refine pfunext _ _, exact !loop_EM2⁻¹ᵉ* ∘* EM1_functor (ring_right_action r), },
+  { intro r r', exact sorry }
+end
+
+definition EMproduct_map {G H K : AbGroup} (φ : G → H →g K) (n m : ℕ) (g : G) :
+  EMadd1 H n →* EMadd1 K n :=
+begin
+  fapply EMadd1_functor (φ g) n
+end
+
+definition EM0EMadd1product {G H K : AbGroup} (φ : G →g H →gg K) (n : ℕ) :
+  G →* EMadd1 H n →** EMadd1 K n :=
+EMadd1_pfunctor H K n ∘* pmap_of_homomorphism φ
+
+definition EMadd1product {G H K : AbGroup} (φ : G →g H →gg K) (n m : ℕ) :
+  EMadd1 G n →* EMadd1 H m →** EMadd1 K (m + succ n) :=
+begin
+  assert H1 : is_trunc n.+1 (EMadd1 H m →** EMadd1 K (m + succ n)),
+  { refine is_trunc_pmap_of_is_conn _ (m.-1) !is_conn_EMadd1 _ _ _ _ !is_trunc_EMadd1,
+    exact le_of_eq (trunc_index.of_nat_add_plus_two_of_nat m n)⁻¹ᵖ },
+  fapply EMadd1_pmap,
+  { refine (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* ∘* ppcompose_left !loopn_EMadd1_add⁻¹ᵉ* ∘*
+      EM0EMadd1product φ m },
+  { exact sorry }
+end
+
+definition EMproduct {G H K : AbGroup} (φ : G →g H →gg K) (n m : ℕ) :
+  EM G n →* EM H m →** EM K (m + n) :=
+begin
+  cases n with n,
+  { cases m with m,
+    { exact pmap_of_homomorphism2 φ },
+    { exact EM0EMadd1product φ m }},
+  { cases m with m,
+    { exact ppcompose_left (ptransport (EMadd1 K) (zero_add n)⁻¹) ∘*
+        pmap_swap_map (EM0EMadd1product (homomorphism_swap φ) n) },
+    { exact ppcompose_left (ptransport (EMadd1 K) !succ_add⁻¹) ∘* EMadd1product φ n m }}
+end
+
+end EM