Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group #12799

Open
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

jstoobysmith
Copy link
Collaborator

Add properties of the special unitary group, mirroring the properties of found in Algebra/Star/Unitary.lean. In particular, I add an instance of specialUnitaryGroup as a Group, Star, InvolutiveStar, and StarMul.


Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label May 10, 2024
@jstoobysmith jstoobysmith added awaiting-review t-algebra Algebra (groups, rings, fields, etc) labels May 10, 2024
Copy link
Collaborator

@chrisflav chrisflav left a comment

Choose a reason for hiding this comment

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

I left some comments.

Comment on lines +244 to +249
theorem star_mem_iff {U : Matrix n n α} :
star U ∈ specialUnitaryGroup n α ↔ U ∈ specialUnitaryGroup n α :=
⟨fun h => star_star U ▸ star_mem h, star_mem⟩

instance : Star (specialUnitaryGroup n α) :=
⟨fun U => ⟨star U, star_mem U.prop⟩⟩
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
theorem star_mem_iff {U : Matrix n n α} :
star U ∈ specialUnitaryGroup n α ↔ U ∈ specialUnitaryGroup n α :=
⟨fun h => star_star U ▸ star_mem h, star_mem⟩
instance : Star (specialUnitaryGroup n α) :=
⟨fun U => ⟨star U, star_mem U.prop⟩⟩
theorem star_mem_iff {U : Matrix n n α} :
star U ∈ specialUnitaryGroup n α ↔ U ∈ specialUnitaryGroup n α :=
⟨fun h star_star U ▸ star_mem h, star_mem⟩
instance : Star (specialUnitaryGroup n α) :=
⟨fun U ⟨star U, star_mem U.prop⟩⟩

I think this is the preferred style.

Comment on lines +269 to +272
instance : Group (specialUnitaryGroup n α) :=
{ Submonoid.toMonoid _ with
inv := star
mul_left_inv := star_mul_self }
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
instance : Group (specialUnitaryGroup n α) :=
{ Submonoid.toMonoid _ with
inv := star
mul_left_inv := star_mul_self }
instance : Group (specialUnitaryGroup n α) where
inv := star
mul_left_inv := star_mul_self

Comment on lines +274 to +278
instance : InvolutiveStar (specialUnitaryGroup n α) :=
⟨by
intro x
ext
rw [coe_star, coe_star, star_star]⟩
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
instance : InvolutiveStar (specialUnitaryGroup n α) :=
by
intro x
ext
rw [coe_star, coe_star, star_star]⟩
instance : InvolutiveStar (specialUnitaryGroup n α) :=
star_involutive x := by
ext
rw [coe_star, coe_star, star_star]

Comment on lines +280 to +284
instance : StarMul (specialUnitaryGroup n α) :=
⟨by
intro x y
ext
rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]⟩
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
instance : StarMul (specialUnitaryGroup n α) :=
by
intro x y
ext
rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]⟩
instance : StarMul (specialUnitaryGroup n α) :=
star_mul x y := by
ext
rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]

Comment on lines +261 to +268
@[simp]
theorem star_mul_self (U : specialUnitaryGroup n α) : star U * U = 1 :=
Subtype.ext <| coe_star_mul_self U

@[simp]
theorem mul_star_self (U : specialUnitaryGroup n α) : U * star U = 1 :=
Subtype.ext <| coe_mul_star_self U

Copy link
Collaborator

Choose a reason for hiding this comment

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

Currently

example (U : specialUnitaryGroup n α) : U * star U = 1 := by
  simp

right after these lemmas fails because simp is running out of heartbeats. Changing abbrev specialUnitaryGroup to def specialUnitaryGroup fixes this. Maybe the other abbrevs in this file should also be defs?

Comment on lines +288 to +294

theorem star_eq_inv (U : specialUnitaryGroup n α) : star U = U⁻¹ :=
rfl

theorem star_eq_inv' : (star : specialUnitaryGroup n α → specialUnitaryGroup n α) = Inv.inv :=
rfl

Copy link
Collaborator

Choose a reason for hiding this comment

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

Currently this

example (U : unitaryGroup n α) : U⁻¹ = (star U : Matrix n n α) := by
  simp

works, but

example (U : specialUnitaryGroup n α) : U⁻¹ = (star U : Matrix n n α) := by
  simp

does not. I am not sure what the correct behavior should be, but it should probably be consistent.

@chrisflav chrisflav added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels May 19, 2024
@jcommelin
Copy link
Member

This PR looks mostly fine, but there are still some places where it needs some work. Are you planning to continue working on this PR? Would you like some help from others, or do you want to hand it over completely? (In the latter case, please label it with please-adopt.)

@jstoobysmith jstoobysmith added the please-adopt Inactive PR (would be valuable to adopt) label Oct 30, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-author A reviewer has asked the author a question or requested changes new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! please-adopt Inactive PR (would be valuable to adopt) t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants