Defining IsHomogenization as linear equivalence

[ooovi]

as suggested on zulip, redefines IsHomogenization as something thats linearly equivalent to the canonical homogenization. this is maybe nicer than the axiomatic definition because transferring API from canonical homogenization is smoother. also provides the axiomatic constructor

closes #59

[ooovi]

There's a draft PR to mathlib now, and I have adjusted the code here to match its current state.
leanprover-community/mathlib4#44160

[martinwintermath]

Can we call this canonical?

[martinwintermath]

Does it not suffice to only pass weight and weight \ne 0?

And a second def which takes embed, Injective embed and 0 \not\in embed.range or so? Or do we even need this, because maybe this is better:

A version that takes an affine subspace E and 0 \not\in E.

Update. After some thought my current idea is:

• have the weight version
• don't have the emed version
• but have a def that turns an affine subspace E, a proof of 0 \not\in E and a proof of E.codim = 1 into a linear form weight. (the last hypothesis was missing above). So to say a reverse of AffineSubspace.comap for hyperplanes.
• maybe add an affine subspace version, that just uses this def

[ooovi]

i'd kind of like to keep this def, since it mirrors the axiomatic definition. i added a constructor for weight \ne 0 over DivisionRing and created #110 for the AffineSubspace constructor.

[martinwintermath]

Is it helpful to have the nonempty statement as a typeclass argument? Can we not just ask for g \neq 0? This feels more canonical.

Update

• my suggestion does not suffice as it does not imply what we need over general rings
• there should nevertheless be a second def which uses g \neq 0 under sufficiently strong assumptions about R
• Nonempty should not be a typeclass parameters since it cannot be inferred here ... I think. Unless, we make suitable instances, but not sure we should.

[ooovi]

I'm not sure about the typeclass question. IsHomogenization needs an affine space as second arg, so the Nonempty instance actually needs to be available to state the type of this def. So I could

• make it be (h : Nonempty ...) which I probably should not since Nonempty is a class
• make it be something like

  def ofWeightOne (g : W →ₗ[R] R) (h : (comap g.toAffineMap {1} : Set W).Nonempty) :
      letI := nonempty_subtype.mpr h
      IsHomogenization R (comap g.toAffineMap {1}) W := ...
  

  which probably isn't a good idea
  Mathlib has a couple of places where Nonempty instances are passed by the caller. None of them is about a specific set like this case tho. Lets leave it like this and see what review says about it?

[martinwintermath]

I see. Another way out is to have parameters linear form g, AffineSubspace E, [Nonempty E], E = comap g {1}. Then the typeclass argument makes more sense and has a chance of firing automatically. The drawback is that we are redundant. But one could call it like ofWeightOne g (comap g {1}) rfl.

@YaelDillies Can you help out? What is the right design here?

[martinwintermath]

Also, I am not sure there is anything morally wrong with (h : Nonempty ...) just because it is a class. In my understanding, being a class allows you to be inferred automatically, but it does not take anything away that was permissable before.

[YaelDillies]

Is this not equivalent to 1 \in range g which is itself equivalent to g \ne 0? Why this weird Nonempty assumption?

[ooovi]

i need to pass an AffineSpace to IsHomogenization, so i need to have Nonempty for it. no?

also i think if you don't have multiplicative inverses in your ring there are linear maps that are neither 0 nor does their range contain 1.

[YaelDillies]

You could prove it inline like this:

Suggested change

	def ofWeightOne (g : W →ₗ[R] R) [Nonempty (comap g.toAffineMap {1})] :
	def ofWeightOne (g : W →ₗ[R] R) (hg : g \ne 0) :
	have : Nonempty (comap g.toAffineMap {1}) ;= sorry