Skip to content

Commit 1e659b6

Browse files
feat: HahnModule action by HahnSeries (#10164)
Given a `SMul R V` instance, we introduce `HahnModule Γ R V` as an alias for HahnSeries Γ V, and produce a `SMul (HahnSeries Γ R) (HahnModule Γ R V)` instance. We use the `SMul` instance to shorten the `Mul` instance. We will work our way up to `Module (HahnSeries Γ R) (HahnModule Γ R V)` in a later PR. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
1 parent c783238 commit 1e659b6

File tree

1 file changed

+107
-18
lines changed

1 file changed

+107
-18
lines changed

Mathlib/RingTheory/HahnSeries.lean

Lines changed: 107 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -588,10 +588,14 @@ end Domain
588588

589589
end Module
590590

591+
end HahnSeries
592+
591593
section Multiplication
592594

593595
variable [OrderedCancelAddCommMonoid Γ]
594596

597+
namespace HahnSeries
598+
595599
instance [Zero R] [One R] : One (HahnSeries Γ R) :=
596600
⟨single 0 1
597601

@@ -618,22 +622,111 @@ theorem order_one [MulZeroOneClass R] : order (1 : HahnSeries Γ R) = 0 := by
618622
· exact order_single one_ne_zero
619623
#align hahn_series.order_one HahnSeries.order_one
620624

621-
instance [NonUnitalNonAssocSemiring R] : Mul (HahnSeries Γ R) where
622-
mul x y :=
623-
{ coeff := fun a =>
624-
∑ ij in addAntidiagonal x.isPWO_support y.isPWO_support a, x.coeff ij.fst * y.coeff ij.snd
625-
isPWO_support' :=
625+
end HahnSeries
626+
627+
/-- We introduce a type alias for `HahnSeries` in order to work with scalar multiplication by
628+
series. If we wrote a `SMul (HahnSeries Γ R) (HahnSeries Γ V)` instance, then when
629+
`V = HahnSeries Γ R`, we would have two different actions of `HahnSeries Γ R` on `HahnSeries Γ V`.
630+
See `Mathlib.Data.Polynomial.Module` for more discussion on this problem. -/
631+
@[nolint unusedArguments]
632+
def HahnModule (Γ R V : Type*) [PartialOrder Γ] [Zero V] [SMul R V] :=
633+
HahnSeries Γ V
634+
635+
namespace HahnModule
636+
637+
/-- The casting function to the type synonym. -/
638+
def of {Γ : Type*} (R : Type*) {V : Type*} [PartialOrder Γ] [Zero V] [SMul R V] :
639+
HahnSeries Γ V ≃ HahnModule Γ R V := Equiv.refl _
640+
641+
/-- Recursion principle to reduce a result about the synonym to the original type. -/
642+
@[elab_as_elim]
643+
def rec {Γ R V : Type*} [PartialOrder Γ] [Zero V] [SMul R V] {motive : HahnModule Γ R V → Sort*}
644+
(h : ∀ x : HahnSeries Γ V, motive (of R x)) : ∀ x, motive x :=
645+
fun x => h <| (of R).symm x
646+
647+
@[ext]
648+
theorem ext {Γ R V : Type*} [PartialOrder Γ] [Zero V] [SMul R V]
649+
(x y : HahnModule Γ R V) (h : ((of R).symm x).coeff = ((of R).symm y).coeff) : x = y :=
650+
(of R).symm.injective <| HahnSeries.coeff_inj.1 h
651+
652+
variable {V : Type*} [AddCommMonoid V] [SMul R V]
653+
654+
instance instAddCommMonoid : AddCommMonoid (HahnModule Γ R V) :=
655+
inferInstanceAs <| AddCommMonoid (HahnSeries Γ V)
656+
657+
@[simp] theorem of_zero : of R (0 : HahnSeries Γ V) = 0 := rfl
658+
@[simp] theorem of_add (x y : HahnSeries Γ V) : of R (x + y) = of R x + of R y := rfl
659+
660+
@[simp] theorem of_symm_zero : (of R).symm (0 : HahnModule Γ R V) = 0 := rfl
661+
@[simp] theorem of_symm_add (x y : HahnModule Γ R V) :
662+
(of R).symm (x + y) = (of R).symm x + (of R).symm y := rfl
663+
664+
instance instSMul [Zero R] : SMul (HahnSeries Γ R) (HahnModule Γ R V) where
665+
smul x y := {
666+
coeff := fun a =>
667+
∑ ij in addAntidiagonal x.isPWO_support y.isPWO_support a,
668+
x.coeff ij.fst • ((of R).symm y).coeff ij.snd
669+
isPWO_support' :=
626670
haveI h :
627671
{ a : Γ |
628672
(∑ ij : Γ × Γ in addAntidiagonal x.isPWO_support y.isPWO_support a,
629-
x.coeff ij.fst * y.coeff ij.snd) ≠
673+
x.coeff ij.fst y.coeff ij.snd) ≠
630674
0 } ⊆
631675
{ a : Γ | (addAntidiagonal x.isPWO_support y.isPWO_support a).Nonempty } := by
632676
intro a ha
633677
contrapose! ha
634678
simp [not_nonempty_iff_eq_empty.1 ha]
635679
isPWO_support_addAntidiagonal.mono h }
636680

681+
theorem smul_coeff [Zero R] (x : HahnSeries Γ R) (y : HahnModule Γ R V) (a : Γ) :
682+
((of R).symm <| x • y).coeff a =
683+
∑ ij in addAntidiagonal x.isPWO_support y.isPWO_support a,
684+
x.coeff ij.fst • ((of R).symm y).coeff ij.snd :=
685+
rfl
686+
687+
variable {W : Type*} [Zero R] [AddCommMonoid W]
688+
689+
instance instSMulZeroClass [SMulZeroClass R W] :
690+
SMulZeroClass (HahnSeries Γ R) (HahnModule Γ R W) where
691+
smul_zero x := by
692+
ext
693+
simp [smul_coeff]
694+
695+
theorem smul_coeff_right [SMulZeroClass R W] {x : HahnSeries Γ R}
696+
{y : HahnModule Γ R W} {a : Γ} {s : Set Γ} (hs : s.IsPWO) (hys : ((of R).symm y).support ⊆ s) :
697+
((of R).symm <| x • y).coeff a =
698+
∑ ij in addAntidiagonal x.isPWO_support hs a,
699+
x.coeff ij.fst • ((of R).symm y).coeff ij.snd := by
700+
rw [smul_coeff]
701+
apply sum_subset_zero_on_sdiff (addAntidiagonal_mono_right hys) _ fun _ _ => rfl
702+
intro b hb
703+
simp only [not_and, mem_sdiff, mem_addAntidiagonal, HahnSeries.mem_support, not_imp_not] at hb
704+
rw [hb.2 hb.1.1 hb.1.2.2, smul_zero]
705+
706+
theorem smul_coeff_left [SMulWithZero R W] {x : HahnSeries Γ R}
707+
{y : HahnModule Γ R W} {a : Γ} {s : Set Γ}
708+
(hs : s.IsPWO) (hxs : x.support ⊆ s) :
709+
((of R).symm <| x • y).coeff a =
710+
∑ ij in addAntidiagonal hs y.isPWO_support a,
711+
x.coeff ij.fst • ((of R).symm y).coeff ij.snd := by
712+
rw [smul_coeff]
713+
apply sum_subset_zero_on_sdiff (addAntidiagonal_mono_left hxs) _ fun _ _ => rfl
714+
intro b hb
715+
simp only [not_and', mem_sdiff, mem_addAntidiagonal, HahnSeries.mem_support, not_ne_iff] at hb
716+
rw [hb.2 ⟨hb.1.2.1, hb.1.2.2⟩, zero_smul]
717+
718+
end HahnModule
719+
720+
namespace HahnSeries
721+
722+
instance [NonUnitalNonAssocSemiring R] : Mul (HahnSeries Γ R) where
723+
mul x y := (HahnModule.of R).symm (x • HahnModule.of R y)
724+
725+
726+
theorem of_symm_smul_of_eq_mul [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} :
727+
(HahnModule.of R).symm (x • HahnModule.of R y) = x * y := rfl
728+
729+
637730
/-@[simp] Porting note: removing simp. RHS is more complicated and it makes linter
638731
failures elsewhere-/
639732
theorem mul_coeff [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a : Γ} :
@@ -645,23 +738,15 @@ theorem mul_coeff [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a : Γ}
645738
theorem mul_coeff_right' [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a : Γ} {s : Set Γ}
646739
(hs : s.IsPWO) (hys : y.support ⊆ s) :
647740
(x * y).coeff a =
648-
∑ ij in addAntidiagonal x.isPWO_support hs a, x.coeff ij.fst * y.coeff ij.snd := by
649-
rw [mul_coeff]
650-
apply sum_subset_zero_on_sdiff (addAntidiagonal_mono_right hys) _ fun _ _ => rfl
651-
intro b hb
652-
simp only [not_and, mem_sdiff, mem_addAntidiagonal, mem_support, not_imp_not] at hb
653-
rw [hb.2 hb.1.1 hb.1.2.2, mul_zero]
741+
∑ ij in addAntidiagonal x.isPWO_support hs a, x.coeff ij.fst * y.coeff ij.snd :=
742+
HahnModule.smul_coeff_right hs hys
654743
#align hahn_series.mul_coeff_right' HahnSeries.mul_coeff_right'
655744

656745
theorem mul_coeff_left' [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a : Γ} {s : Set Γ}
657746
(hs : s.IsPWO) (hxs : x.support ⊆ s) :
658747
(x * y).coeff a =
659-
∑ ij in addAntidiagonal hs y.isPWO_support a, x.coeff ij.fst * y.coeff ij.snd := by
660-
rw [mul_coeff]
661-
apply sum_subset_zero_on_sdiff (addAntidiagonal_mono_left hxs) _ fun _ _ => rfl
662-
intro b hb
663-
simp only [not_and', mem_sdiff, mem_addAntidiagonal, mem_support, not_ne_iff] at hb
664-
rw [hb.2 ⟨hb.1.2.1, hb.1.2.2⟩, zero_mul]
748+
∑ ij in addAntidiagonal hs y.isPWO_support a, x.coeff ij.fst * y.coeff ij.snd :=
749+
HahnModule.smul_coeff_left hs hxs
665750
#align hahn_series.mul_coeff_left' HahnSeries.mul_coeff_left'
666751

667752
instance [NonUnitalNonAssocSemiring R] : Distrib (HahnSeries Γ R) :=
@@ -1081,8 +1166,12 @@ end Domain
10811166

10821167
end Algebra
10831168

1169+
end HahnSeries
1170+
10841171
end Multiplication
10851172

1173+
namespace HahnSeries
1174+
10861175
section Semiring
10871176

10881177
variable [Semiring R]

0 commit comments

Comments
 (0)