Zulip Chat Archive

Stream: maths

Topic: Ideal lemma


view this post on Zulip orlando (Mar 28 2020 at 09:16):

Hello,
I have a little problem !

lemma Test_2 (A B C:Type)[comm_ring A][comm_ring B][comm_ring C]
(I : ideal A)(f: A  B) (g: B   C)[is_ring_hom f][is_ring_hom g]:
   ideal.map (g  f) I = ideal.map g (ideal.map f I) :=
begin
   sorry,
 end

view this post on Zulip orlando (Mar 28 2020 at 09:17):

There is map_comp for module but not for ideal ! I don't understand how to deal !!!

view this post on Zulip Mario Carneiro (Mar 28 2020 at 09:21):

I think ideal.map is just sugar over module.map, so you may be able to prove this by just applying module.map_comp

view this post on Zulip orlando (Mar 28 2020 at 09:31):

Ok, but the little problem is gg is not AA module morphism

lemma map_comp (f : M [R] M₂) (g : M₂ [R] M₃) (p : submodule R M) :
 ```

view this post on Zulip Mario Carneiro (Mar 28 2020 at 09:34):

welp, I guess you will have to prove it ;)

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 09:37):

is_ring_hom is deprecated right? @orlando you should stop using it and use ring_hom

view this post on Zulip Kenny Lau (Mar 28 2020 at 09:37):

import ring_theory.ideal_operations

lemma Test_2 (A B C : Type) [comm_ring A] [comm_ring B] [comm_ring C]
  (I : ideal A) (f : A  B) (g : B  C) [is_ring_hom f] [is_ring_hom g] :
  ideal.map (g  f) I = ideal.map g (ideal.map f I) :=
le_antisymm
  (ideal.map_le_iff_le_comap.2 $ λ x hxI, ideal.mem_map_of_mem $ ideal.mem_map_of_mem hxI)
  (ideal.map_le_iff_le_comap.2 $ ideal.map_le_iff_le_comap.2 $ λ x hxI, ideal.mem_map_of_mem hxI)

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 09:37):

Kenny can you do this with ring_hom?

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 09:37):

Just to show Orlando the bundled approach?

view this post on Zulip Mario Carneiro (Mar 28 2020 at 09:37):

what was that galois connection emoji again

view this post on Zulip Kenny Lau (Mar 28 2020 at 09:38):

ideal.map takes is_ring_hom

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 09:39):

:-/

view this post on Zulip Mario Carneiro (Mar 28 2020 at 09:39):

refactor time

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 09:41):

It's submodule.map we should be talking about not module.map

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 09:42):

Ideals are submodules not modules

view this post on Zulip Mario Carneiro (Mar 28 2020 at 09:42):

zulip needs autocompletion

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 09:42):

And easy ability to input Unicode on phones

view this post on Zulip orlando (Mar 28 2020 at 09:48):

I don't understand anything Mario ! But it's work :tada:

view this post on Zulip orlando (Mar 28 2020 at 09:51):

What is the $ ???

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 09:51):

a $ b c d is just a (b c d)

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 09:52):

$ is notation (anything which is not letters and _ is usually notation) and you can see what it does with #print notation $

view this post on Zulip Mario Carneiro (Mar 28 2020 at 09:52):

we should put that in the faq

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 09:53):

The output is _ `$`:1 _:0 := #1 #0 which means a $ b := a b and make it right associative and have "power" 1 (which is low). Here's more information written for mathematicians

view this post on Zulip Mario Carneiro (Mar 28 2020 at 09:55):

It's too bad that looking up info on one piece of unfamimiar notation shows a whole bunch of unfamiliar notation

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 09:55):

$ is particularly bad in this regard

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 09:56):

because the binding powers are 1 and 0, and the missing variables are #1 and #0

view this post on Zulip Mario Carneiro (Mar 28 2020 at 09:56):

and they are numbered in reverse order because de bruijn thought it would be a good idea

view this post on Zulip Johan Commelin (Mar 28 2020 at 09:57):

Yes, I'm still wondering why he didn't use negative integers, so that they would be ordered the right way :rolling_on_the_floor_laughing:

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 09:59):

You might naively think he'd want to use non-positive ones, but the negative integers are the inbuilt constructor

view this post on Zulip orlando (Mar 28 2020 at 18:35):

I make Ideals into a functor :grinning_face_with_smiling_eyes:

For the moment and don't understand really the difference between ring_hom and (ψ : A ⟶ B)

import algebra.category.CommRing
import category_theory.types
import ring_theory.ideals
import ring_theory.ideal_operations
universes  u

local notation `Ring` := CommRing.{u}
local notation `Set` :=  Type u

namespace ideal
lemma ideal_id (A : Ring) (I : ideal A) : ideal.map (𝟙 A)I = I :=
begin
  have g : set.image (𝟙 A) I = (I : set A),
    exact set.image_id I,
    unfold ideal.map,
    rw g,
    exact ideal.span_eq I,
end
lemma ideal_comp (A B C : Ring)(I : ideal A) (f : A   B) (g : B   C)  :
  ideal.map (f  g) I = ideal.map g (ideal.map f I) :=
le_antisymm
  (ideal.map_le_iff_le_comap.2 $ λ x hxI, ideal.mem_map_of_mem $ ideal.mem_map_of_mem hxI)
  (ideal.map_le_iff_le_comap.2 $ ideal.map_le_iff_le_comap.2 $ λ x hxI, ideal.mem_map_of_mem hxI)
end ideal

namespace Omega
def Ω_obj (A : Ring):= ideal A
def Ω_map (A B :Ring)(ψ : A  B) : Ω_obj A  Ω_obj B:= λ I,begin
  exact ideal.map ψ I,
end
def Ω : Ring  Set :=
{
  obj := Ω_obj,
  map := Ω_map,
  map_id' := λ A, begin
    funext I,
    rw category_theory.types_id,
    exact ideal.ideal_id A I,
  end,
  map_comp' := begin
    rintros,
    rw category_theory.types_comp,
    funext I,
    exact ideal.ideal_comp X Y Z I f g,
end,
}
end Omega

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 18:46):

The difference between ring_hom and is_ring_hom is the same as the difference between CommRing and comm_ring. With ring_hom, the function is "bundled" as part of the structure. With is_ring_hom it is an input. Similarly comm_ring takes an input R but CommRing does not.

view this post on Zulip Johan Commelin (Mar 28 2020 at 18:47):

There isn't really a difference between those two types of homs. The difference is in what kind of objects you can stick at the end of the arrow (-;
If you use ring_hom you give it two types R and S, and make sure that there are instances of ring R or comm_semiring S etc floating around.
If you use the category theory arrow, then you have to provide objects of the category Ring or CommRing, and those objects are types + a suitable instance, packaged together.

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 18:48):

@orlando you can replace

λ I,begin
  exact ideal.map ψ I,
end

with exact ideal.map ψ. You don't even need to enter tactic mode.

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 18:48):

Oh! You're talking about the \hom arrow? Right, the only difference is that for one the inputs are unbundled and for the other the inputs are bundled.

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 18:49):

Did you see the definition of functor in mathlib?

view this post on Zulip orlando (Mar 28 2020 at 18:49):

An exemple :

def V_obj (S : set R)(A : Ring) : Type u := { ζ : ring_hom R A |  x  S, ζ (x)  = 0}
--- if i use ζ : R ⟶ A i can't use ζ x = 0 ! Is it normal ?

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 18:50):

structure functor (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D] :
  Type (max v₁ v₂ u₁ u₂) :=
(obj       : C  D)
(map       : Π {X Y : C}, (X  Y)  ((obj X)  (obj Y)))
(map_id'   :  (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
(map_comp' :  {X Y Z : C} (f : X  Y) (g : Y  Z), map (f  g) = (map f)  (map g) . obviously)

The last two structure fields -- map_id' and map_comp' have . obviously at the end, which means "if the user does not prove them, try proving them yourself with the obviously tactic".

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 18:51):

I think it is possible to somehow train obviously to be able to solve these things.

view this post on Zulip orlando (Mar 28 2020 at 18:51):

Hum the definition of functor yes but i don't understand obiously In my case of Ω\Omega, without map_id' this doesn't works !

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 18:52):

I don't understand it either. @Scott Morrison where do we learn about how to train obviously to solve these cases of map_id' and map_comp'? Does it work like that?

view this post on Zulip Johan Commelin (Mar 28 2020 at 18:53):

Kevin Buzzard said:

I think it is possible to somehow train obviously to be able to solve these things.

The training is mostly done by proving the right simp-lemmas before you define the functor.

view this post on Zulip Johan Commelin (Mar 28 2020 at 18:54):

Currently obviously cannot do rw

view this post on Zulip Johan Commelin (Mar 28 2020 at 18:54):

So if your proof really needs to do a rw, then you have to do it your self.

view this post on Zulip Johan Commelin (Mar 28 2020 at 18:54):

But if the proof is something like intros, ext, simp, assumption, then obviously will fill in the proof for you.

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 18:55):

So we need to make it a confluent rewrite situation

view this post on Zulip Reid Barton (Mar 28 2020 at 18:58):

I mean, you already did the work manually by proving ideal_id and ideal_comp, it just wasn't quite the right work

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 18:58):

So we should be tagging these with simp and also proving something about \Omega_map \b1 or something.

view this post on Zulip Reid Barton (Mar 28 2020 at 19:00):

The rewrites in Ω are definitional equalities anyways. You could omit them and write the whole proof in term mode and it would be very short.

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:00):

@orlando you should try and make the following proofs work:

  map_id' := λ A, begin
    funext I,
   simp
  end,
  map_comp' := begin
    rintros,
    simp,
    funext I,
    simp
end,

view this post on Zulip Reid Barton (Mar 28 2020 at 19:00):

Like, shorter than those proofs.

view this post on Zulip Reid Barton (Mar 28 2020 at 19:01):

(Although I guess the point is that you won't have to write those proofs because of obviously)

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:01):

See how far they get, and then if they don't finish the job, look at where they are stuck and add some simp lemmas to unstick them. Or is Reid saying that there's another way?

view this post on Zulip Reid Barton (Mar 28 2020 at 19:01):

Isn't map_id' := \lam A, funext (\lam I, ideal.ideal_id A I)

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:01):

attribute [simp] ideal.ideal_id I already got

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:02):

but now I have

a : x_1 ∈ Ω_map X X (𝟙 X) x
⊢ x_1 ∈ x

view this post on Zulip Reid Barton (Mar 28 2020 at 19:02):

It's better to "inline" Ω_obj Ω_map anyways

view this post on Zulip Reid Barton (Mar 28 2020 at 19:03):

i.e.

def Ω : Ring  Set :=
{
  obj := ideal,
   ...

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:03):

  obj := λ A, ideal A,
  map := λ A B ψ, ideal.map ψ,

I can't get rid of A or psi

view this post on Zulip Reid Barton (Mar 28 2020 at 19:04):

Yeah, Lean is sometimes dumb :shrug:

view this post on Zulip orlando (Mar 28 2020 at 19:04):

The rw rw category_theory.types_id, in map_id ' is not necesarry

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:09):

attribute [simp] ideal.ideal_id

namespace Omega

@[simp] lemma ideal.map_id (A : Ring) (J : ideal A) : ideal.map (𝟙 A) J = J :=
begin
  ext,
  simp,
end

def Ω : Ring  Set :=
{
  obj := λ A, ideal A,
  map := λ A B ψ, ideal.map ψ,
  map_comp' := begin
    rintros,
    rw category_theory.types_comp,
    funext I,
    exact ideal.ideal_comp X Y Z I f g,
end,
}
end Omega

I now just get a (deterministic) timeout :-/

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:09):

(having removed map_id')

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:11):

wait what? map_id' := begin intros, ext, simp end works fine, but obviously just gets stuck in a loop :-(

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:12):

No, I tell a lie!

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:13):

I had assumed that this was going to end badly, but in fact it compiles fine!

elaboration of Ω took 75.4s

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:14):

Scott -- is this a new record?

view this post on Zulip Reid Barton (Mar 28 2020 at 19:14):

can you have tidy print a trace, then?

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:14):

elaboration: tactic execution took 69.8s
num. allocated objects:  1711
num. allocated closures: 1503
num. allocated big nums: 4
69848ms   100.0%   tactic.replacer
69848ms   100.0%   interaction_monad_orelse
69848ms   100.0%   tactic.istep
69848ms   100.0%   tactic.chain_core
69848ms   100.0%   tactic.chain_many
69848ms   100.0%   tactic.tidy.core
69848ms   100.0%   tactic.step
69848ms   100.0%   tactic.chain_many._main._lambda_1
69848ms   100.0%   _interaction._lambda_2
69848ms   100.0%   tactic.istep._lambda_1
69848ms   100.0%   tactic.tidy
69848ms   100.0%   tactic.first
69848ms   100.0%   tactic.chain_single
69848ms   100.0%   tactic.chain
69848ms   100.0%   _interaction
69848ms   100.0%   tactic.replacer_core
69848ms   100.0%   scope_trace
69848ms   100.0%   tactic.replacer_core._main._lambda_4
69800ms    99.9%   tactic.tidy.default_tactics._lambda_3
68698ms    98.4%   tactic.to_expr
68698ms    98.4%   tactic.tidy.default_tactics._lambda_4
68698ms    98.4%   tactic.interactive.exact
 1014ms     1.5%   tactic.tidy.default_tactics._lambda_8
 1013ms     1.5%   tactic.interactive.dsimp
...

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:15):

Reid Barton said:

can you have tidy print a trace, then?

just a minute

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:16):

Oh I just changed obviously to tidy assuming that this was what you meant, and it's no different. How do I get tidy to print a trace?

view this post on Zulip Reid Barton (Mar 28 2020 at 19:17):

tidy? I think?

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:17):

just a minute

view this post on Zulip Reid Barton (Mar 28 2020 at 19:18):

or slightly longer in this case

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:18):

Try this: intros X, dsimp at *, ext1, dsimp at *, simp at *

view this post on Zulip Reid Barton (Mar 28 2020 at 19:19):

sometimes it is better to write the 1-line term mode proof and move on

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:19):

Oh but that compiles in a reasonable time -- elaboration takes 1 second

view this post on Zulip Reid Barton (Mar 28 2020 at 19:20):

I guess it could be trying other things that fail

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:20):

So every time there's an obviously used in the library, we might be losing up to a minute of compile time when we could just go through them all and replace them with the one-liners which obviously finds, thus speeding up compile time but making the code look uglier.

view this post on Zulip Rob Lewis (Mar 28 2020 at 19:21):

(https://github.com/leanprover-community/mathlib/pull/1204)

view this post on Zulip Johan Commelin (Mar 28 2020 at 19:22):

It might be fun to count how many times there is a transparent call to obviously in the library. Probably a lot.

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:22):

obviously should learn to tidy up after itself: it found intros X, dsimp at *, ext1, dsimp at *, simp at * but intros X, ext1, simp also works and is in some sense a strict subset of the proof originally found.

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:24):

Yes I remember some discussion about this sort of thing when we were doing the T5000 challenge or whatever it was called. But I didn't understand things so well then -- I was more concerned with learning how to do mathematics in Lean at that time rather than learning how it all actually worked.

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:27):

Hey many thanks for that link Rob -- there's a link to the T50000 thread and for me it's well worth a re-read. In particular Floris' comment to me near the top used to say (to me) "blah blah blah, it's like proving 1000+1000=2000 by rfl" which showed me what the problem basically was, but now I can understand what the problem actually was. At the time \ggg terrified me.

view this post on Zulip orlando (Mar 28 2020 at 19:51):

I read slowly,

So Kevin this work !

attribute [simp] ideal.ideal_id
attribute [simp] ideal.ideal_comp
namespace Omega
def Ω_obj (A : Ring):= ideal A
def Ω_map (A B :Ring)(ψ : A  B) : Ω_obj A  Ω_obj B:= λ I,begin
  exact ideal.map ψ I,
end
def Ω : Ring  Set :=
{
  obj := λ A, ideal A,
  map := λ A B ψ, ideal.map ψ,

}
end Omega

view this post on Zulip orlando (Mar 28 2020 at 19:51):

it's your code !

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 19:53):

You can delete \Omega_obj and Omega_map -- Reid says it's better to just define them directly in the structure (like you are doing now)

view this post on Zulip orlando (Mar 28 2020 at 19:54):

yes !

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 20:19):

Does your code now take 10 minutes to compile though? :-/

view this post on Zulip orlando (Mar 28 2020 at 20:32):

20 seconde with simp and 1 seconde with the first code !

view this post on Zulip orlando (Mar 28 2020 at 20:34):

I will make a natural transformation ΩΩ \Omega \to \Omega given by II2I \mapsto I^2 , that's fun :grinning_face_with_smiling_eyes:

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 20:45):

Well you can either prove the missing lemmas with tidy and then click on "try this" (and then it will be quick again) or you can finish this file now, compile it into an olean file, and then import it :-)

view this post on Zulip orlando (Mar 28 2020 at 20:46):

hum what is olean ?

view this post on Zulip orlando (Mar 28 2020 at 20:46):

perhaps i don't understand "compile"

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 20:47):

Are you making these files in a lean project? I hope so. You can just stop editing this file now and start a new file and import this file

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 20:48):

Because this file takes 20 seconds to compile now (the orange bars) but if you import it then it will just compile once and then never compile again until you restart VS code or lean

view this post on Zulip orlando (Mar 28 2020 at 20:48):

Yes yes in a lean project, ok

view this post on Zulip orlando (Mar 28 2020 at 20:48):

i understand

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 20:49):

Or alternatively you can write lean --make path/to/file.lean and then you will have a compiled olean file on your computer

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 20:50):

And then even after you restart lean and Vs code it will still be quick because the olean file stores the 20 seconds

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 20:50):

The reason you don't get orange bars for one hour when you start to use mathlib is because all the oleans are on your computer thanks to leanproject

view this post on Zulip orlando (Mar 28 2020 at 20:51):

ohhh ok !!!

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 20:51):

But in your project there are probably no olean files

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 20:52):

So every time you open the project it has to compile all the files you made which you use or import

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 20:53):

And if one of them takes 20 seconds then this is a pain

view this post on Zulip orlando (Mar 28 2020 at 20:57):

hum i do lean --make but i don't see olean file !

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 21:05):

Do lean --make src/file.lean and it will make file.olean in src

view this post on Zulip Reid Barton (Mar 28 2020 at 21:07):

is leanpkg build no longer a cool thing to do?

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 22:23):

Leanproject build ftw

view this post on Zulip orlando (Mar 30 2020 at 08:15):

Hello, just a question
0/ Omega is the previous files.
1/ In square_ideal_naturality : is it possible to simplify the construction without using the line have H : (Ω.map ψ ∘ square_ideal_app A) I = ideal.map ψ (I * I) and do the rw H directly ?

open Omega
variables (A :Ring)
def square_ideal_app (A : Ring) : ideal A  ideal A := λ I, begin
  exact (I * I),
end
def square_ideal_naturality (A B :Ring) (ψ : A  B)  :
    Ω.map ψ  square_ideal_app B = square_ideal_app A  Ω.map ψ := begin
    rw [category_theory.types_comp,category_theory.types_comp],
    funext  I,
    have H : (Ω.map ψ  square_ideal_app A) I = ideal.map ψ (I * I),
      exact rfl,
    rw H,
    rw ideal.map_mul ψ I I,
    exact rfl,
    end
def square_ideal :  Ω   Ω :=
{
    app := λ A : Ring, square_ideal_app A,
    naturality' := square_ideal_naturality,
}
end Omega_2

view this post on Zulip Kenny Lau (Mar 30 2020 at 08:25):

rw [show _ = _, from rfl]

view this post on Zulip orlando (Mar 30 2020 at 08:33):

Ok, thx Kenny,

view this post on Zulip orlando (Apr 07 2020 at 19:43):

Hello,

Another problem with Ideal :confused:

import algebra.category.CommRing
import ring_theory.ideals
import ring_theory.ideal_operations
universes u
local notation `Ring` := CommRing.{u}
local notation `Set` :=  Type u

lemma set_image_S_subset_set_image_span_S (A B : Ring )(f : A  B) (S : set A) :
set.image f S   set.image f (ideal.span S) :=
begin
    apply set.image_subset,
    exact ideal.subset_span,
end


lemma ideal.map_span_eq_span_image(A B : Ring )(f : A  B) (S : set A):
    ideal.span (set.image f S) = ideal.map f (ideal.span S) :=
begin
    unfold ideal.map,
    apply le_antisymm,
    exact ideal.span_mono (set_image_S_subset_set_image_span_S A B f S),
    have ccl : set.image f (ideal.span S)  ideal.span (set.image f S),
        sorry, ---- HERE !!!!
    apply ideal.span_le.2 ccl,
end

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 19:48):

Here is the proof for submonoids:

lemma closure_preimage_le (f : M →* N) (s : set N) :
  closure (f ⁻¹' s)  (closure s).comap f :=
closure_le.2 $ λ x hx, mem_coe.2 $ mem_comap.2 $ subset_closure hx

lemma map_mclosure (f : M →* N) (s : set M) :
  (closure s).map f = closure (f '' s) :=
le_antisymm
  (map_le_iff_le_comap.2 $ le_trans (closure_mono $ set.subset_preimage_image _ _)
    (closure_preimage_le _ _))
  (closure_le.2 $ set.image_subset _ subset_closure)

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 19:49):

I think that something similar can be done for ideals as well.

view this post on Zulip orlando (Apr 07 2020 at 19:56):

ok i thinck (closure_le.2 $ set.image_subset _ subset_closure) is the same than my exact ideal.span_mono (set_image_S_subset_set_image_span_S A B f S),

So if i understand, i have to deal with comap ... ahah Kenny play also with comap at the beginning of the topic here

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 19:57):

comap is the preimage

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 20:16):

map = image = pushforward, comap = pullback = preimage

view this post on Zulip orlando (Apr 07 2020 at 20:27):

Ok perhaps it's not the shortest proof :joy:

import algebra.category.CommRing
import ring_theory.ideals
import ring_theory.ideal_operations
universes u
local notation `Ring` := CommRing.{u}
local notation `Set` :=  Type u
lemma set_image_S_subset_set_image_span_S (A B : Ring )(f : A  B) (S : set A) :
set.image f S   set.image f (ideal.span S) :=
begin
    apply set.image_subset,
    exact ideal.subset_span,
end

lemma ideal.map_span_eq_span_image(A B : Ring )(f : A  B) (S : set A):
    ideal.span (set.image f S) = ideal.map f (ideal.span S) :=
begin
    -- unfold ideal.map,
    apply le_antisymm,
    exact ideal.span_mono (set_image_S_subset_set_image_span_S A B f S),
    have ccl3 : S  ideal.comap f (ideal.span (set.image f S)),
        unfold ideal.comap,
        have T : S  f ⁻¹' (ideal.span (f '' S)),
            have T' : set.image f S  (ideal.span (f '' S)),
                exact ideal.subset_span,
            apply set.image_subset_iff.1 T',
    exact T,
    have ccl2 : ideal.span S  ideal.comap f (ideal.span (set.image f S)),
           apply ideal.span_le.2 ccl3,
    have ccl : ideal.map f (ideal.span S)   ideal.span (set.image f S),
        apply ideal.map_le_iff_le_comap.2 ccl2,
    exact ccl,
end

view this post on Zulip orlando (Apr 07 2020 at 20:35):

lemma set_image_S_subset_set_image_span_S (A B : Ring )(f : A  B) (S : set A) :
set.image f S   set.image f (ideal.span S) :=
begin
    apply set.image_subset,
    exact ideal.subset_span,
end

lemma ideal.map_span_eq_span_image(A B : Ring )(f : A  B) (S : set A):
    ideal.span (set.image f S) = ideal.map f (ideal.span S) :=
begin
    apply le_antisymm,
    exact ideal.span_mono (set_image_S_subset_set_image_span_S A B f S),
    exact ideal.map_le_iff_le_comap.2 (ideal.span_le.2 (set.image_subset_iff.1 (ideal.subset_span))),
end

view this post on Zulip orlando (Apr 07 2020 at 20:36):

shorter :grinning_face_with_smiling_eyes:

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 20:44):

I wonder what is the general statement here. Probably it should involve four galois_insertions (two closure/coe, image/preimage, and map/comap).

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 20:54):

Hey @orlando it's great that your proofs got shorter -- now can you write them in term mode? That way they will compile quicker

view this post on Zulip Patrick Massot (Apr 07 2020 at 20:55):

I'm not sure this is true.

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 20:55):

Opening up tactic mode has a cost, no?

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 20:59):

For short proofs this should be true but for longer proofs elaborating parts one after another may help Lean. At least I remember some proofs that were failing in term mode because Lean wanted to elaborate arguments left to right. Rewriting using refine; exact made them work. I suspect that it's possible to make an example where "fails" will be replaced by "slow".

view this post on Zulip orlando (Apr 07 2020 at 20:59):

without Begin end ??? Kevin ?

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 21:05):

BTW, you can use #print to see the term mode proof generated by your tactic mode proof.

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 21:05):

It can be much longer than the tactic proof.

view this post on Zulip orlando (Apr 09 2020 at 15:34):

hum another problem i don't know how to do this without the description in term of linear combinaison :confused:

import algebra.category.CommRing
import ring_theory.ideals
import ring_theory.ideal_operations
local notation `Ring` := CommRing.
lemma inverse_image_ideal (A B : Ring)(f : A  B)(S : set B) :
    ideal.span (set.preimage f S) = ideal.comap f (ideal.span S) :=
    begin
        apply le_antisymm,  -- double inclusion
        rw ideal.span_le,   -- span S \leq I ↔  S ≤ I
        apply set.preimage_mono ideal.subset_span,
        sorry,
    end

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 15:43):

Is this true?

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 15:44):

What about A=ZA=\mathbb{Z} and B=CB=\mathbb{C} and S={π}S=\{\pi\}?

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 15:46):

You have access to "proof using linear combination" with things like submodule.span_induction

view this post on Zulip orlando (Apr 09 2020 at 16:03):

:face_palm: :face_palm:


Last updated: May 19 2021 at 02:10 UTC