Notation for HomogeneousIdeal.irrelevant

Stream: mathlib4

[Kenny Lau]

Should we use ₊ for docs#HomogeneousIdeal.irrelevant ? We could also make it scoped. The current uses for this character are:

import Mathlib

#find_syntax "₊"
/-
Found 4 uses among 2396 syntax declarations
In `Mathlib.Algebra.Order.Floor.Defs`:
  Nat.«term⌈_⌉₊»: '⌈ _ ⌉₊'
  Nat.«term⌊_⌋₊»: '⌊ _ ⌋₊'

In `Mathlib.Analysis.Normed.Group.Basic`:
  «term‖_‖₊»: '‖ _ ‖₊'

In `Mathlib.CategoryTheory.Bicategory.Kan.HasKan`:
  CategoryTheory.Bicategory.«term_₊_»: '₊'
-/

[Christian Merten]

Why do we need notation for this?

[Kenny Lau]

it's more convenient

[Kenny Lau]

and closer to maths

[Christian Merten]

But it is one more notation to learn.

[Kenny Lau]

I think anyone who knows the irrelevant ideal knows this notation, just like with Gal

[Kenny Lau]

@Christian Merten btw there's this extra condition that says 𝒜₂₊ ≤ HomogeneousIdeal.map f₁₂ 𝒜₁₊ that I need in order to define Proj.map, and I'm wondering whether I should bundle that or not. in my project it is not bundled (and I named it "admissible" because) but I think in the mathlib PR I will bundle it. I thought I would discuss this with you beforehand.

[Andrew Yang]

I don't think we should bundle it. Another thing we might want to consider about is whether we should define a partial map even if the "admissible" condition doesn't hold, like what stacks#01MY does.

[Kenny Lau]

they won't be defeq (because you're using a subtype) and then when it's admissible you'll still need a new definition

[Kenny Lau]

and in any case i think we can define the partial map in another PR

[Kenny Lau]

also a cons of unbundling is that sometimes rw fails (this is already a problem with IsOpenImmersion and IsIso i think?)

[Kenny Lau]

i think we'll need laxer rw lemmas and/or more congr lemmas

[Kenny Lau]

what should I call this condition 𝒜₂₊ ≤ 𝒜₁₊.map f₁₂ ?

[Kenny Lau]

and should I make a def for it?

[Kenny Lau]

or even make it a class predicate on GradedRingHom?

[Kenny Lau]

@Kevin Buzzard have you ever encountered a name for this Prop?

[Kevin Buzzard]

nope

[Aaron Liu]

Kenny Lau said:

what should I call this condition 𝒜₂₊ ≤ 𝒜₁₊.map f₁₂ ?

seems vaguely similar to docs#Set.SurjOn