Add FiniteDimensional for affine subspaces

[martinwintermath]

No description provided.

[YaelDillies]

This is the sort of lemmas that should be proved by simping away the new definition. I advise you use this proof as much as possible to make sure that we have all the required simp lemmas:

Suggested change

	unfold Affine.FinDim
	rw [vectorSpan_convexHull]
	simp [Affine.FinDim]

[YaelDillies]

Suggested change

	theorem _root_.Affine.FinDim.convexHull {s : Set A} (hs : Affine.FinDim R s) :
	protected theorem _root_.Affine.FinDim.convexHull {s : Set A} (hs : Affine.FinDim R s) :

[YaelDillies]

Suggested change

	theorem dim_eq_affine_dim (s : AffineSubspace K P) [Nonempty s] :
	theorem dim_eq_affineSpaceDim (s : AffineSubspace K P) [Nonempty s] :

Same below

[YaelDillies]

Suggested change

	theorem finiteDimensional_top_iff :
	(⊤ : AffineSubspace K P).FinDim ↔ _root_.FiniteDimensional K V := by
	theorem finDim_top_iff :
	(⊤ : AffineSubspace K P).FinDim ↔ _root_.FiniteDimensional K V := by

[YaelDillies]

Suggested change

	theorem finiteDimensional_iff_of_equiv (e : P ≃ᵃ[K] Q) :
	FiniteDimensional K P ↔ FiniteDimensional K Q := by
	theorem finiteDimensional_congr (e : P ≃ᵃ[K] Q) :
	FiniteDimensional K P ↔ FiniteDimensional K Q := by

[YaelDillies]

Suggested change

	theorem finDim_eq_of_equiv (e : P ≃ᵃ[K] Q) : finDim K P = finDim K Q :=
	theorem finDim_congr (e : P ≃ᵃ[K] Q) : finDim K P = finDim K Q :=

[martinwintermath]

@YaelDillies Your are fast! Sorry, this PR is 100% AI generated and not even read by me in detail. I was just a proof of concept to show @vlad902 what I have in mind. Still something I hope to go for. Feedback still welcome of course! But I worry there will be too many improvements at this point 😄 .

[YaelDillies]

I am a compulsive reviewer, sorry 😁

[martinwintermath]

@vlad902

The definition seems fine, it's an abbrev which I think is good. There's a lot of unnecessary copy-and-paste slop that is hard to wade through.

I'm not sure why the use of this typeclass was changed from a typeclass parameter to an explicit hypothesis

Can you say were exactly?
Do you mean this?:

theorem _root_.Affine.FinDim.convexHull {s : Set A} (hs : Affine.FinDim R s)

Why should it be a typeclass argument?

and another thing I find odd is that AffineSubspace.FinDim is defined using AffineSubspace.direction but Affine.FinDim is defined using vectorSpan, maybe it should be defined using FinDim (affineSpan R s).direction instead to match?

I was also wondering whether there should be both FinDim for sets and affine subspaces. I tend to say yes. The next question is how similar they should be. For example, is there a good reason to have them similar e.g. because of defeq? Otherwise implementation convenience might point the other way.

And did you mean Affine.FinDim can be FinDim (affineSpan R s) (without .directions).

[martinwintermath]

My goal is to discuss what of this AI generated code we want in principle, and then I (or someone else, who is quicker) can make this into a proper PR. My understanding is that we want all three of these:

• a definition Affine.FinDim for sets
• a definition AffineSubspace.FinDim for affine subspaces
• a class AffineSpace.FiniteDimensional for affine spaces

Yes, this causes duplication of API, but I see no way this can currently be handled otherwise.