Every surjective `A`-linear map between modules with module topology is open.
This is the **open mapping theorem** for module topologies (Prop 6.18(2) of Wedhorn). 

A short exact sequence `0 → M₁ → M₂ → M₃ → 0` of modules with module topology
is **strict exact**: `g` is an open map and `f` is continuous.
This is a consequence of Prop 6.18(2) (open mapping theorem). 

**Wedhorn Proposition 6.17 (ideal form):** Every ideal in a complete Tate
ring `A` with a noetherian ring of definition `P.A₀` is closed.

The statement requires a pair of definition `P = (A₀, I)` such that `A₀` is
noetherian. This is automatic for **strongly noetherian** Tate rings (the
setting of Huber's theory, Wedhorn Def 6.9), and downstream callers can
discharge the `IsNoetherianRing P.A₀` hypothesis from a strongly-noetherian
structure.

**Proof sketch (Krull intersection on the ring of definition).**

1. `A₀ = P.A₀` is an open, hence closed (open subgroup of a topological
   group), subring of `A`. It inherits `CompleteSpace`, `T2Space`, and its
   subspace topology is the `I`-adic topology by `P.isAdic`.
2. `J₀ := J.comap P.A₀.subtype`, the pullback of `J` to `A₀`, is closed in
   `A₀` by the abstract helper
   `isClosed_ideal_of_adicComplete_noetherian` applied to the noetherian
   complete T₂ adic ring `A₀`.
3. `closure_A(J) ∩ A₀ = J₀`: for `x ∈ A₀`, membership in `closure_A(J)` is
   characterised by the `A`-neighborhood basis `{x + Subtype.val '' I^n}`,
   which equals the `A₀`-basis `{x + I^n}` under the inclusion. So
   `x ∈ closure_A(J) ↔ x ∈ closure_{A₀}(J₀)`, and the latter equals `J₀`
   since `J₀` is closed in `A₀`.
4. To close the argument for a general `x ∈ closure_A(J)`, we use that `P`
   can be chosen as a **principal pair** (via
   `IsTateRing.exists_principal_pairOfDefinition`) with generator `π` a
   topologically nilpotent unit in `A`. Then some power `π^k · x` lands in
   `A₀` (because `π^k → 0` and `A₀` is an open neighborhood of `0`), and
   `π^k · x ∈ closure_A(J) ∩ A₀ = J₀ ⊆ J`, so `x = π^(-k) · (π^k · x) ∈ J`.

Because the signature of the theorem takes an **arbitrary** pair `P`, not
necessarily principal, step 4 uses `IsTateRing.exists_principal_pairOfDefinition`
to produce a principal pair `P'` and argues via `P'` whose `A₀'`-inclusion
factors through `P.A₀`'s closure — this only needs the *abstract* existence of a
topologically nilpotent unit and `P.A₀` being open. 

**Sub-lemma — type-level sheaf condition for the locally-fraction subpresheaf.**

This is the *type-level* sheaf condition on `subpresheafToTypes
isLocallyFraction.toPrelocalPredicate`, which is precisely the underlying
type-presheaf of `structurePresheaf A` (modulo bundling into
`CompleteTopCommRingCat`). The proof is a direct application of Mathlib's
`subpresheafToTypes.isSheaf` for any `LocalPredicate`. Used by
`structurePresheaf_isSheaf` below as the type-level input to the (still-pending)
`CompleteTopCommRingCat`-to-types infrastructure transfer.

Per CLAUDE.md sub-lemma policy: this fully discharges the type-level half
of `structurePresheaf_isSheaf`, isolating the remaining obligation to the
forgetful-functor / concrete-category infrastructure for
`CompleteTopCommRingCat`.