a "reflect" structure for when you don't want subtype

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

/-- Morally, `A ≃ Subtype (α := B) p` -/
class HasReflect (A B : Type*) (p : B → Prop) extends Coe A B where
  reflect (x : B) (h : p x) : A
  satisfy (x : A) : p x := by simp
  left_inv {x : A} : reflect x (satisfy x) = x := by simp
  coe_reflect {x : B} {h : p x} : reflect x h = x := by simp

attribute [simp] HasReflect.satisfy HasReflect.left_inv HasReflect.coe_reflect

def HasReflect.addCommGroup (A B p) [HasReflect A B p] [AddCommGroup B]
    (hzero : p 0) (hadd : ∀ {x y}, p x → p y → p (x + y)) : AddCommGroup A where
  add x y := reflect (x + y : B) (hadd (by simp) (by simp))
  zero := reflect (0 : B) hzero
  neg x := reflect (-x : B) (p := p) sorry
  nsmul := sorry
  zsmul := sorry
  add_assoc := sorry
  zero_add := sorry
  add_zero := sorry
  neg_add_cancel := sorry
  add_comm := sorry
  nsmul_zero := sorry
  nsmul_succ := sorry
  zsmul_zero' := sorry
  zsmul_succ' := sorry
  zsmul_neg' := sorry

structure Diagonal (M : Type*) where
  fst : M
  snd : M
  eq : fst = snd

attribute [simp] Diagonal.eq

@[ext] lemma Diagonal.ext {x y : Diagonal M} (h1 : x.1 = y.1) (h2 : x.2 = y.2) : x = y := by
  cases x; cases y; congr

attribute [simp] Diagonal.ext_iff

instance : HasReflect (Diagonal M) (M × M) (fun x ↦ x.1 = x.2) where
  coe x := (x.fst, x.snd)
  reflect x p := ⟨x.1, x.2, p⟩

instance [AddCommGroup M] : AddCommGroup (Diagonal M) :=
  HasReflect.addCommGroup _ (M × M) (fun x ↦ x.1 = x.2) rfl (by simp)

[Kenny Lau]

I'm asking here to gauge if this is a good idea; basically this is useful for when something is morally a subtype, but you want to make it a separate definition rather than just to use subtype. Is there any usecases for that?

[Kenny Lau]

For example, the recently merged #26060 (Grassmannians) used structure rather than subtype:

[Kenny Lau]

@[stacks 089R] structure Grassmannian extends Submodule R M where
  finite_quotient : Module.Finite R (M ⧸ toSubmodule)
  projective_quotient : Projective R (M ⧸ toSubmodule)
  rankAtStalk_eq : ∀ p, rankAtStalk (R := R) (M ⧸ toSubmodule) p = k

[Kenny Lau]

image.png

[Kenny Lau]

the justification was this comment (@Eric Wieser , do you remember why that was a good idea?)

[Kenny Lau]

maybe it's for better instances

[Kenny Lau]

or maybe I should have just used the equiv and transport the module structure... on hindsight maybe this code can be avoided

[Kenny Lau]

idk if there would be defeq problems tho if I use equiv...

[Ruben Van de Velde]

I'm thinking because the separate fields feel more ergonomic

[Kenny Lau]

Kenny Lau said:

or maybe I should have just used the equiv and transport the module structure... on hindsight maybe this code can be avoided

I'm mainly following the philosophy of IsLocalization here

[Kenny Lau]

that sometimes some explicit conditions is better than just an equiv

[Andrew Yang]

Why not just docs#Function.Injective.addCommGroup etc?

[Kenny Lau]

oh yeah I eventually discovered that instead