This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 298
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore(algebra/opposites): split group actions and division_ring into …
…their own files (#10383) This splits out `group_theory.group_action.opposite` and `algebra.field.opposite` from `algebra.opposites`. The motivation is to make opposite actions available slightly earlier in the import graph. We probably want to split out `ring` at some point too, but that's likely a more annoying change so I've left it for future work. These lemmas are just moved, and some `_root_` prefixes eliminated by removing the surrounding `namespace`.
- Loading branch information
1 parent
2aea996
commit d8d0c59
Showing
18 changed files
with
156 additions
and
98 deletions.
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
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
File renamed without changes.
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,23 @@ | ||
/- | ||
Copyright (c) 2018 Kenny Lau. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Kenny Lau | ||
-/ | ||
import algebra.field.basic | ||
import algebra.opposites | ||
|
||
/-! | ||
# Field structure on the multiplicative opposite | ||
-/ | ||
|
||
variables (α : Type*) | ||
|
||
namespace mul_opposite | ||
|
||
instance [division_ring α] : division_ring αᵐᵒᵖ := | ||
{ .. mul_opposite.group_with_zero α, .. mul_opposite.ring α } | ||
|
||
instance [field α] : field αᵐᵒᵖ := | ||
{ .. mul_opposite.division_ring α, .. mul_opposite.comm_ring α } | ||
|
||
end mul_opposite |
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
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
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
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
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,114 @@ | ||
/- | ||
Copyright (c) 2020 Eric Wieser. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Eric Wieser | ||
-/ | ||
import algebra.opposites | ||
import group_theory.group_action.defs | ||
|
||
/-! | ||
# Scalar actions on and by `Mᵐᵒᵖ` | ||
This file defines the actions on the opposite type `has_scalar R Mᵐᵒᵖ`, and actions by the opposite | ||
type, `has_scalar Rᵐᵒᵖ M`. | ||
Note that `mul_opposite.has_scalar` is provided in an earlier file as it is needed to provide the | ||
`add_monoid.nsmul` and `add_comm_group.gsmul` fields. | ||
-/ | ||
|
||
variables (α : Type*) | ||
|
||
/-! ### Actions _on_ the opposite type | ||
Actions on the opposite type just act on the underlying type. | ||
-/ | ||
|
||
namespace mul_opposite | ||
|
||
instance (R : Type*) [monoid R] [mul_action R α] : mul_action R αᵐᵒᵖ := | ||
{ one_smul := λ x, unop_injective $ one_smul R (unop x), | ||
mul_smul := λ r₁ r₂ x, unop_injective $ mul_smul r₁ r₂ (unop x), | ||
.. mul_opposite.has_scalar α R } | ||
|
||
instance (R : Type*) [monoid R] [add_monoid α] [distrib_mul_action R α] : | ||
distrib_mul_action R αᵐᵒᵖ := | ||
{ smul_add := λ r x₁ x₂, unop_injective $ smul_add r (unop x₁) (unop x₂), | ||
smul_zero := λ r, unop_injective $ smul_zero r, | ||
.. mul_opposite.mul_action α R } | ||
|
||
instance (R : Type*) [monoid R] [monoid α] [mul_distrib_mul_action R α] : | ||
mul_distrib_mul_action R αᵐᵒᵖ := | ||
{ smul_mul := λ r x₁ x₂, unop_injective $ smul_mul' r (unop x₂) (unop x₁), | ||
smul_one := λ r, unop_injective $ smul_one r, | ||
.. mul_opposite.mul_action α R } | ||
|
||
instance {M N} [has_scalar M N] [has_scalar M α] [has_scalar N α] [is_scalar_tower M N α] : | ||
is_scalar_tower M N αᵐᵒᵖ := | ||
⟨λ x y z, unop_injective $ smul_assoc _ _ _⟩ | ||
|
||
instance {M N} [has_scalar M α] [has_scalar N α] [smul_comm_class M N α] : | ||
smul_comm_class M N αᵐᵒᵖ := | ||
⟨λ x y z, unop_injective $ smul_comm _ _ _⟩ | ||
|
||
end mul_opposite | ||
|
||
/-! ### Actions _by_ the opposite type (right actions) | ||
In `has_mul.to_has_scalar` in another file, we define the left action `a₁ • a₂ = a₁ * a₂`. For the | ||
multiplicative opposite, we define `mul_opposite.op a₁ • a₂ = a₂ * a₁`, with the multiplication | ||
reversed. | ||
-/ | ||
|
||
open mul_opposite | ||
|
||
/-- Like `has_mul.to_has_scalar`, but multiplies on the right. | ||
See also `monoid.to_opposite_mul_action` and `monoid_with_zero.to_opposite_mul_action_with_zero`. -/ | ||
instance has_mul.to_has_opposite_scalar [has_mul α] : has_scalar αᵐᵒᵖ α := | ||
{ smul := λ c x, x * c.unop } | ||
|
||
@[simp] lemma op_smul_eq_mul [has_mul α] {a a' : α} : op a • a' = a' * a := rfl | ||
|
||
-- TODO: add an additive version once we have additive opposites | ||
/-- The right regular action of a group on itself is transitive. -/ | ||
instance mul_action.opposite_regular.is_pretransitive {G : Type*} [group G] : | ||
mul_action.is_pretransitive Gᵐᵒᵖ G := | ||
⟨λ x y, ⟨op (x⁻¹ * y), mul_inv_cancel_left _ _⟩⟩ | ||
|
||
instance semigroup.opposite_smul_comm_class [semigroup α] : | ||
smul_comm_class αᵐᵒᵖ α α := | ||
{ smul_comm := λ x y z, (mul_assoc _ _ _) } | ||
|
||
instance semigroup.opposite_smul_comm_class' [semigroup α] : | ||
smul_comm_class α αᵐᵒᵖ α := | ||
{ smul_comm := λ x y z, (mul_assoc _ _ _).symm } | ||
|
||
/-- Like `monoid.to_mul_action`, but multiplies on the right. -/ | ||
instance monoid.to_opposite_mul_action [monoid α] : mul_action αᵐᵒᵖ α := | ||
{ smul := (•), | ||
one_smul := mul_one, | ||
mul_smul := λ x y r, (mul_assoc _ _ _).symm } | ||
|
||
instance is_scalar_tower.opposite_mid {M N} [monoid N] [has_scalar M N] | ||
[smul_comm_class M N N] : | ||
is_scalar_tower M Nᵐᵒᵖ N := | ||
⟨λ x y z, mul_smul_comm _ _ _⟩ | ||
|
||
instance smul_comm_class.opposite_mid {M N} [monoid N] [has_scalar M N] | ||
[is_scalar_tower M N N] : | ||
smul_comm_class M Nᵐᵒᵖ N := | ||
⟨λ x y z, by { induction y using mul_opposite.rec, simp [smul_mul_assoc] }⟩ | ||
|
||
-- The above instance does not create an unwanted diamond, the two paths to | ||
-- `mul_action αᵐᵒᵖ αᵐᵒᵖ` are defeq. | ||
example [monoid α] : monoid.to_mul_action αᵐᵒᵖ = mul_opposite.mul_action α αᵐᵒᵖ := rfl | ||
|
||
/-- `monoid.to_opposite_mul_action` is faithful on cancellative monoids. -/ | ||
instance left_cancel_monoid.to_has_faithful_opposite_scalar [left_cancel_monoid α] : | ||
has_faithful_scalar αᵐᵒᵖ α := | ||
⟨λ x y h, unop_injective $ mul_left_cancel (h 1)⟩ | ||
|
||
/-- `monoid.to_opposite_mul_action` is faithful on nontrivial cancellative monoids with zero. -/ | ||
instance cancel_monoid_with_zero.to_has_faithful_opposite_scalar | ||
[cancel_monoid_with_zero α] [nontrivial α] : has_faithful_scalar αᵐᵒᵖ α := | ||
⟨λ x y h, unop_injective $ mul_left_cancel₀ one_ne_zero (h 1)⟩ |
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
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