From 4a82e8493df67709505908ffe4c576f09ea949a9 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Wed, 5 Aug 2020 11:37:36 +0000
Subject: [PATCH] feat(algebra/*/ulift): algebraic instances for ulift (#3675)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
---
 src/algebra/group/ulift.lean  | 96 +++++++++++++++++++++++++++++++++++
 src/algebra/module/pi.lean    |  4 +-
 src/algebra/module/ulift.lean | 86 +++++++++++++++++++++++++++++++
 src/algebra/ring/ulift.lean   | 57 +++++++++++++++++++++
 4 files changed, 242 insertions(+), 1 deletion(-)
 create mode 100644 src/algebra/group/ulift.lean
 create mode 100644 src/algebra/module/ulift.lean
 create mode 100644 src/algebra/ring/ulift.lean

diff --git a/src/algebra/group/ulift.lean b/src/algebra/group/ulift.lean
new file mode 100644
index 0000000000000..23938c8878b74
--- /dev/null
+++ b/src/algebra/group/ulift.lean
@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import data.equiv.mul_add
+
+/-!
+# `ulift` instances for groups and monoids
+
+This file defines instances for group, monoid, semigroup and related structures on `ulift` types.
+
+(Recall `ulift α` is just a "copy" of a type `α` in a higher universe.)
+
+We use `tactic.pi_instance_derive_field`, even though it wasn't intended for this purpose,
+which seems to work fine.
+
+We also provide `ulift.mul_equiv : ulift R ≃* R` (and its additive analogue).
+-/
+
+universes u v
+variables {α : Type u} {x y : ulift.{v} α}
+
+namespace ulift
+
+@[to_additive] instance has_one [has_one α] : has_one (ulift α) := ⟨⟨1⟩⟩
+@[simp, to_additive] lemma one_down [has_one α] : (1 : ulift α).down = 1 := rfl
+
+@[to_additive]
+instance has_mul [has_mul α] : has_mul (ulift α) := ⟨λ f g, ⟨f.down * g.down⟩⟩
+@[simp, to_additive] lemma mul_down [has_mul α] : (x * y).down = x.down * y.down := rfl
+
+@[to_additive] instance has_inv [has_inv α] : has_inv (ulift α) := ⟨λ f, ⟨f.down⁻¹⟩⟩
+@[simp, to_additive] lemma inv_down [has_inv α] : x⁻¹.down = (x.down)⁻¹ := rfl
+
+@[to_additive]
+instance semigroup [semigroup α] : semigroup (ulift α) :=
+by refine_struct { mul := (*), .. }; tactic.pi_instance_derive_field
+
+/--
+The multiplicative equivalence between `ulift α` and `α`.
+-/
+@[to_additive "The additive equivalence between `ulift α` and `α`."]
+def mul_equiv [semigroup α] : ulift α ≃* α :=
+{ to_fun := ulift.down,
+  inv_fun := ulift.up,
+  map_mul' := λ x y, rfl,
+  left_inv := by tidy,
+  right_inv := by tidy, }
+
+@[to_additive]
+instance comm_semigroup [comm_semigroup α] : comm_semigroup (ulift α) :=
+by refine_struct { mul := (*), .. }; tactic.pi_instance_derive_field
+
+@[to_additive]
+instance monoid [monoid α] : monoid (ulift α) :=
+by refine_struct { one := (1 : ulift α), mul := (*), .. }; tactic.pi_instance_derive_field
+
+@[to_additive]
+instance comm_monoid [comm_monoid α] : comm_monoid (ulift α) :=
+by refine_struct { one := (1 : ulift α), mul := (*), .. }; tactic.pi_instance_derive_field
+
+@[to_additive]
+instance group [group α] : group (ulift α) :=
+by refine_struct { one := (1 : ulift α), mul := (*), inv := has_inv.inv, .. };
+  tactic.pi_instance_derive_field
+
+@[simp] lemma sub_down [add_group α] : (x - y).down = x.down - y.down := rfl
+
+@[to_additive]
+instance comm_group [comm_group α] : comm_group (ulift α) :=
+by refine_struct { one := (1 : ulift α), mul := (*), inv := has_inv.inv, .. };
+  tactic.pi_instance_derive_field
+
+@[to_additive add_left_cancel_semigroup]
+instance left_cancel_semigroup [left_cancel_semigroup α] :
+  left_cancel_semigroup (ulift α) :=
+begin
+  refine_struct { mul := (*) }; tactic.pi_instance_derive_field,
+  replace a_1 := congr_arg ulift.down a_1,
+  assumption,
+end
+
+@[to_additive add_right_cancel_semigroup]
+instance right_cancel_semigroup [right_cancel_semigroup α] :
+  right_cancel_semigroup (ulift α) :=
+begin
+  refine_struct { mul := (*) }; tactic.pi_instance_derive_field,
+  replace a_1 := congr_arg ulift.down a_1,
+  assumption,
+end
+
+-- TODO we don't do `ordered_cancel_comm_monoid` or `ordered_comm_group`
+-- We'd need to add instances for `ulift` in `order.basic`.
+
+end ulift
diff --git a/src/algebra/module/pi.lean b/src/algebra/module/pi.lean
index 5ab8521fc21cf..3b17d6e572b5b 100644
--- a/src/algebra/module/pi.lean
+++ b/src/algebra/module/pi.lean
@@ -3,7 +3,9 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
-import algebra.module.basic algebra.ring.pi
+import algebra.module.basic
+import algebra.ring.pi
+
 /-!
 # Pi instances for module and multiplicative actions
 
diff --git a/src/algebra/module/ulift.lean b/src/algebra/module/ulift.lean
new file mode 100644
index 0000000000000..d36841f216f58
--- /dev/null
+++ b/src/algebra/module/ulift.lean
@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import linear_algebra.basic
+import algebra.ring.ulift
+
+/-!
+# `ulift` instances for module and multiplicative actions
+
+This file defines instances for module, mul_action and related structures on `ulift` types.
+
+(Recall `ulift α` is just a "copy" of a type `α` in a higher universe.)
+
+We also provide `ulift.semimodule_equiv : ulift M ≃ₗ[R] M`.
+
+-/
+
+namespace ulift
+universes u v w
+variable {R : Type u}
+variable {M : Type v}
+
+instance has_scalar [has_scalar R M] :
+  has_scalar (ulift R) M :=
+⟨λ s x, s.down • x⟩
+
+@[simp] lemma smul_down [has_scalar R M] (s : ulift R) (x : M) : (s • x) = s.down • x := rfl
+
+instance has_scalar' [has_scalar R M] :
+  has_scalar R (ulift M) :=
+⟨λ s x, ⟨s • x.down⟩⟩
+
+@[simp]
+lemma smul_down' [has_scalar R M] (s : R) (x : ulift M) :
+  (s • x).down = s • x.down :=
+rfl
+
+instance mul_action [monoid R] [mul_action R M] :
+  mul_action (ulift R) M :=
+{ smul := (•),
+  mul_smul := λ r s f, by { cases r, cases s, simp [mul_smul], },
+  one_smul := λ f, by { simp [one_smul], } }
+
+instance mul_action' [monoid R] [mul_action R M] :
+  mul_action R (ulift M) :=
+{ smul := (•),
+  mul_smul := λ r s f, by { cases f, ext, simp [mul_smul], },
+  one_smul := λ f, by { ext, simp [one_smul], } }
+
+instance distrib_mul_action [monoid R] [add_monoid M] [distrib_mul_action R M] :
+  distrib_mul_action (ulift R) M :=
+{ smul_zero := λ c, by { cases c, simp [smul_zero], },
+  smul_add := λ c f g, by { cases c, simp [smul_add], },
+  ..ulift.mul_action }
+
+instance distrib_mul_action' [monoid R] [add_monoid M] [distrib_mul_action R M] :
+  distrib_mul_action R (ulift M) :=
+{ smul_zero := λ c, by { ext, simp [smul_zero], },
+  smul_add := λ c f g, by { ext, simp [smul_add], },
+  ..ulift.mul_action' }
+
+instance semimodule [semiring R] [add_comm_monoid M] [semimodule R M] :
+  semimodule (ulift R) M :=
+{ add_smul := λ c f g, by { cases c, simp [add_smul], },
+  zero_smul := λ f, by { simp [zero_smul], },
+  ..ulift.distrib_mul_action }
+
+instance semimodule' [semiring R] [add_comm_monoid M] [semimodule R M] :
+  semimodule R (ulift M) :=
+{ add_smul := by { intros, ext1, apply add_smul },
+  zero_smul := by { intros, ext1, apply zero_smul } }
+
+/--
+The `R`-linear equivalence between `ulift M` and `M`.
+-/
+def semimodule_equiv [semiring R] [add_comm_monoid M] [semimodule R M] : ulift M ≃ₗ[R] M :=
+{ to_fun := ulift.down,
+  inv_fun := ulift.up,
+  map_smul' := λ r x, rfl,
+  map_add' := λ x y, rfl,
+  left_inv := by tidy,
+  right_inv := by tidy, }
+
+end ulift
diff --git a/src/algebra/ring/ulift.lean b/src/algebra/ring/ulift.lean
new file mode 100644
index 0000000000000..aa5a3f18753ce
--- /dev/null
+++ b/src/algebra/ring/ulift.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import algebra.group.ulift
+import data.equiv.ring
+
+/-!
+# `ulift` instances for ring
+
+This file defines instances for ring, semiring and related structures on `ulift` types.
+
+(Recall `ulift α` is just a "copy" of a type `α` in a higher universe.)
+
+We also provide `ulift.ring_equiv : ulift R ≃+* R`.
+-/
+
+universes u v
+variables {α : Type u} {x y : ulift.{v} α}
+
+namespace ulift
+
+instance mul_zero_class [mul_zero_class α] : mul_zero_class (ulift α) :=
+by refine_struct { zero := (0 : ulift α), mul := (*), .. }; tactic.pi_instance_derive_field
+
+instance distrib [distrib α] : distrib (ulift α) :=
+by refine_struct { add := (+), mul := (*), .. }; tactic.pi_instance_derive_field
+
+instance semiring [semiring α] : semiring (ulift α) :=
+by refine_struct { zero := (0 : ulift α), one := 1, add := (+), mul := (*), .. };
+  tactic.pi_instance_derive_field
+
+/--
+The ring equivalence between `ulift α` and `α`.
+-/
+def ring_equiv [semiring α] : ulift α ≃+* α :=
+{ to_fun := ulift.down,
+  inv_fun := ulift.up,
+  map_mul' := λ x y, rfl,
+  map_add' := λ x y, rfl,
+  left_inv := by tidy,
+  right_inv := by tidy, }
+
+instance comm_semiring [comm_semiring α] : comm_semiring (ulift α) :=
+by refine_struct { zero := (0 : ulift α), one := 1, add := (+), mul := (*),  .. };
+  tactic.pi_instance_derive_field
+
+instance ring [ring α] : ring (ulift α) :=
+by refine_struct { zero := (0 : ulift α), one := 1, add := (+), mul := (*),
+  neg := has_neg.neg, .. }; tactic.pi_instance_derive_field
+
+instance comm_ring [comm_ring α] : comm_ring (ulift α) :=
+by refine_struct { zero := (0 : ulift α), one := 1, add := (+), mul := (*),
+  neg := has_neg.neg, .. }; tactic.pi_instance_derive_field
+
+end ulift