English
The module topology on the finite product ∀ i, A i agrees with the product of the module topologies on each A i.
Русский
На конечном произведении ∀ i, A i модульная топология совпадает с произведением модульных топологий каждого A i.
LaTeX
$$$IsModuleTopology(R, ∀ i, A i)$$$
Lean4
/-- The product of the module topologies for a finite family of modules over a topological ring
is the module topology. -/
instance instPi : IsModuleTopology R (∀ i, A i) := by
-- This is an easy induction on the size of the finite type, given the result
-- for binary products above. We use a "decategorified" induction principle for finite types.
induction ι using Finite.induction_empty_option
· -- invariance under equivalence of the finite type we're taking the product over
case of_equiv X Y e _ _ _ _ _ => exact iso (ContinuousLinearEquiv.piCongrLeft R A e)
· -- empty case
infer_instance
· -- "inductive step" is to check for product over `Option ι` case when known for product over `ι`
case h_option ι _ hind _ _ _ _ =>
-- `Option ι` is a `Sum` of `ι` and `Unit`
let e : Option ι ≃ ι ⊕ Unit := Equiv.optionEquivSumPUnit ι
suffices IsModuleTopology R ((i' : ι ⊕ Unit) → A (e.symm i')) from
iso
(.piCongrLeft R A e.symm)
-- but such a product is isomorphic to a binary product
-- of (product over `ι`) and (product over `Unit`)
suffices IsModuleTopology R (((s : ι) → A (e.symm (Sum.inl s))) × ((t : Unit) → A (e.symm (Sum.inr t)))) from
iso (ContinuousLinearEquiv.sumPiEquivProdPi R ι Unit _).symm
have := iso (ContinuousLinearEquiv.piUnique R (fun t ↦ A (e.symm (Sum.inr t)))).symm
infer_instance
