[Merged by Bors] - feat(algebra/*/ulift): algebraic instances for ulift

src/algebra/group/ulift.lean

@@ -0,0 +1,92 @@
+/-
+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.
+
+We use `tactic.pi_instance_derive_field`, even though it wasn't intended for this purpose,
+which seems to work fine.
+-/
+
+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_apply [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

src/algebra/ring/ulift.lean

@@ -0,0 +1,53 @@
+/-
+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
+
+/-!
+# Pi instances for ring
+
+This file defines instances for ring, semiring and related structures on Pi Types
+-/
+
+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