The represented augmented support flag #
After choosing integer lattice charts with injective reductions modulo p,
the augmented support diagram admits a representation on the old cumulative
support spans. Its maps are the modular chart inverses of the augmented maps.
@[reducible, inline]
noncomputable abbrev
EGZ.FlagDecomposition.Augmented.representation
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(e : Φ.flag.Node → ℕ)
(ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p)
(hp : Odd p)
(he : Antitone e)
(C : (x : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x))
(hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
:
FpRepresentation p d ((diagram Φ e ξ hp he).chartedFlag C)
A surjective representation of the charted augmented flag.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
EGZ.FlagDecomposition.Augmented.representation_map
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(e : Φ.flag.Node → ℕ)
(ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p)
(hp : Odd p)
(he : Antitone e)
(C : (x : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x))
(hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(x : Φ.flag.Node)
:
@[simp]
theorem
EGZ.FlagDecomposition.Augmented.representation_space
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(e : Φ.flag.Node → ℕ)
(ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p)
(hp : Odd p)
(he : Antitone e)
(C : (x : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x))
(hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(x : Φ.flag.Node)
:
(representation Φ e ξ hp he C hmod).space x = affineSpan (ZMod p) {v : FpCoord p d | Φ.cumulativeWeight x v ≠ 0}
theorem
EGZ.FlagDecomposition.Augmented.local_supported
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(e : Φ.flag.Node → ℕ)
(ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p)
(hp : Odd p)
(he : Antitone e)
(C : (x : Φ.flag.Node) → IntegerLatticeChart (support Φ e ξ x))
(hmod : ∀ (x : Φ.flag.Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(x : Φ.flag.Node)
(v : FpCoord p d)
(hv : Φ.localWeight x v ≠ 0)
: