## Stream: maths

#### Kenny Lau (Aug 23 2020 at 06:34):

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 (Aug 23 2020 at 06:34):

How should we formalize this in Lean?

#### Kenny Lau (Aug 23 2020 at 06:35):

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 (Aug 23 2020 at 06:48):

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

#### Kenny Lau (Aug 23 2020 at 06:49):

/-- 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)


#### Kenny Lau (Aug 23 2020 at 06:49):

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

#### Kenny Lau (Aug 23 2020 at 06:50):

how would you state the theorem then?

Wedhorn 6.14

#### Kenny Lau (Aug 23 2020 at 06:52):

how can we even do these transitions seamlessly?

#### Kenny Lau (Aug 23 2020 at 06:53):

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

#### Kenny Lau (Aug 23 2020 at 06:53):

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

#### Kevin Buzzard (Aug 23 2020 at 06:57):

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 (Aug 23 2020 at 06:57):

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

#### Kenny Lau (Aug 23 2020 at 06:58):

$sB$ opens so many cans of worms

#### Kenny Lau (Aug 23 2020 at 06:58):

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

#### Kenny Lau (Aug 23 2020 at 06:59):

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

#### Kenny Lau (Aug 23 2020 at 06:59):

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

#### Kenny Lau (Aug 23 2020 at 07:00):

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

#### Kenny Lau (Aug 23 2020 at 07:00):

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

#### Kenny Lau (Aug 23 2020 at 07:00):

but in maths they are the same set

#### Kevin Buzzard (Aug 23 2020 at 07:01):

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 (Aug 23 2020 at 07:02):

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

right

#### Kenny Lau (Aug 23 2020 at 07:02):

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

#### Kevin Buzzard (Aug 23 2020 at 07:02):

and they're the same set

#### Kenny Lau (Aug 23 2020 at 07:05):

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

#### Kenny Lau (Aug 23 2020 at 07:22):

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 (Aug 23 2020 at 07:23):

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

ext, split, etc?

#### Kevin Buzzard (Aug 23 2020 at 07:40):

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 (Aug 23 2020 at 07:40):

Your objection is that "this is obvious"?

#### Kenny Lau (Aug 23 2020 at 07:41):

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

#### Kenny Lau (Aug 23 2020 at 07:42):

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

#### Kevin Buzzard (Aug 23 2020 at 07:44):

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 (Aug 23 2020 at 07:46):

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 (Aug 23 2020 at 07:47):

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 (Aug 23 2020 at 07:50):

you don't need exists_congr

#### Kenny Lau (Aug 23 2020 at 07:50):

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

#### Kenny Lau (Aug 23 2020 at 07:50):

as you say, in maths the identifications are very transparent

#### Kevin Buzzard (Aug 23 2020 at 07:50):

you should learn to love the simplifier

#### Kenny Lau (Aug 23 2020 at 07:50):

"the ideal spanned by s" is $sB$

That's a theorem

#### Kevin Buzzard (Aug 23 2020 at 07:51):

the ideal spanned by s is some stupid Inf probably

#### Kevin Buzzard (Aug 23 2020 at 07:51):

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

#### Kevin Buzzard (Aug 23 2020 at 07:51):

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

#### Kenny Lau (Aug 23 2020 at 07:52):

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

#### Kenny Lau (Aug 23 2020 at 07:52):

yeah exactly

Last updated: May 06 2021 at 18:20 UTC