f-adic ring

Stream: maths

[Kenny Lau]

An $f$-adic ring is a topological ring $A$ for which there is an open subring $A_0$ and a finite generated ideal $I \trianglelefteq A_0$ such that $\{I^n \mid n \ge 0\}$ is a neighbourhood basis of $0$.

[Kenny Lau]

How should we formalize this in Lean?

[Kenny Lau]

Theorem: if $x \in A$ is such that $\lim_{n \to \infty} x^n = 0$, then $x^n \in A_0$ for $n \gg 0$.

[Kevin Buzzard]

You can look at how we formalised it in the perfectoid project

[Kenny Lau]

/-- A “ring of definition” of a topological ring A is an open subring A₀
that has a finitely generated ideal J such that the topology on A₀ is J-adic.
See [Wedhorn, Def 6.1] -/
structure Huber_ring.ring_of_definition
  (A₀ : Type*) (A : Type*)
  [comm_ring A₀] [topological_space A₀] [topological_ring A₀]
  [comm_ring A] [topological_space A] [topological_ring A]
  extends algebra A₀ A :=
(emb : open_embedding to_fun)
(J   : ideal A₀)
(fin : J.fg)
(top : is_ideal_adic J)

[Kenny Lau]

https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/Huber_ring/basic.lean

[Kenny Lau]

how would you state the theorem then?

[Kenny Lau]

Wedhorn 6.14

[Kenny Lau]

how can we even do these transitions seamlessly?

[Kenny Lau]

$sB$ is open because $s : A \to A$ is a homeomorphism

[Kenny Lau]

so $sB$ is an open ideal of $B$

[Kevin Buzzard]

Well, we have a ring homomorphism B -> A, so either B is a subring of A, or A is a B-algebra, and you have to choose which one and then it's irritating when you want the other one

[Kenny Lau]

no in maths they're all just subsets of each other and stuff

[Kenny Lau]

$sB$ opens so many cans of worms

[Kenny Lau]

it's the fusion of different types that are meant to be segregated

[Kenny Lau]

in maths we just say, oh just multiply the elements pointwise

[Kenny Lau]

in Lean the ideal $sB$ is ideal.span ({s} : set B)

[Kenny Lau]

and the open set is (*) s '' B

[Kenny Lau]

(the two Bs in the pseudocode already have different meanings)

[Kenny Lau]

but in maths they are the same set

[Kevin Buzzard]

I don't know if s has type A or type B. In Lean they're the same set too, right? But this is a lemma.

[Kenny Lau]

when I see $sB$ in the statement, my internal representation is ideal.span {s}

[Kevin Buzzard]

right

[Kenny Lau]

then when it says $s : A \to A$ is a homeomorphism so $sB$ is open, I see (*) s '' B

[Kevin Buzzard]

and they're the same set

[Kenny Lau]

so it's a translator seeing "you", ne sachant pas si on doit ecrire "tu" ou "vous"

[Kenny Lau]

import ring_theory.algebra
import topology.algebra.ring

variables (A₀ : Type*) (A : Type*)
variables [comm_ring A₀] [topological_space A₀] [topological_ring A₀]
variables [comm_ring A] [topological_space A] [topological_ring A]
variables [algebra A₀ A] (emb : open_embedding (algebra_map A₀ A))

theorem foo {s : A} (hs : is_unit s) {X : set A} (hx : is_open X) : is_open ((*) s '' X) :=
let ⟨t, ht⟩ := is_unit_iff_exists_inv.1 hs in
by { convert continuous_mul_left t _ hx,
  exact set.ext (λ z, ⟨λ ⟨y, hy, hsyz⟩, hsyz ▸ show t * (s * y) ∈ X,
      by rwa [← mul_assoc, mul_comm t, ht, one_mul],
    λ hz, ⟨t * z, hz, by rw [← mul_assoc, ht, one_mul]⟩⟩) }

include emb

theorem bar (s : A₀) (hs : is_unit (algebra_map A₀ A s)) :
  is_open (ideal.span ({s} : set A₀) : set A₀) :=
begin
  rw emb.open_iff_image_open,
  convert foo _ hs emb.open_range,
  -- ⊢ ⇑(algebra_map A₀ A) '' ↑(ideal.span {s}) =
  --     has_mul.mul (⇑(algebra_map A₀ A) s) '' set.range ⇑(algebra_map A₀ A)
  sorry
end

[Kenny Lau]

how to tell Lean "they are equal because they are both $sA_0$"?

[Kevin Buzzard]

ext, split, etc?

[Kevin Buzzard]

theorem bar (s : A₀) (hs : is_unit (algebra_map A₀ A s)) :
  is_open (ideal.span ({s} : set A₀) : set A₀) :=
begin
  rw emb.open_iff_image_open,
  convert foo _ hs emb.open_range,
  -- ⊢ ⇑(algebra_map A₀ A) '' ↑(ideal.span {s}) =
  --     has_mul.mul (⇑(algebra_map A₀ A) s) '' set.range ⇑(algebra_map A₀ A)
  ext,
  split,
  { rintro ⟨a0, ha0, rfl⟩,
    rw submodule.mem_coe at ha0,
    rw ideal.mem_span_singleton' at ha0,
    rcases ha0 with ⟨a1, rfl⟩,
    rw set.mem_image,
    use (algebra_map A₀ A a1),
    use a1,
    simp [mul_comm] },
  { rintro ⟨-, ⟨a1, rfl⟩, rfl⟩,
    use s * a1,
    split,
    { rw submodule.mem_coe,
      rw ideal.mem_span_singleton',
      use a1,
      apply mul_comm },
    { simp } }
end

[Kevin Buzzard]

Your objection is that "this is obvious"?

[Kenny Lau]

my objection is that the mathematician identifies the two sets, an identification that cannot be done in Lean

[Kenny Lau]

I have no objection; I am merely pointing out that identifications open cans of worms

[Kevin Buzzard]

begin
  rw emb.open_iff_image_open,
  convert foo _ hs emb.open_range,
  -- ⊢ ⇑(algebra_map A₀ A) '' ↑(ideal.span {s}) =
  --     has_mul.mul (⇑(algebra_map A₀ A) s) '' set.range ⇑(algebra_map A₀ A)
  ext,
  rw set.mem_image,
  rw set.mem_image,
  simp_rw set.mem_range,
  simp_rw submodule.mem_coe,
  simp_rw ideal.mem_span_singleton',
  simp [exists_congr, mul_comm]
end

[Kevin Buzzard]

begin
  rw emb.open_iff_image_open,
  convert foo _ hs emb.open_range,
  ext,
  simp [ideal.mem_span_singleton', exists_congr, mul_comm]
end

[Kevin Buzzard]

Now the proof is the same as the maths proof -- "they're equal because they have the same elements -- oh by the way the ideal spanned by a singleton is its multiples"

[Kenny Lau]

you don't need exists_congr

[Kenny Lau]

I object that the maths proof is "they're equal because they're the same"

[Kenny Lau]

as you say, in maths the identifications are very transparent

[Kevin Buzzard]

you should learn to love the simplifier

[Kenny Lau]

"the ideal spanned by s" is $sB$

[Kevin Buzzard]

That's a theorem

[Kevin Buzzard]

the ideal spanned by s is some stupid Inf probably

[Kevin Buzzard]

that's another of our definitions of the ideal spanned by something

[Kevin Buzzard]

of course things are the same if you're allowed to have 10 definitions for everything

[Kenny Lau]

yeah but you'll notice that the text doesn't even say it

[Kenny Lau]

yeah exactly