/
ulift.lean
57 lines (43 loc) · 1.82 KB
/
ulift.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
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