Refactoring the set of instance requirements on a type

Stream: new members

[Jineon Baek]

I need to require a fixed set of instances to a type multiple times

theorem EuclideanSpace.induction_on_dimension
    {P : (α : Type) →
      [AddCommGroup α] → [TopologicalSpace α] →  [TopologicalAddGroup α] → [T2Space α] → [Module ℝ α] → [ContinuousSMul ℝ α] → [FiniteDimensional ℝ α] → Sort}
    {base0 : P (EuclideanSpace ℝ (Fin 0))}
    {base1 : P ℝ}
    {induct : {α β : Type} →
      [AddCommGroup α] → [TopologicalSpace α] →  [TopologicalAddGroup α] → [T2Space α] → [Module ℝ α] → [ContinuousSMul ℝ α] → [FiniteDimensional ℝ α] →
      [AddCommGroup β] → [TopologicalSpace β] →  [TopologicalAddGroup β] → [T2Space β] → [Module ℝ β] → [ContinuousSMul ℝ β] → [FiniteDimensional ℝ β] →
      P α → P β → P (α × β)} :
  (α : Type) → [AddCommGroup α] → [TopologicalSpace α] →  [TopologicalAddGroup α] → [T2Space α] → [Module ℝ α] → [ContinuousSMul ℝ α] → [FiniteDimensional ℝ α] → P α := by sorry

All the [AddCommGroup α] → (...) → [FiniteDimensional ℝ α] is very repeatitive and I want to get rid of it. How should I refactor this?

[Jineon Baek]

The set of instances basically tries to characterize a finite dimensional Euclidean real space (R^n) in an abstract sense

[Jineon Baek]

...now I am realising that I would also need to require that P a is equivalent under isomorphisms on a

[Matteo Cipollina]

Hi, I found this characterization very useful so I've tried to refactor the EuclideanSpaceStructure typeclass . I've split it into EuclideanBaseStructure (core properties) and EuclideanSpaceIsoInvariant (for the isomorphism invariance). Hope this helps!

import Mathlib

-- Original theorem
theorem EuclideanSpace.induction_on_dimension'
    {P : (α : Type) →
      [AddCommGroup α] → [TopologicalSpace α] →  [TopologicalAddGroup α] → [T2Space α] → [Module ℝ α] → [ContinuousSMul ℝ α] → [FiniteDimensional ℝ α] → Sort}
    {base0 : P (EuclideanSpace ℝ (Fin 0))}
    {base1 : P ℝ}
    {induct : {α β : Type} →
      [AddCommGroup α] → [TopologicalSpace α] →  [TopologicalAddGroup α] → [T2Space α] → [Module ℝ α] → [ContinuousSMul ℝ α] → [FiniteDimensional ℝ α] →
      [AddCommGroup β] → [TopologicalSpace β] →  [TopologicalAddGroup β] → [T2Space β] → [Module ℝ β] → [ContinuousSMul ℝ β] → [FiniteDimensional ℝ β] →
      P α → P β → P (α × β)} :
  (α : Type) → [AddCommGroup α] → [TopologicalSpace α] →  [TopologicalAddGroup α] → [T2Space α] → [Module ℝ α] → [ContinuousSMul ℝ α] → [FiniteDimensional ℝ α] → P α := by sorry

-- Helper typeclass to bundle the core properties
class EuclideanBaseStructure (α : Type) extends
  AddCommGroup α, TopologicalSpace α, TopologicalAddGroup α, T2Space α,
  Module ℝ α, ContinuousSMul ℝ α, FiniteDimensional ℝ α

-- Separate typeclass for the isomorphism invariance property
class EuclideanSpaceIsoInvariant (P : (α : Type) → Sort) (α : Type) [EuclideanBaseStructure α] where
  isomorphism_invariant : {β : Type} → [EuclideanBaseStructure β] → (α ≃ₗ[ℝ] β) → P α ↔ P β

-- Final structure combining the base and the invariance
class EuclideanSpaceStructure (P : (α : Type) → Sort) (α : Type)
  extends EuclideanBaseStructure α, EuclideanSpaceIsoInvariant P α

-- Refactored induction theorem
theorem EuclideanSpace.induction_on_dimension
    (P : (α : Type) → Sort)
    {base0 : P (EuclideanSpace ℝ (Fin 0))}
    {base1 : P ℝ}
    {induct : {α β : Type} → [EuclideanSpaceStructure P α] → [EuclideanSpaceStructure P β] →
      P α → P β → P (α × β)} :
  (α : Type) → [EuclideanSpaceStructure P α] → P α := by sorry

-- Instances for ℝ and EuclideanSpace, now parameterized by P
noncomputable instance : EuclideanBaseStructure ℝ where
  toAddCommGroup := inferInstance
  toTopologicalSpace := inferInstance
  toTopologicalAddGroup := inferInstance
  toT2Space := inferInstance
  toModule := inferInstance
  toContinuousSMul := inferInstance

instance (P : (α : Type) → Sort) : EuclideanSpaceIsoInvariant P ℝ where
  isomorphism_invariant := sorry

noncomputable instance (P : (α : Type) → Sort) : EuclideanSpaceStructure P ℝ where

noncomputable instance (n : ℕ) : EuclideanBaseStructure (EuclideanSpace ℝ (Fin n)) where
  toAddCommGroup := inferInstance
  toTopologicalSpace := inferInstance
  toTopologicalAddGroup := inferInstance
  toT2Space := inferInstance
  toModule := inferInstance
  toContinuousSMul := inferInstance

instance (P : (α : Type) → Sort) (n : ℕ) : EuclideanSpaceIsoInvariant P (EuclideanSpace ℝ (Fin n)) where
  isomorphism_invariant := sorry

noncomputable instance (P : (α : Type) → Sort) (n : ℕ) : EuclideanSpaceStructure P (EuclideanSpace ℝ (Fin n)) where

[Jineon Baek]

@Matteo Cipollina This helps a ton!! Much thanks :blush: