[Merged by Bors] - feat(analysis/convex/cone/basic): add has_add, add_zero_class, and add_comm_semigroup instances to convex_cone

[apurvnakade]

Adds has_add, add_zero_class, and add_comm_semigroup instance to convex_cones.

---

• depends on: [Merged by Bors] - feat(analysis/convex/cone): add inner_dual_cone_of_inner_dual_cone_eq_self for nonempty, closed, convex cones #15637 for the has_zero instance

#15637 also adds a few other theorems not relevant for this PR.

[mcdoll]

I would guess that your addition and the zero element are compatible in the sense of add_zero_class and that the addition is associative add_semigroup

I haven't tested it, but I would hope that you can use set_like.coe_injective and function.injective.add_semigroup and set.add_semigroup for that.

[apurvnakade]

I would guess that your addition and the zero element are compatible in the sense of add_zero_class and that the addition is associative add_semigroup

I haven't tested it, but I would hope that you can use set_like.coe_injective and function.injective.add_semigroup and set.add_semigroup for that.

Great, thanks! I'll upgrade the classes.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(analysis/convex/cone): add inner_dual_cone_of_inner_dual_cone_eq_self for nonempty, closed, convex cones #15637
  By Dependent Issues (🤖). Happy coding!

[apurvnakade]

I removed @[simp] lemma coe_add {K₁ K₂ : convex_cone 𝕜 E} : ((K₁ + K₂) : set E) = ↑K₁ + ↑K₂ := rfl because of the following linter error:

/- The syn_taut linter reports: -/
/- THE FOLLOWING DECLARATIONS ARE SYNTACTIC TAUTOLOGIES. This usually means that they are of the form ∀ a b ... z, e₁ = e₂ where e₁ and e₂ are identical expressions. We call declarations of this form syntactic tautologies. Such lemmas are (mostly) useless and sometimes introduced unintentionally when proving basic facts using rfl, when elaboration results in a different term than the user intended. You should check that the declaration really says what you think it does. -/
-- analysis/convex/cone.lean
#check @convex_cone.coe_add /- LHS equals RHS syntactically -/
Error: convex_cone.coe_add - LHS equals RHS syntactically

[mcdoll]

Sorry for the delay. Looks good to me, even though I am slightly sad that K1 + K2 did not work.

[apurvnakade]

Sorry for not the delay. Looks good to me, even though I am slightly sad that K1 + K2 did not work.

No worries! I have also been super busy with teaching so this delay kinda worked out for me.
I'm a bit surprised by the set.has_add issue as well. But I think the API for set.has_add isn't that powerful so not much is lost by not using it.

[mcdoll]

Thanks 🐙

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by mcdoll.

[hrmacbeth]

Thanks!

On the proposed lemma

@[simp] lemma coe_add {K₁ K₂ : convex_cone 𝕜 E} : ((K₁ + K₂) : set E) = ↑K₁ + ↑K₂ := rfl

I might guess the way to have Lean interpret it in a non-tautological way is (↑(K₁ + K₂) : set E) = ↑K₁ + ↑K₂; worth a try later since I agree this is a useful connection.

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[apurvnakade]

Thanks!

On the proposed lemma

@[simp] lemma coe_add {K₁ K₂ : convex_cone 𝕜 E} : ((K₁ + K₂) : set E) = ↑K₁ + ↑K₂ := rfl

I might guess the way to have Lean interpret it in a non-tautological way is (↑(K₁ + K₂) : set E) = ↑K₁ + ↑K₂; worth a try later since I agree this is a useful connection.

bors r+

I'll try this out and if it works make a small PR. Thank you,

[apurvnakade]

Nope, still the same linter error :(