target of ring hom algebra over image

Stream: maths

[Ashwin Iyengar]

If I have a commutative unital ring homomorphism $f: A \to B$, then does mathlib know that $B$ is an $f(A)$-algebra? What would be the best way to access this instance of being an algebra?

[Ashwin Iyengar]

Or do I just have to construct it

[Kevin Buzzard]

What do you mean by f(A)? There is a type v term issue here. The image of f has type subring B so in particular it's a term. However algebra X B needs X to be a type. Do you really need to consider this image? Would you be happy with the idea that B is an A-algebra? That is much easier.

[Adam Topaz]

If you insist:

import algebra.algebra.basic

variables (A B : Type*) [comm_ring A] [comm_ring B]

example (f : A →+* B) : algebra (f.range) B :=
algebra.of_subring _

[Adam Topaz]

(found using library_search BTW)

[Eric Wieser]

Doesn't apply_instance find it?

[Ashwin Iyengar]

Thanks! I think I am actually happy for $B$ to be an $A$ algebra in the end.

[Notification Bot]

Ashwin Iyengar has marked this topic as unresolved.

[Ashwin Iyengar]

I guess I want to say "a field $F$ of characteristic $p$ such that $[F:F^p]$ is finite". So I want to write something like finite_dimensional (frobenius F p).range F, but this doesn't work because, among other reasons, (frobenius F p).range is a term rather than a type. So instead I want to say something like finite_dimensional F F but I want to view the second F as a module over F via frobenius rather than the canonical module structure. I've been searching the docs but can't figure out how to do this in a clean way. Any help would be appreciated.

[Adam Topaz]

I would introduce a type alias for the second F (the target of the Frobenius map), and consider it as an F algebra w.r.t. Frob.

[Adam Topaz]

In any case, you can still use the range and write finite_dimensional Frob.range F or something like this. I don't know how Frobenius is denoted in mathlib.

[Adam Topaz]

Oh, I guess it should be finite_dimensional (frobenius F p).range F. I'm surprised that doesn't work...

[Adam Topaz]

Aha! The issue is not that it's a term as opposed to a type (because there is a coercion to sort), but rather that mathlib doesn't know that the image will be a division ring, which is required for finite_dimensional.

[Adam Topaz]

Okay, that's indeed the issue:

import algebra.char_p.basic
import linear_algebra.finite_dimensional
import algebra.algebra.basic

universe u
variables (F : Type*) [field F] (p : ℕ) [fact (nat.prime p)] [char_p F p]

instance : field (frobenius F p).range :=
{ inv := sorry,
  div := sorry,
  div_eq_mul_inv := sorry,
  zpow := sorry,
  zpow_zero' := sorry,
  zpow_succ' := sorry,
  zpow_neg' := sorry,
  exists_pair_ne := sorry,
  mul_inv_cancel := sorry,
  inv_zero := sorry,
  ..(infer_instance : comm_ring _) }

example : Prop := finite_dimensional (frobenius F p).range F

[Ashwin Iyengar]

Ah ok! That's interesting, thanks

[Ashwin Iyengar]

the mathlib docs suggest you can make an aliases of a def or theorem, but how do you alias a type?

[Adam Topaz]

It can be as easy as def K := F.

[Adam Topaz]

But the issue of considering F as an algebra over itself with respect to Frobenius is important enough that we should give some thought about how to do this properly so that it's easy to work with. Unfortunately, I won't be able to help with this tonight.

[Ashwin Iyengar]

Ah okay. Maybe it's worth making an instance of field for the image whenever you have a nontrivial homomorphism from a field?

[Kevin Buzzard]

I think the right generality is "homomorphism from a field into a nontrivial ring" and yes I think the type class inference system should be able to handle this.

[Eric Wieser]

There's possibly a trap here when that nontrivial ring is already a field

[Eric Wieser]

Which might end up creating an equal but not defeq diamond in has_inv

[Kevin Buzzard]

but the range will be a subring, right?

[Damiano Testa]

Picking up on what Eric says, non-trivial field automorphisms seem worrying. For instance, there was a recent thread precisely about the image of Frobenius. If the field is perfect (and not the prime field), wouldn't this create issues?

[Kevin Buzzard]

I am not sure what the concern is here; ↥(frobenius F p).range will never be definitionally equal to F.

[Damiano Testa]

Ok, I think that I understand, thanks!

I was worried about potentially creating loops, where the image of a field is a field recursively. But, if I understand correctly, this creates more and more complicated types.

[Kevin Buzzard]

Yeah, subrings are more complex than rings in Lean! Just like the quotient $X/\sim$ is more complicated than $X$ so they write it above it and we get quotient.lift :-)

[Damiano Testa]

Yes, I find this very confusing, even though I understand the motivation. Even knowing this, I still get it wrong!

[Ashwin Iyengar]

When I do obtain below it suddenly changes the goal state so that the code below doesn't compile. I'm a little confused as to why not.

import algebra.algebra.basic

variables (F R : Type*) [field F] [comm_ring R] (f : F →+* R) [nontrivial R]

noncomputable theory

instance : field f.range :=
field_of_is_unit_or_eq_zero (λ a,
  begin
    cases em (a = 0),
    { right, assumption },
    { left,
      let y := function.injective.exists_unique_of_mem_range f.injective a.prop,
      obtain ⟨lift, prop⟩ := y,
      let l : lift ≠ 0 := sorry,
      let a_unit := ring_hom.is_unit_map f (is_unit.mk0 lift l),
      rw prop.1 at a_unit,
      exact a_unit
    }
  end
)

[Ashwin Iyengar]

Okay nevermind, this apparently had something to do with the fact that I used y, this almost works:

import algebra.char_p.basic
import linear_algebra.finite_dimensional
import algebra.algebra.basic

variables (F R : Type*) [field F] [comm_ring R] (f : F →+* R) [nontrivial R]

noncomputable theory

instance : field f.range :=
field_of_is_unit_or_eq_zero (λ a,
  begin
    cases em (a = 0),
    { right, assumption },
    { left,
      obtain ⟨lift, prop⟩ := function.injective.exists_unique_of_mem_range f.injective a.prop,
      let l : lift ≠ 0 := sorry,
      let a_unit := ring_hom.is_unit_map f (is_unit.mk0 lift l),
      rw prop.1 at a_unit,
      exact a_unit
    }
  end
)

[Yaël Dillies]

I suspect the culprit was let.

[Adam Topaz]

This should be true for division rings as well, right?

[Yaël Dillies]

The one thing you have to pay attention to diamond-wise is to never define field (subtype p), because it would match yours.

[Kevin Buzzard]

Yaël said:

I suspect the culprit was let.

What he means is "use let when defining data, but use have when defining proofs". So for example your let l : lift ≠ 0 := sorry, should be have l : lift ≠ 0 := sorry,.

[Kevin Buzzard]

this almost works

Your problem is that you haven't quite proved enough. You have a in the range and you know ↑a, its image in R, is a unit, but that's not enough to deduce that a is a unit because you don't know the inverse is also in the range.

[Kevin Buzzard]

I think a case split on the preimage of a in F is easier.

instance : field f.range :=
field_of_is_unit_or_eq_zero (λ a,
  begin
    rcases a with ⟨_, b, rfl⟩,
    cases em (b = 0),
    { right, ext, simp [h] },
    { left,
      exact is_unit.map f.range_restrict (is_unit.mk0 _ h) }
  end
)

[Ashwin Iyengar]

Ohh thank you, I didn't know about range_restrict

[Kevin Buzzard]

Neither did I until I went looking for it because of your question :-)