Trying to put instance of a compact space on a Zp-module

Stream: new members

[Stepan Nesterov]

I am trying to tell Lean that a finite topolgical Z_p-module is a compact space. The following code complies perfectly:

instance {R : Type*} [AddCommMonoid R] [Module ℤ_[3] R]
    [Module.Finite ℤ_[3] R] [TopologicalSpace R] [IsModuleTopology ℤ_[3] R] :
    CompactSpace R := sorry

But if I try to do the same in general

instance {p : ℕ} [Fact p.Prime] {R : Type*} [AddCommMonoid R] [Module ℤ_[p] R]
    [Module.Finite ℤ_[p] R] [TopologicalSpace R] [IsModuleTopology ℤ_[p] R] :
    CompactSpace R := sorry

I get an error message
cannot find synthesization order for instance @instCompactSpaceOfFactPrimeOfFiniteOfIsModuleTopologyPadicIntOfNatNat with type
∀ {p : ℕ} [Fact (Nat.Prime p)] {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Module ℤ_[3] R]
[Module.Finite ℤ_[3] R] [inst_3 : TopologicalSpace R] [IsModuleTopology ℤ_[3] R], CompactSpace R
all remaining arguments have metavariables:
Fact (Nat.Prime ?p)

What is the issue here?

[Yakov Pechersky]

It can never guess which exact p you mean. It can't invent the p.

[Yakov Pechersky]

Your goal only mentions R, but the hypotheses have a free p.

[Yakov Pechersky]

You can make your instance a lemma, and invoke it at your desired call site

[Stepan Nesterov]

Ok making it a lemma works like a charm :+1:

[Kevin Buzzard]

@Stepan Nesterov your Lean code does not say "R is a topological Z_p-module" (which just means "addition and scalar multiplication are continuous"), it says "R has got some magical canonical topology induced from the fact that a topological ring is acting on it" (or in other words R has the finest topology making addition and scalar multiplication continuous, as opposed to an arbitrary such topology).