Zulip Chat Archive

Stream: maths

Topic: f-adic ring


view this post on Zulip Kenny Lau (Aug 23 2020 at 06:34):

An ff-adic ring is a topological ring AA for which there is an open subring A0A_0 and a finite generated ideal IA0I \trianglelefteq A_0 such that {Inn0}\{I^n \mid n \ge 0\} is a neighbourhood basis of 00.

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:34):

How should we formalize this in Lean?

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:35):

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

view this post on Zulip Kevin Buzzard (Aug 23 2020 at 06:48):

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

view this post on Zulip 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)
(top : is_ideal_adic J)

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:49):

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

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:50):

how would you state the theorem then?

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:52):

Wedhorn 6.14

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:52):

how can we even do these transitions seamlessly?

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:53):

sBsB is open because s:AAs : A \to A is a homeomorphism

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:53):

so sBsB is an open ideal of BB

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:57):

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

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:58):

sBsB opens so many cans of worms

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:58):

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

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:59):

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

view this post on Zulip Kenny Lau (Aug 23 2020 at 06:59):

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

view this post on Zulip Kenny Lau (Aug 23 2020 at 07:00):

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

view this post on Zulip Kenny Lau (Aug 23 2020 at 07:00):

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

view this post on Zulip Kenny Lau (Aug 23 2020 at 07:00):

but in maths they are the same set

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Aug 23 2020 at 07:02):

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

view this post on Zulip Kevin Buzzard (Aug 23 2020 at 07:02):

right

view this post on Zulip Kenny Lau (Aug 23 2020 at 07:02):

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

view this post on Zulip Kevin Buzzard (Aug 23 2020 at 07:02):

and they're the same set

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 23 2020 at 07:23):

how to tell Lean "they are equal because they are both sA0sA_0"?

view this post on Zulip Kevin Buzzard (Aug 23 2020 at 07:34):

ext, split, etc?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 23 2020 at 07:40):

Your objection is that "this is obvious"?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 23 2020 at 07:42):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Kenny Lau (Aug 23 2020 at 07:50):

you don't need exists_congr

view this post on Zulip Kenny Lau (Aug 23 2020 at 07:50):

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

view this post on Zulip Kenny Lau (Aug 23 2020 at 07:50):

as you say, in maths the identifications are very transparent

view this post on Zulip Kevin Buzzard (Aug 23 2020 at 07:50):

you should learn to love the simplifier

view this post on Zulip Kenny Lau (Aug 23 2020 at 07:50):

"the ideal spanned by s" is sBsB

view this post on Zulip Kevin Buzzard (Aug 23 2020 at 07:51):

That's a theorem

view this post on Zulip Kevin Buzzard (Aug 23 2020 at 07:51):

the ideal spanned by s is some stupid Inf probably

view this post on Zulip Kevin Buzzard (Aug 23 2020 at 07:51):

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

view this post on Zulip Kevin Buzzard (Aug 23 2020 at 07:51):

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

view this post on Zulip Kenny Lau (Aug 23 2020 at 07:52):

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

view this post on Zulip Kenny Lau (Aug 23 2020 at 07:52):

yeah exactly


Last updated: May 06 2021 at 18:20 UTC