hypothesis in variable disappear

Stream: new members

[Chengyan Hu]

Hi! There's a small thing confused me: I made an assumption hlp during setting up variables, but when I trying to write a proof of a theorem, It seems lean doesn't allow me to apply it.

import Mathlib

variable
    -- let K be a number field with ring of integers A
    (A K : Type*)
    [CommRing A] [IsDedekindDomain A]
    [Field K] [NumberField K] [Algebra A K]
    [IsFractionRing A K]
    [IsIntegralClosure A ℤ K]
    -- let L be an algebraic closure of K
    (L : Type*) [Field L] [Algebra K L]
    [Algebra A L] [IsScalarTower A K L]
    [IsAlgClosure K L]
    -- and let B be the integral closure of A in L
    (B : Type*) [CommRing B] [Algebra B L]
    [Algebra A B] [IsScalarTower A B L]
    [IsIntegralClosure B A L]
    -- Let G be the Galois group of L/K
    variable (G : Type*) [Group G]
    [MulSemiringAction G L]
    [SMulCommClass G K L]
    [Algebra.IsInvariant K L G]
    [MulSemiringAction G B]
    [SMulCommClass G A B]
    [Algebra.IsInvariant A B G]
    [IsScalarTower G B L]
    -- Let F be an element of G
    (F : G)
    -- Let I be a maximal ideal of B
    (I : Ideal B) (hI : I.IsMaximal)
    -- assume F is a Frobenius element at I
    (hF : IsArithFrobAt A F I)
    -- Then for a prime ell not in I...
    (l : ℕ) [Fact (Nat.Prime l)](hlp : ↑l ∉ I)

-- the value of the cyclotomic character at Frob_I is #A/PA where P = I ∩ A
theorem cyclo_thing :
    ((cyclotomicCharacter L l (MulSemiringAction.toRingEquiv G L F)) : ℤ_[l]) =
      Nat.card (A ⧸ I.under A) := by
      have primeI: I.IsPrime := sorry
      have : ∀i:ℕ , ↑(l^i) ∉ I := by
        by_contra hi
        simp at hi
        rw[← Ideal.mem_radical_iff] at hi
        rw[Ideal.IsPrime.radical primeI] at hi
        exact hlp hi

[Aaron Liu]

You have to include hlp in your theorem

[Chengyan Hu]

Thanks! But I'm kind of confused how can I do this

[Chengyan Hu]

And, why won't the set up of variable automatically being assumed in the theorem even I'm using the same variable?

[Aaron Liu]

Chengyan Hu said:

Thanks! But I'm kind of confused how can I do this

Just write

import Mathlib

variable
    -- let K be a number field with ring of integers A
    (A K : Type*)
    [CommRing A] [IsDedekindDomain A]
    [Field K] [NumberField K] [Algebra A K]
    [IsFractionRing A K]
    [IsIntegralClosure A ℤ K]
    -- let L be an algebraic closure of K
    (L : Type*) [Field L] [Algebra K L]
    [Algebra A L] [IsScalarTower A K L]
    [IsAlgClosure K L]
    -- and let B be the integral closure of A in L
    (B : Type*) [CommRing B] [Algebra B L]
    [Algebra A B] [IsScalarTower A B L]
    [IsIntegralClosure B A L]
    -- Let G be the Galois group of L/K
    variable (G : Type*) [Group G]
    [MulSemiringAction G L]
    [SMulCommClass G K L]
    [Algebra.IsInvariant K L G]
    [MulSemiringAction G B]
    [SMulCommClass G A B]
    [Algebra.IsInvariant A B G]
    [IsScalarTower G B L]
    -- Let F be an element of G
    (F : G)
    -- Let I be a maximal ideal of B
    (I : Ideal B) (hI : I.IsMaximal)
    -- assume F is a Frobenius element at I
    (hF : IsArithFrobAt A F I)
    -- Then for a prime ell not in I...
    (l : ℕ) [Fact (Nat.Prime l)](hlp : ↑l ∉ I)

include hlp in
/-- the value of the cyclotomic character at Frob_I is #A/PA where P = I ∩ A -/
theorem cyclo_thing :
    ((cyclotomicCharacter L l (MulSemiringAction.toRingEquiv G L F)) : ℤ_[l]) =
      Nat.card (A ⧸ I.under A) := by
      have primeI: I.IsPrime := sorry
      have : ∀i:ℕ , ↑(l^i) ∉ I := by
        by_contra hi
        simp at hi
        rw[← Ideal.mem_radical_iff] at hi
        rw[Ideal.IsPrime.radical primeI] at hi
        exact hlp hi

[Robin Arnez]

