Ideal lemma

Stream: maths

[orlando]

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

[orlando]

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

[Mario Carneiro]

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

[orlando]

Ok, but the little problem is $g$ is not $A$ module morphism

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kenny Lau]

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)

[Kevin Buzzard]

Kenny can you do this with ring_hom?

[Kevin Buzzard]

Just to show Orlando the bundled approach?

[Mario Carneiro]

what was that galois connection emoji again

[Kenny Lau]

ideal.map takes is_ring_hom

[Kevin Buzzard]

:-/

[Mario Carneiro]

refactor time

[Kevin Buzzard]

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

[Kevin Buzzard]

Ideals are submodules not modules

[Mario Carneiro]

zulip needs autocompletion

[Kevin Buzzard]

And easy ability to input Unicode on phones

[orlando]

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

[orlando]

What is the $ ???

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

we should put that in the faq

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

$ is particularly bad in this regard

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Johan Commelin]

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:

[Kevin Buzzard]

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

[orlando]

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

[Kevin Buzzard]

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.

[Johan Commelin]

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.

[Kevin Buzzard]

@orlando you can replace

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

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

Did you see the definition of functor in mathlib?

[orlando]

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 ?

[Kevin Buzzard]

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".

[Kevin Buzzard]

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

[orlando]

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

[Kevin Buzzard]

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?

[Johan Commelin]

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.

[Johan Commelin]

Currently obviously cannot do rw

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

So we need to make it a confluent rewrite situation

[Reid Barton]

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

[Kevin Buzzard]

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

[Reid Barton]

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.

[Kevin Buzzard]

@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,

[Reid Barton]

Like, shorter than those proofs.

[Reid Barton]

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

[Kevin Buzzard]

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?

[Reid Barton]

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

[Kevin Buzzard]

attribute [simp] ideal.ideal_id I already got

[Kevin Buzzard]

but now I have

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

[Reid Barton]

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

[Reid Barton]

i.e.

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

[Kevin Buzzard]

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

I can't get rid of A or psi

[Reid Barton]

Yeah, Lean is sometimes dumb :shrug:

[orlando]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

(having removed map_id')

[Kevin Buzzard]

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

[Kevin Buzzard]

No, I tell a lie!

[Kevin Buzzard]

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

elaboration of Ω took 75.4s

[Kevin Buzzard]

Scott -- is this a new record?

[Reid Barton]

can you have tidy print a trace, then?

[Kevin Buzzard]

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
...

[Kevin Buzzard]

Reid Barton said:

can you have tidy print a trace, then?

just a minute

[Kevin Buzzard]

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?

[Reid Barton]

tidy? I think?

[Kevin Buzzard]

just a minute

[Reid Barton]

or slightly longer in this case

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Reid Barton]

I guess it could be trying other things that fail

[Kevin Buzzard]

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.

[Rob Lewis]

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

[Johan Commelin]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[orlando]

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

[orlando]

it's your code !

[Kevin Buzzard]

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)

[orlando]

yes !

[Kevin Buzzard]

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

[orlando]

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

[orlando]

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

[Kevin Buzzard]

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

[orlando]

hum what is olean ?

[orlando]

perhaps i don't understand "compile"

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[orlando]

Yes yes in a lean project, ok

[orlando]

i understand

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[orlando]

ohhh ok !!!

[Kevin Buzzard]

But in your project there are probably no olean files

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[orlando]

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

[Kevin Buzzard]

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

[Reid Barton]

is leanpkg build no longer a cool thing to do?

[Kevin Buzzard]

Leanproject build ftw

[orlando]

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

[Kenny Lau]

rw [show _ = _, from rfl]

[orlando]

Ok, thx Kenny,

[orlando]

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

[Yury G. Kudryashov]

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)

[Yury G. Kudryashov]

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

[orlando]

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

[Yury G. Kudryashov]

comap is the preimage

[Kevin Buzzard]

map = image = pushforward, comap = pullback = preimage

[orlando]

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

[orlando]

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

[orlando]

shorter :grinning_face_with_smiling_eyes:

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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

[Patrick Massot]

I'm not sure this is true.

[Kevin Buzzard]

Opening up tactic mode has a cost, no?

[Yury G. Kudryashov]

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".

[orlando]

without Begin end ??? Kevin ?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

It can be much longer than the tactic proof.

[orlando]

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

[Kevin Buzzard]

Is this true?

[Kevin Buzzard]

What about $A=\mathbb{Z}$ and $B=\mathbb{C}$ and $S=\{\pi\}$?

[Kevin Buzzard]

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

[orlando]

:face_palm: :face_palm: