Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - refactor(linear_algebra/pi): add linear_map.single to match add_monoid_hom.single #6315

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - refactor(linear_algebra/pi): add linear_map.single to match add_monoid_hom.single #6315

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c1581c0
refactor(linear_algebra/pi): add `linear_map.single` to match `add_mo…
eric-wieser Feb 19, 2021
547424d
fix
eric-wieser Feb 19, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 14 additions & 1 deletion src/linear_algebra/pi.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,10 @@ It contains theorems relating these to each other, as well as to `linear_map.ker
## Main definitions

- pi types in the codomain:
- `linear_map.proj`
- `linear_map.pi`
- `linear_map.single`
- pi types in the domain:
- `linear_map.proj`
- `linear_map.diag`

-/
Expand Down Expand Up @@ -70,6 +72,17 @@ begin
exact (mem_bot _).2 (funext $ assume i, h i)
end

/-- The `linear_map` version of `add_monoid_hom.single` and `pi.single`. -/
@[simps]
def single [decidable_eq ι] (i : ι) : φ i →ₗ[R] (Πi, φ i) :=
{ to_fun := pi.single i,
map_smul' := λ r x, begin
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since you simplify linear_map.single i x to pi.single i x, it makes sense to add a lemma pi.single_smul somewhere near the definition of pi.semimodule. BTW, function.update_eq_iff gives a slightly shorter proof.
Otherwise LGTM.
bors d+

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We don't have pi.single_add yet either, but I think we should - I'll leave adding all of those lemmas to a follow-up PR.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But I will have a go at golfing this proof.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I came up with

  map_smul' := λ r x, begin
    ext j,
    have := (function.apply_update (λ i, (•) r) 0 i x j).symm,
    simp only [pi.zero_apply, smul_zero] at this,
    exact this,
  end,

Do you have a better proof in mind?

ext i', by_cases h : i' = i,
{ subst h, simp only [pi.single_eq_same, pi.smul_apply], },
{ simp only [h, pi.single_eq_of_ne, ne.def, not_false_iff, pi.smul_apply, smul_zero], },
end,
.. add_monoid_hom.single φ i}

section
variables (R φ)

Expand Down
13 changes: 10 additions & 3 deletions src/linear_algebra/std_basis.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,10 +39,10 @@ variables (R : Type*) {ι : Type*} [semiring R] (φ : ι → Type*)
[Π i, add_comm_monoid (φ i)] [Π i, semimodule R (φ i)] [decidable_eq ι]

/-- The standard basis of the product of `φ`. -/
def std_basis (i : ι) : φ i →ₗ[R] (Πi, φ i) := pi (diag i)
def std_basis : Π (i : ι), φ i →ₗ[R] (Πi, φ i) := single

lemma std_basis_apply (i : ι) (b : φ i) : std_basis R φ i b = update 0 i b :=
by ext j; rw [std_basis, pi_apply, diag, update_apply]; refl
rfl

lemma coe_std_basis (i : ι) : ⇑(std_basis R φ i) = pi.single i :=
funext $ std_basis_apply R φ i
Expand All @@ -53,6 +53,13 @@ by rw [std_basis_apply, update_same]
lemma std_basis_ne (i j : ι) (h : j ≠ i) (b : φ i) : std_basis R φ i b j = 0 :=
by rw [std_basis_apply, update_noteq h]; refl

lemma std_basis_eq_pi_diag (i : ι) : std_basis R φ i = pi (diag i) :=
begin
ext x j,
convert (update_apply 0 x i j _).symm,
refl,
end

section ext

variables {R φ} {M : Type*} [fintype ι] [add_comm_monoid M] [semimodule R M]
Expand Down Expand Up @@ -84,7 +91,7 @@ ker_eq_bot_of_injective $ assume f g hfg,
by simpa only [std_basis_same]

lemma proj_comp_std_basis (i j : ι) : (proj i).comp (std_basis R φ j) = diag j i :=
by rw [std_basis, proj_pi]
by rw [std_basis_eq_pi_diag, proj_pi]

lemma proj_std_basis_same (i : ι) : (proj i).comp (std_basis R φ i) = id :=
by ext b; simp
Expand Down
4 changes: 2 additions & 2 deletions src/ring_theory/power_series/basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -121,11 +121,11 @@ by rw [coeff, monomial, linear_map.proj_apply, linear_map.std_basis_apply, funct

@[simp] lemma coeff_monomial_same (n : σ →₀ ℕ) (a : R) :
coeff R n (monomial R n a) = a :=
linear_map.std_basis_same _ _ _ _
linear_map.std_basis_same R _ n a

lemma coeff_monomial_ne {m n : σ →₀ ℕ} (h : m ≠ n) (a : R) :
coeff R m (monomial R n a) = 0 :=
linear_map.std_basis_ne _ _ _ _ h a
linear_map.std_basis_ne R _ _ _ h a

lemma eq_of_coeff_monomial_ne_zero {m n : σ →₀ ℕ} {a : R} (h : coeff R m (monomial R n a) ≠ 0) :
m = n :=
Expand Down