Skip to content

Commit 11c83ea

Browse files
leanprover-community-mathlib4-botleanprover-community-mathlib4-bot
committed
Merge master into nightly-testing
2 parents 16e0f54 + a02b532 commit 11c83ea

File tree

10 files changed

+81
-70
lines changed

10 files changed

+81
-70
lines changed

‎Mathlib.lean

+1
Original file line numberDiff line numberDiff line change
@@ -355,6 +355,7 @@ import Mathlib.Algebra.Group.Submonoid.Defs
355355
import Mathlib.Algebra.Group.Submonoid.DistribMulAction
356356
import Mathlib.Algebra.Group.Submonoid.Finsupp
357357
import Mathlib.Algebra.Group.Submonoid.Membership
358+
import Mathlib.Algebra.Group.Submonoid.MulAction
358359
import Mathlib.Algebra.Group.Submonoid.MulOpposite
359360
import Mathlib.Algebra.Group.Submonoid.Operations
360361
import Mathlib.Algebra.Group.Submonoid.Pointwise

‎Mathlib/Algebra/Group/Submonoid/MulAction.lean

+69
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
/-
2+
Copyright (c) 2021 Eric Wieser. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Eric Wieser
5+
-/
6+
import Mathlib.Algebra.Group.Submonoid.Defs
7+
import Mathlib.Algebra.Group.Action.Defs
8+
9+
/-!
10+
# Actions by `Submonoid`s
11+
12+
These instances transfer the action by an element `m : M` of a monoid `M` written as `m • a` onto
13+
the action by an element `s : S` of a submonoid `S : Submonoid M` such that `s • a = (s : M) • a`.
14+
15+
These instances work particularly well in conjunction with `Monoid.toMulAction`, enabling
16+
`s • m` as an alias for `↑s * m`.
17+
-/
18+
19+
namespace Submonoid
20+
21+
variable {M' : Type*} {α β : Type*}
22+
23+
section MulOneClass
24+
25+
variable [MulOneClass M']
26+
27+
@[to_additive]
28+
instance smul [SMul M' α] (S : Submonoid M') : SMul S α :=
29+
SMul.comp _ S.subtype
30+
31+
@[to_additive]
32+
instance smulCommClass_left [SMul M' β] [SMul α β] [SMulCommClass M' α β]
33+
(S : Submonoid M') : SMulCommClass S α β :=
34+
⟨fun a _ _ => smul_comm (a : M') _ _⟩
35+
36+
@[to_additive]
37+
instance smulCommClass_right [SMul α β] [SMul M' β] [SMulCommClass α M' β]
38+
(S : Submonoid M') : SMulCommClass α S β :=
39+
⟨fun a s => smul_comm a (s : M')⟩
40+
41+
/-- Note that this provides `IsScalarTower S M' M'` which is needed by `SMulMulAssoc`. -/
42+
instance isScalarTower [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β]
43+
(S : Submonoid M') :
44+
IsScalarTower S α β :=
45+
⟨fun a => smul_assoc (a : M')⟩
46+
47+
section SMul
48+
variable [SMul M' α] {S : Submonoid M'}
49+
50+
@[to_additive] lemma smul_def (g : S) (a : α) : g • a = (g : M') • a := rfl
51+
52+
@[to_additive (attr := simp)]
53+
lemma mk_smul (g : M') (hg : g ∈ S) (a : α) : (⟨g, hg⟩ : S) • a = g • a := rfl
54+
55+
end SMul
56+
end MulOneClass
57+
58+
variable [Monoid M']
59+
60+
/-- The action by a submonoid is the action by the underlying monoid. -/
61+
@[to_additive
62+
"The additive action by an `AddSubmonoid` is the action by the underlying `AddMonoid`. "]
63+
instance mulAction [MulAction M' α] (S : Submonoid M') : MulAction S α where
64+
one_smul := one_smul M'
65+
mul_smul m₁ m₂ := mul_smul (m₁ : M') m₂
66+
67+
example {S : Submonoid M'} : IsScalarTower S M' M' := by infer_instance
68+
69+
end Submonoid

‎Mathlib/Algebra/Group/Submonoid/Operations.lean

+3-67
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ import Mathlib.Algebra.Group.Action.Faithful
88
import Mathlib.Algebra.Group.Nat.Defs
99
import Mathlib.Algebra.Group.Prod
1010
import Mathlib.Algebra.Group.Submonoid.Basic
11+
import Mathlib.Algebra.Group.Submonoid.MulAction
1112
import Mathlib.Algebra.Group.TypeTags.Basic
1213

1314
/-!
@@ -973,75 +974,10 @@ theorem Submonoid.equivMapOfInjective_coe_mulEquiv (e : M ≃* N) :
973974
ext
974975
rfl
975976

976-
section Actions
977-
978-
/-! ### Actions by `Submonoid`s
979-
980-
These instances transfer the action by an element `m : M` of a monoid `M` written as `m • a` onto
981-
the action by an element `s : S` of a submonoid `S : Submonoid M` such that `s • a = (s : M) • a`.
982-
983-
These instances work particularly well in conjunction with `Monoid.toMulAction`, enabling
984-
`s • m` as an alias for `↑s * m`.
985-
-/
986-
987-
988-
namespace Submonoid
989-
990-
variable {M' : Type*} {α β : Type*}
991-
992-
section MulOneClass
993-
994-
variable [MulOneClass M']
995-
996-
@[to_additive]
997-
instance smul [SMul M' α] (S : Submonoid M') : SMul S α :=
998-
SMul.comp _ S.subtype
999-
1000-
@[to_additive]
1001-
instance smulCommClass_left [SMul M' β] [SMul α β] [SMulCommClass M' α β]
1002-
(S : Submonoid M') : SMulCommClass S α β :=
1003-
⟨fun a _ _ => smul_comm (a : M') _ _⟩
1004-
1005-
@[to_additive]
1006-
instance smulCommClass_right [SMul α β] [SMul M' β] [SMulCommClass α M' β]
1007-
(S : Submonoid M') : SMulCommClass α S β :=
1008-
⟨fun a s => smul_comm a (s : M')⟩
1009-
1010-
/-- Note that this provides `IsScalarTower S M' M'` which is needed by `SMulMulAssoc`. -/
1011-
instance isScalarTower [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β]
1012-
(S : Submonoid M') :
1013-
IsScalarTower S α β :=
1014-
⟨fun a => smul_assoc (a : M')⟩
1015-
1016-
section SMul
1017-
variable [SMul M' α] {S : Submonoid M'}
1018-
1019-
@[to_additive] lemma smul_def (g : S) (a : α) : g • a = (g : M') • a := rfl
1020-
1021-
@[to_additive (attr := simp)]
1022-
lemma mk_smul (g : M') (hg : g ∈ S) (a : α) : (⟨g, hg⟩ : S) • a = g • a := rfl
1023-
1024-
instance faithfulSMul [FaithfulSMul M' α] : FaithfulSMul S α :=
977+
instance Submonoid.faithfulSMul {M' α : Type*} [MulOneClass M'] [SMul M' α] {S : Submonoid M'}
978+
[FaithfulSMul M' α] : FaithfulSMul S α :=
1025979
⟨fun h => Subtype.ext <| eq_of_smul_eq_smul h⟩
1026980

1027-
end SMul
1028-
end MulOneClass
1029-
1030-
variable [Monoid M']
1031-
1032-
/-- The action by a submonoid is the action by the underlying monoid. -/
1033-
@[to_additive
1034-
"The additive action by an `AddSubmonoid` is the action by the underlying `AddMonoid`. "]
1035-
instance mulAction [MulAction M' α] (S : Submonoid M') : MulAction S α :=
1036-
MulAction.compHom _ S.subtype
1037-
1038-
example {S : Submonoid M'} : IsScalarTower S M' M' := by infer_instance
1039-
1040-
1041-
end Submonoid
1042-
1043-
end Actions
1044-
1045981
section Units
1046982

1047983
namespace Submonoid

‎Mathlib/Algebra/Module/Submodule/Defs.lean

+1
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
55
-/
66
import Mathlib.Algebra.Group.Subgroup.Defs
77
import Mathlib.GroupTheory.GroupAction.SubMulAction
8+
import Mathlib.Algebra.Group.Submonoid.Basic
89

910
/-!
1011

‎Mathlib/Algebra/Polynomial/Basic.lean

+1
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ import Mathlib.Algebra.MonoidAlgebra.Defs
88
import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
99
import Mathlib.Data.Finset.Sort
1010
import Mathlib.Tactic.FastInstance
11+
import Mathlib.Algebra.Group.Submonoid.Operations
1112

1213
/-!
1314
# Theory of univariate polynomials

‎Mathlib/GroupTheory/GroupAction/Defs.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ Authors: Chris Hughes
55
-/
66
import Mathlib.Algebra.Group.Pointwise.Set.Basic
77
import Mathlib.Algebra.Group.Subgroup.Defs
8-
import Mathlib.Algebra.Group.Submonoid.Operations
98
import Mathlib.Algebra.GroupWithZero.Action.Defs
9+
import Mathlib.Algebra.Group.Submonoid.MulAction
1010

1111
/-!
1212
# Definition of `orbit`, `fixedPoints` and `stabilizer`

‎Mathlib/GroupTheory/MonoidLocalization/Basic.lean

+1
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Amelia Livingston
66
import Mathlib.Algebra.Group.Submonoid.Defs
77
import Mathlib.GroupTheory.Congruence.Hom
88
import Mathlib.GroupTheory.OreLocalization.Basic
9+
import Mathlib.Algebra.Group.Submonoid.Operations
910

1011
/-!
1112
# Localizations of commutative monoids

‎Mathlib/GroupTheory/OreLocalization/Basic.lean

+2-1
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@ Copyright (c) 2022 Jakob von Raumer. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jakob von Raumer, Kevin Klinge, Andrew Yang
55
-/
6-
import Mathlib.Algebra.Group.Submonoid.Operations
76
import Mathlib.GroupTheory.OreLocalization.OreSet
87
import Mathlib.Tactic.Common
8+
import Mathlib.Algebra.Group.Submonoid.MulAction
9+
import Mathlib.Algebra.Group.Units.Defs
910

1011
/-!
1112

‎Mathlib/Order/Antisymmetrization.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ def AntisymmRel (a b : α) : Prop :=
4040
r a b ∧ r b a
4141

4242
theorem antisymmRel_swap : AntisymmRel (swap r) = AntisymmRel r :=
43-
funext fun _ => funext fun _ => propext and_comm
43+
funext₂ fun _ _ ↦ propext and_comm
4444

4545
@[refl]
4646
theorem antisymmRel_refl [IsRefl α r] (a : α) : AntisymmRel r a a :=

‎Mathlib/Topology/Algebra/Monoid.lean

+1
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ import Mathlib.Topology.Algebra.MulAction
99
import Mathlib.Algebra.BigOperators.Pi
1010
import Mathlib.Algebra.Group.ULift
1111
import Mathlib.Topology.ContinuousMap.Defs
12+
import Mathlib.Algebra.Group.Submonoid.Basic
1213

1314
/-!
1415
# Theory of topological monoids

0 commit comments

Comments
 (0)