probably do same with hI, hF (include hI hF hlp in ...)

[Chengyan Hu]

Ahhh I see! Thanks! But I'm kind of curious if there is some method to automatically including every hypothesis I made on the variables during setting up?

[Aaron Liu]

Chengyan Hu said:

And, why won't the set up of variable automatically being assumed in the theorem even I'm using the same variable?

From the 4.11.0 release notes:

The variable inclusion mechanism has been changed. Like before, when a definition mentions a variable, Lean will add it as an argument of the definition, but now in theorem bodies, variables are not included based on usage in order to ensure that changes to the proof cannot change the statement of the overall theorem. Instead, variables are only available to the proof if they have been mentioned in the theorem header or in an include command or are instance implicit and depend only on such variables. The omit command can be used to omit included variables.

[Robin Arnez]

I guess

import Mathlib

theorem cyclo_thing
    -- let K be a number field with ring of integers A
    (A K : Type*)
    [CommRing A] [IsDedekindDomain A]
    [Field K] [NumberField K] [Algebra A K]
    [IsFractionRing A K]
    [IsIntegralClosure A ℤ K]
    -- let L be an algebraic closure of K
    (L : Type*) [Field L] [Algebra K L]
    [Algebra A L] [IsScalarTower A K L]
    [IsAlgClosure K L]
    -- and let B be the integral closure of A in L
    (B : Type*) [CommRing B] [Algebra B L]
    [Algebra A B] [IsScalarTower A B L]
    [IsIntegralClosure B A L]
    -- Let G be the Galois group of L/K
    (G : Type*) [Group G]
    [MulSemiringAction G L]
    [SMulCommClass G K L]
    [Algebra.IsInvariant K L G]
    [MulSemiringAction G B]
    [SMulCommClass G A B]
    [Algebra.IsInvariant A B G]
    [IsScalarTower G B L]
    -- Let F be an element of G
    (F : G)
    -- Let I be a maximal ideal of B
    (I : Ideal B) (hI : I.IsMaximal)
    -- assume F is a Frobenius element at I
    (hF : IsArithFrobAt A F I)
    -- Then for a prime ell not in I...
    (l : ℕ) [Fact (Nat.Prime l)](hlp : ↑l ∉ I) :
    ((cyclotomicCharacter L l (MulSemiringAction.toRingEquiv G L F)) : ℤ_[l]) =
      Nat.card (A ⧸ I.under A) := by
  have primeI : I.IsPrime := hI.isPrime
  have : ∀ i : ℕ, (l : B) ^ i ∉ I := by
    by_contra! hi
    rw [← Ideal.mem_radical_iff] at hi
    rw [Ideal.IsPrime.radical primeI] at hi
    exact hlp hi

[Chengyan Hu]

As if I have to include each time, why should I write things in setting up stage instead of just write hypothesis in theorem

[Robin Arnez]

Usually hypotheses are part of the theorem and the variables are only types and instances

[Chengyan Hu]

Ah I see!

[Chengyan Hu]

It makes things clear

[Chengyan Hu]

Thank you guys

[Robin Arnez]

Also please write Type* variables in curly braces, e.g. {A K : Type*}, otherwise you have to specified directly when trying to use this

[Chengyan Hu]

Get it!

[Notification Bot]

Chengyan Hu has marked this topic as resolved.

[Philippe Duchon]

So, there is no way of setting up a number of hypotheses, say in a section, so that they will automatically be included in every theorem of the section?

The way I understand things, any declared variables that are mentioned in the statement of the theorem (typically, data rather than properties) will be included in the statement, but any property-valued hypotheses will have to be included manually, right? (I didn't know about this "include ... in" until five minutes ago)

This makes the variable declaration much less useful, even though I understand the rationale about making the theorem statements not depend on their proof script.

[Notification Bot]

Chengyan Hu has marked this topic as unresolved.

[Anthony Fernandes]

So, there is no way of setting up a number of hypotheses, say in a section, so that they will automatically be included in every theorem of the section?

I don't know if it is against mathlib's style policy (really need to read it again) but you can use include my_hypothesis (without in) to include it in all subsequent declarations in the current section, even where it is not needed.

The way I understand things, any declared variables that are mentioned in the statement of the theorem (typically, data rather than properties) will be included in the statement, but any property-valued hypotheses will have to be included manually, right? (I didn't know about this "include ... in" until five minutes ago)

Essentially yes except with cautious use of what I just said.

This makes the variable declaration much less useful, even though I understand the rationale about making the theorem statements not depend on their proof script.

It is still useful like in the initial example of this thread when declaring types, elements of those types and loads of instances.