Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(algebra/*/ulift): algebraic instances for ulift (#3675)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
- Loading branch information
1 parent
2b9ac69
commit 4a82e84
Showing
4 changed files
with
242 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |